Can one prove an equivalent to Forall_inv for heterogeneous lists in Coq?

Link:: https://stackoverflow.com/q/59178484

Display all goals and responses

Question

Following Adam Chlipala's definition of heterogeneous lists, I wanted to define an equivalent of the Forall function on normal lists. This isn't too difficult, and you end up with two constructors as usual. Now suppose that I know that a fact is true about every element of a non-empty list. With normal lists, I could use Forall_inv and Forall_inv_tail to assert that it's true about the head and tail of the list.

I'd like to prove the equivalent for hForall as defined below, starting with the head case. Looking at the source in Lists/List.v, the proof for normal lists is easy and runs by inversion on Forall (a :: l). The equivalent for my hForall gives a mess of dependent variables. Am I missing something obvious?

Require Import List.

Section hlist.
  Variable A : Type.
  Variable B : A -> Type.

  Inductive hlist : list A -> Type :=
  | HNil : hlist nil
  | HCons {a : A} {ls : list A} : B a -> hlist ls -> hlist (a :: ls).

  Section hForall.
    Variable P : forall a : A, B a -> Prop.

    Inductive hForall : forall {As : list A}, hlist As -> Prop :=
    | hForall_nil : hForall HNil
    | hForall_cons {a : A} {ls : list A} (x : B a) (hl : hlist ls)
      : P a x -> hForall hl -> hForall (HCons x hl).

    Lemma hForall_inv (a : A) (ls : list A) (x : B a) (hl : hlist ls)
      : hForall (HCons x hl) -> P a x.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
hForall (HCons x hl) -> P a x
    Proof.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
hForall (HCons x hl) -> P a x
      (* Help! *)
    Abort.
  End hForall.
End hlist.

Answer

Inductives indexed by indexed types lead to that kind of difficulty.

Alternatively, consider defining hForall as a Fixpoint. Then the inversion lemma follows by just unfolding the definition.

Section hForall'.

  Variable P : forall a, B a -> Prop.

  Inductive hlist : list A -> Type :=
  | HNil : hlist nil
  | HCons {a : A} {ls : list A} : B a -> hlist ls -> hlist (a :: ls).

  Fixpoint hForall' {As : list A} (hs : hlist As) : Prop :=
    match hs with
    | HNil => True
    | HCons x js => P _ x /\ hForall' js
    end.

  Lemma hForall'_inv (a : A) (ls : list A) (x : B a) (hl : hlist ls)
    : hForall' (HCons x hl) -> P a x.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
hForall' (HCons x hl) -> P a x
  Proof.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
hForall' (HCons x hl) -> P a x
    intros []; auto.
  Qed.

End hForall'.

Appendix

Mostly for educational purposes, here's a few ways to prove that inversion lemma for the original inductive definition of hForall (starting from the simpler to use).

One solution is the dependent destruction tactic, which also automatically handles heterogeneous equalities, as opposed to destruct. It is imported from the Program module:

Require Import Program.Use of “Require” inside a section is fragile. It is
not recommended to use this functionality in finished
proof scripts. [require-in-section,fragile]

Lemma hForall_inv (a : A) (ls : list A) (x : B a) (hl : hlist ls)
  : hForall (HCons x hl) -> P a x.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
hForall (HCons x hl) -> P a x
Proof.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
hForall (HCons x hl) -> P a x
  intros H.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
H: hForall (HCons x hl)
P a x dependent destruction H.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
H: P a x
H0: hForall hl
P a x auto.
Qed.

The (minor) catch is that it uses some axioms about heterogeneous equality:

Print Assumptions hForall_inv.Section Variables:
P
: forall a : A, B a -> Prop
B
: A -> Type
A
: Type
Axioms:
Eqdep.Eq_rect_eq.eq_rect_eq
  : forall (U : Type) (p : U) (Q : U -> Type)
      (x : Q p) (h : p = p), x = eq_rect p Q x p h
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y

With a little more knowledge of how destruct works/dependent pattern-matching, here's a proof without axioms.

There are some detailed explanations of dependent pattern-matching in CPDT, but briefly the issue is that when we do destruct/inversion on hForall (HCons x hl), the index HCons x hl gets generalized before the case-split, so you get a nonsensical case where it is replaced with HNil, and a second case with a different index HCons x0 hl0, and a good way of remembering the (heterogeneous) equality across that generalization is a research-grade problem. You wouldn't need to mess with heterogeneous equalities if the goal just got rewritten with those variables, and indeed you can refactor the goal so that it explicitly depends on HCons x hl, instead of x and hl separately, which will then be generalized by destruct:

Lemma hForall_inv' (a : A) (ls : list A) (x : B a) (hl : hlist ls) :
  hForall (HCons x hl) -> P a x.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
hForall (HCons x hl) -> P a x
Proof.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
hForall (HCons x hl) -> P a x
  intros H.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
H: hForall (HCons x hl)
P a x
  change (match HCons x hl return Prop with
          (* for some reason you have to explicitly annotate the
             return type as Prop right here *)
          | HNil => True
          | HCons x _ => P _ x
          end).A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
H: hForall (HCons x hl)
match HCons x hl with
| HNil => True
| @HCons a0 _ x _ => P a0 x
end
      destruct H.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
True
A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
a0: A
ls0: list A
x0: B a0
hl0: hlist ls0
H: P a0 x0
H0: hForall hl0
P a0 x0
  -A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
True exact I.
  (* Replace [HCons x hl] with [HNil], the goal reduces to [True].
     (This is an unreachable case.) *)
  -A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
a0: A
ls0: list A
x0: B a0
hl0: hlist ls0
H: P a0 x0
H0: hForall hl0
P a0 x0 assumption.

  (* Or, directly writing down the proof term. *)
  Restart.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
hForall (HCons x hl) -> P a x
  intros H.A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
H: hForall (HCons x hl)
P a x
  refine (match H in @hForall As hs return
                match hs return Prop with
                | HNil => True
                | HCons x _ => P _ x
                end
          with
          | hForall_nil => I
          | hForall_cons _ _ _ _ => _
          end).A: Type
B: A -> Type
P: forall a : A, B a -> Prop
a: A
ls: list A
x: B a
hl: hlist ls
H: hForall (HCons x hl)
a0: A
l: list A
b: B a0
h: hlist l
p: P a0 b
h0: hForall h
P a0 b
  assumption.
Qed.

The Equations plugin probably automates that properly, but I haven't tried.