Getting List.Exists into an induction principle

Using Coq
1

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.

2

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
3

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