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:

```
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”:

```
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`

:

```
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:

```
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:

```
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:

```
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:

```
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:

```
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):

```
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:

```
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…

```
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.

```
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.