我一直有依赖诱导的一些问题,因为“弱假设”。
例如 :
我有一个依赖完整的可折叠列表:
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).
还有一个函数,它从归纳类型列表和其他函数返回应用的折叠值,强制通过匹配计算这些值。
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.
显然,如果具有相同的依赖类型列表,则该函数返回相同的值,并证明这不应该如此困难。
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'。
我的问题是,如果有一种方法来定义更多“强大”和多态感应,而不是疯狂重写有时困扰我的术语。
如果你这样做
simpl.
unfold v'_list.
你可以看到你几乎就在那里(你可以完成重写),但z
的参数是错误的顺序,因为list
和fold
不同意折叠的方式。
在一个不相关的说明,Acons
可以量化单个x
,用f x x''
取代x
。