# Getting List.Exists into an induction principle

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.

You do not need separate P_Forall_list and P_Exists_list, we can just use Forall all the time:

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

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

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

1 Like

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