Coq：如何产生强多态依赖类型假设

Question

我在依赖归纳方面遇到了一些问题，因为 "weak hypothesis"。

例如：

我有一个依赖的完整可折叠列表:

Inductive list (A : Type) (f : A -> A -> A) : A -> Type :=
  |Acons : forall {x x'' : A} (y' : A) (cons' : list f (f x x'')), list f (f (f x x'') y')
  |Anil : forall (x: A) (y : A), list f (f x y).

还有一个函数，该函数 return 从归纳类型列表中应用的折叠值和其他通过匹配强制计算这些值的函数。

Definition v'_list {X} {f : X -> X -> X} {y : X} (A : list f y) := y.

Fixpoint fold {A : Type} {Y : A} (z : A -> A -> A) (d' : list z Y) :=
  match d' return A with
    |Acons x y => z x (@fold _ _ z y)
    |Anil _ x y  => z x y
   end.

很明显，如果具有相同的依赖类型列表，那么函数 return 具有相同的值并证明这不应该那么难。

Theorem listFold_eq : forall {A : Type} {Y : A} (z : A -> A -> A) (d' : list z Y), fold d' = v'_list d'.
intros.
generalize dependent Y.
dependent induction d'.
(.. so ..)
Qed.

我的问题是相关定义为我生成了一个弱假设。

因为我在使用依赖定义的大多数证明中都有类似的东西，所以上面的证明问题：

A : Type
z : A -> A -> A
x, x'', y' : A
d' : list z (z x x'')
IHd' : fold d' = v'_list d'
______________________________________(1/2)
fold (Acons y' d') = v'_list (Acons y' d')

即使我在 (z x x'') 中有一个多态定义，我也不能在我的目标中应用 IHd'。

我的问题是是否有办法定义更多 "powerful" 和多态归纳，而不是疯狂地重写有时让我苦恼的术语。

Answer 1

如果你这样做

simpl.
unfold v'_list.

可以看到差不多大功告成了（重写即可结束），但是z的参数顺序错了，因为list和fold不'同意弃牌的方式。

顺便说一句，Acons 可以量化单个 x，将 f x x'' 替换为 x。

Coq：如何产生强多态依赖类型假设

Coq: How to produce a strong polymorphic dependent type hypothesis

proof

coq

induction

proof-of-correctness

coq-tactic