# Getting List.Exists into an induction principle

**URL:** <https://discourse.rocq-prover.org/t/getting-list-exists-into-an-induction-principle/1924>\
**Category:** Using Rocq\
**Created:** [April 9, 2023, 4:02pm UTC](https://discourse.rocq-prover.org/t/getting-list-exists-into-an-induction-principle/1924 "2023-04-09T16:02:28Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![io7m](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/io7m/32/643_2.png) [@io7m](https://discourse.rocq-prover.org/u/io7m)\
**Post date:** [April 9, 2023, 4:02pm UTC](https://discourse.rocq-prover.org/t/getting-list-exists-into-an-induction-principle/1924/1 "2023-04-09T16:02:28Z")

</div>

Hello!

This is a severely reduced example from a larger development, so apologies if some of it seems a bit silly. I’m running into an issue (once again) with custom induction principles. I’ll try to illustrate. Here’s a subset of a small expression language:

```auto
Require Import Coq.Lists.List.

Import ListNotations.

Inductive exp0 :=
  | E0_True : exp0
  | E0_False : exp0
  | E0_And : list exp0 -> exp0
  .

```

Here’s a relation that expresses whether or not a given expression is “true”:

```auto
Inductive istrue0 : exp0 -> Prop :=
  | M0_True : istrue0 E0_True
  | M0_And : forall es, Forall istrue0 es -> istrue0 (E0_And es)
  .

```

And here’s a decision procedure that maps `exp0` values to `bool`:

```auto
Fixpoint istrueF0 (e : exp0) : bool :=
  match e with
  | E0_True => true
  | E0_False => false
  | E0_And es => forallb istrueF0 es
  end.

```

We’d like to prove that `forall e, istrue0 e -> istrueF0 e = true.`, and this seems straightforward until you hit the `E0_And` case:

```auto
Lemma istrue0_istrueF0_eq : forall e, istrue0 e -> istrueF0 e = true.
Proof.
  induction e.
  - intro H.
    reflexivity.
  - intros Hcontra.
    inversion Hcontra.
  - (* EAnd *)
    intro H.
 (* ^^^^^^^ *)
Abort.

```

At this point, the context looks like this:

```auto
1 goal
l : list exp0
H : istrue0 (E0_And l)
______________________________________ (1/1)
(istrueF0 (E0_And l)) = true

```

Obviously, we’re missing a usable induction hypothesis. This is due to the well-understood limitations in the way induction principles are generated. We can define our own:

```auto
Section rect.
  Variable P : exp0 -> Type.
  Variable P_ForAll_list : list exp0 -> Type.
  Hypothesis P_ForAll_nil : P_ForAll_list [].
  Hypothesis P_ForAll_cons : forall x xs, P x -> P_ForAll_list xs -> P_ForAll_list (x :: xs).

  Hypothesis P_True : P E0_True.
  Hypothesis P_False : P E0_False.
  Hypothesis P_And : forall es, P_ForAll_list es -> P (E0_And es).

  Fixpoint exp0_new_rect (e : exp0) : P e :=
    let
      fix e_for_all (xs : list exp0) : P_ForAll_list xs :=
        match xs as rxs return (P_ForAll_list rxs) with
        | [] => @P_ForAll_nil
        | (y :: ys) => @P_ForAll_cons y ys (exp0_new_rect y) (e_for_all ys)
        end
    in
      match e with
      | E0_True => P_True
      | E0_False => P_False
      | E0_And es => P_And es (e_for_all es)
      end.

End rect.

Section ind.
  Variable P : exp0 -> Prop.
  Hypothesis P_True : P E0_True.
  Hypothesis P_False : P E0_False.
  Hypothesis P_And : forall es, Forall P es -> P (E0_And es).

  Definition exp0_new_ind (e : exp0) : P e :=
    exp0_new_rect
      P
      (List.Forall P)
      (List.Forall_nil P)
      (fun x xs Px Pxs => @List.Forall_cons _ P x xs Px Pxs)
      P_True
      P_False
      P_And
      e.
End ind.

```

And then we can prove the original theorem without too much pain:

```auto
Lemma Forall_impl_lifted : forall
  (A : Type)
  (P : A -> Prop)
  (Q : A -> Prop)
  (xs : list A),
  Forall (fun x => P x) xs ->
    Forall (fun x => P x -> Q x) xs ->
      Forall (fun x => Q x) xs.
Proof.
  induction xs as [|y ys IH]. {
    intros F0 H1.
    constructor.
  } {
    intros F0 F1.
    constructor. {
      apply (Forall_inv F1).
      apply (Forall_inv F0).
    } {
      apply IH.
      apply (Forall_inv_tail F0).
      apply (Forall_inv_tail F1).
    }
  }
Qed.

Lemma istrue0_istrueF0_eq : forall e, istrue0 e -> istrueF0 e = true.
Proof.
  induction e as [| |xs Hxs] using exp0_new_ind.
  - intro H.
    reflexivity.
  - intros Hcontra.
    inversion Hcontra.
  - (* EAnd *)
    intro Hand.
    destruct xs as [|y ys].
    * reflexivity.
    * simpl.
      rewrite Bool.andb_true_iff.
      inversion Hand.
      pose proof (Forall_inv H0) as H1.
      pose proof (Forall_inv_tail H0) as H2.
      constructor. {
        apply (Forall_inv Hxs).
        exact H1.
      } {
        rewrite forallb_forall.
        rewrite <- Forall_forall.
        apply (Forall_impl_lifted exp0 istrue0 _ ys H2 (Forall_inv_tail Hxs)).
      }
Qed.

```

Now imagine the original expression language is extended with an `or` expression:

```auto
Inductive exp1 :=
  | E1_True : exp1
  | E1_False : exp1
  | E1_And : list exp1 -> exp1
  | E1_Or : list exp1 -> exp1
  .

```

The corresponding `istrue` relation needs a case for the `E1_Or` case, and the most reasonable encoding seems to be to use `List.Exists` (because if any of the subexpressions of an `or` are true, then the `or` expression is true; we don’t care which subexpression was true):

```auto
Inductive istrue1 : exp1 -> Prop :=
  | M1_True : istrue1 E1_True
  | M1_And : forall es, Forall istrue1 es -> istrue1 (E1_And es)
  | M1_Or : forall es, Exists istrue1 es -> istrue1 (E1_Or es)
  .

```

This is where I run into (at least one) issue trying to define a similar induction principle as before. I’m not sure what the most sane arrangement of propositions is:

```auto
Section rect.
  Variable P : exp1 -> Type.
  Variable P_ForAll_list : list exp1 -> Type.
  Hypothesis P_ForAll_nil : P_ForAll_list [].
  Hypothesis P_ForAll_cons : forall x xs, P x -> P_ForAll_list xs -> P_ForAll_list (x :: xs).

  Variable P_Exists_list : list exp1 -> Type.
  Hypothesis P_Exists_nil : P_Exists_list [] -> False.
  Hypothesis P_Exists_cons : forall x xs, P x -> P_Exists_list (x :: xs).

```

I’m not convinced by these `P_Exists` lines…

```auto
  Hypothesis P_True : P E1_True.
  Hypothesis P_False : P E1_False.
  Hypothesis P_And : forall es, P_ForAll_list es -> P (E1_And es).
  Hypothesis P_Or : forall es, P_Exists_list es -> P (E1_Or es).

  Program Fixpoint exp1_new_rect (e : exp1) : P e :=
    let
      fix e_for_all (xs : list exp1) : P_ForAll_list xs :=
        match xs as rxs return (P_ForAll_list rxs) with
        | [] => @P_ForAll_nil
        | (y :: ys) => @P_ForAll_cons y ys (exp1_new_rect y) (e_for_all ys)
        end
    in let
      fix e_exists (xs : list exp1) : P_Exists_list xs :=
        match xs as rxs return (P_Exists_list rxs) with
        | [] => @False_rect (P_Exists_list []) _
        | (y :: ys) => @P_Exists_cons y ys (exp1_new_rect y)
        end
    in
      match e with
      | E1_True => P_True
      | E1_False => P_False
      | E1_And es => P_And es (e_for_all es)
      | E1_Or es => P_Or es (e_exists es)
      end.

```

… And the resulting principle seems malformed anyway. I’m not ultimately intending to use `Program Fixpoint` over a plain `Fixpoint`, but I just wanted to see what kind of type errors it might produce.

```auto
Recursive definition of e_exists is ill-formed.
In environment
P : exp1 -> Type
P_ForAll_list : (list exp1) -> Type
P_ForAll_nil : P_ForAll_list []
P_ForAll_cons : forall (x : exp1) (xs : list exp1), (P x) -> (P_ForAll_list xs) -> P_ForAll_list (x :: xs)
P_Exists_list : (list exp1) -> Type
P_Exists_nil : (P_Exists_list []) -> False
P_Exists_cons : forall (x : exp1) (xs : list exp1), (P x) -> P_Exists_list (x :: xs)
P_True : P E1_True
P_False : P E1_False
P_And : forall es : list exp1, (P_ForAll_list es) -> P (E1_And es)
P_Or : forall es : list exp1, (P_Exists_list es) -> P (E1_Or es)
exp1_new_rect : forall e : exp1, P e
e : exp1
e_for_all :=
fix e_for_all (xs : list exp1) : P_ForAll_list xs :=
  match xs as rxs return (P_ForAll_list rxs) with
  | [] => P_ForAll_nil
  | y :: ys => P_ForAll_cons y ys (exp1_new_rect y) (e_for_all ys)
  end : forall xs : list exp1, P_ForAll_list xs
e_exists : forall xs : list exp1, P_Exists_list xs
xs : list exp1
Recursive call to e_exists has principal argument equal to "[]" instead of
a subterm of "xs".
Recursive definition is:
"fun xs : list exp1 =>
 match xs as rxs return (P_Exists_list rxs) with
 | [] => False_rect (P_Exists_list []) (exp1_new_rect_obligation_1 e_exists)
 | y :: ys => P_Exists_cons y ys (exp1_new_rect y)
 end".

```

Obviously, the call that `Program Fixpoint` attempts to synthesize would not terminate (`e_exists []` would ultimately call `e_exists []`).

Is there some other approach I should take? Is this even a reasonable way to express what I’m trying to express? I’m not certain _where_ I’m making the mistake I’m apparently making.

Obviously, I’d prefer not to have to have a custom induction principle at all, but it seems as though I’m required to.

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [April 9, 2023, 4:54pm UTC](https://discourse.rocq-prover.org/t/getting-list-exists-into-an-induction-principle/1924/2 "2023-04-09T16:54:29Z")

</div>

You do not need separate P\_Forall\_list and P\_Exists\_list, we can just use Forall all the time:

```auto
Section rect.
  Variable P : exp1 -> Prop.

  Hypothesis P_True : P E1_True.
  Hypothesis P_False : P E1_False.
  Hypothesis P_And : forall es, Forall P es -> P (E1_And es).
  Hypothesis P_Or : forall es, Forall P es -> P (E1_Or es).

  Fixpoint exp1_new_ind (e : exp1) : P e :=
    let
      fix e_list (xs : list exp1) : Forall P xs :=
      match xs as rxs return (Forall P rxs) with
      | [] => Forall_nil _
      | (y :: ys) => @Forall_cons _ _ y ys (exp1_new_ind y) (e_list ys)
      end
    in
    match e with
    | E1_True => P_True
    | E1_False => P_False
    | E1_And es => P_And es (e_list es)
    | E1_Or es => P_Or es (e_list es)
    end.
End rect.

```

(for `rect` we would need a Type version of Forall)  
Then for the Or case you will need lemma

```auto
Lemma Exists_impl_lifted : forall
  (A : Type)
  (P : A -> Prop)
  (Q : A -> Prop)
  (xs : list A),
  Exists (fun x => P x) xs ->
    Forall (fun x => P x -> Q x) xs ->
      Exists (fun x => Q x) xs.
Proof.
  intros A P Q xs Hex Hforall; induction Hex.
  - constructor 1. apply Forall_inv in Hforall;auto.
  - constructor 2. apply Forall_inv_tail in Hforall; auto.
Qed.

```

(btw Forall\_impl\_lifted should accept a similar short proof)  
then the theorem is

```auto
Lemma istrue1_istrueF1_eq : forall e, istrue1 e -> istrueF1 e = true.
Proof.
  induction e as [| |xs Hxs|xs Hxs] using exp1_new_ind.
  - intro H.
    reflexivity.
  - intros Hcontra.
    inversion Hcontra.
  - (* EAnd *)
    intro Hand.
    simpl.
    rewrite forallb_forall.
    rewrite <- Forall_forall.
    inversion Hand.
    apply (Forall_impl_lifted exp1 istrue1 _ xs H0 Hxs).
  - (* EOr *)
    intro Hor.
    simpl.
    rewrite existsb_exists, <-Exists_exists.
    inversion Hor.
    apply (Exists_impl_lifted exp1 istrue1);auto.
Qed.

```

(notice that the And case was simplified, no need to destruct xs)

The induction hypothesis is `Forall (fun x => istrue x -> istrueF x = true) xs` and you have locally `istrue (Or xs)` ie `Exists istrue xs`.  
Indeed having `Exists (istrue -> ...)` as induction hypothesis would be useless since there would be nothing telling you that it happens at the same element as the `Exists istrue` hypothesis.

---

<div class="post-metadata">

**Author:** ![io7m](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/io7m/32/643_2.png) [@io7m](https://discourse.rocq-prover.org/u/io7m)\
**Post date:** [April 9, 2023, 6:04pm UTC](https://discourse.rocq-prover.org/t/getting-list-exists-into-an-induction-principle/1924/3 "2023-04-09T18:04:54Z")

</div>

Thank you, that’s a very clever solution. For whatever reason, I didn’t spot the usable relationship between `List.Forall` and `List.Exists`.