Можно ли доказать эквивалент Forall_inv для разнородных списков в Coq?

Индуктивы, индексированные индексированными типами, приводят к такого рода затруднениям.

В качестве альтернативы рассмотрите возможность определения hForall как Fixpoint. Тогда лемма об обращении следует, просто разворачивая определение.

  Section hForall'.

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

    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.
    Proof.
      intros []; auto.
    Qed.

  End hForall'.

Приложение

В основном в образовательных целях, вот несколько способов доказать эту лемму об обращении для исходного индуктивного определения hForall (начиная с более простого в использовании).

Одним из решений является тактика dependent destruction, которая также автоматически обрабатывает неоднородные равенства, в отличие от destruct. Импортируется из модуля Program:

    Import Program.

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

(Небольшая) загвоздка в том, что он использует некоторые аксиомы о гетерогенном равенстве:

    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
*)

С немного большим знанием того, как destruct работает / зависимым сопоставлением с образцом, вот доказательство без аксиом.

Есть несколько подробных объяснений зависимого сопоставления с образцом в CPDT, но вкратце проблема заключается в том, что когда мы делаем _11 _ / _ 12_ на hForall (HCons x hl), индекс HCons x hl обобщается до разделения регистра, поэтому вы получаете бессмысленный случай, когда он заменяется на HNil, а второй случай с другим индексом HCons x0 hl0 и хорошим способом запомнить (неоднородное) равенство в этом обобщении является проблемой исследовательского уровня. Вам не нужно было бы связываться с неоднородными равенствами, если бы цель была просто переписана этими переменными, и действительно, вы можете реорганизовать цель так, чтобы она явно зависела от HCons x hl, а не от x и hl по отдельности, которые затем будут обобщены на destruct:

    Lemma hForall_inv'
          (a : A)
          (ls : list A)
          (x : B a)
          (hl : hlist ls)
      : hForall (HCons x hl) -> P a x.
    Proof.
      intros H.

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

      destruct H.
      - exact I.  (* Replace [HCons x hl] with [HNil], the goal reduces to [True]. (This is an unreachable case.) *)
      - assumption.

    (* Or, directly writing down the proof term. *)
    Restart.
      intros H.
      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).
      assumption.
    Qed.

Плагин Equations, вероятно, автоматизирует это должным образом, но я не пробовал.

Я думаю, что самый простой способ решить эту проблему - сказать Coq, что мы заботимся об этих разрушенных паттернах. В качестве альтернативы вы можете использовать тактику запоминания, но иногда она усложняет обоснование вашей теоремы.

    Lemma hForall_inv
          (a : A)
          (ls : list A)
          (x : B a)
          (hl : hlist ls)
      : hForall (HCons x hl) -> P a x.
    Proof.
      have : forall (F : forall (a : A) (ls : list A) (x : B a) (hl : hlist ls) (H : hForall (HCons x hl)), Prop), 
               (forall (a : A) (ls : list A) (x : B a) (hl : hlist ls) (H : hForall (HCons x hl)) (I : forall (a : A) (ls : list A) (x : B a) (hl : hlist ls) (f : P a x) (H : hForall (HCons x hl)), F a ls x hl H),
                   F a ls x hl H).
      intros.
      refine (match H in (hForall (HCons x hl)) return F _ _ _ _ H with 
               |hForall_nil => _
               |hForall_cons a x y z => _
             end).
      exact idProp.
      exact (I _ _ _ _ y (hForall_cons a x y z)).
      move => forall_rect. 
      elim/forall_rect; by [].
   Qed.

Наблюдение, которое я использую Type, чтобы исключить:

Inductive hForall : forall {As : list A}, hlist As -> Type :=
| 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).