我之前提出过一个问题,但我认为这个问题很难正式化,所以......我在这个具体定义中面临一些问题来证明它们的属性:
我有一个列表的定义:
Inductive list (A : Type) (f : A -> A -> A) : A -> Type :=
|Acons : forall {x : A} (y' : A) (cons' : list f x), list f (f x y')
|Anil : forall (x: A) (y : A), list f (f x y).
这是定义:
Definition t_list (T : Type) := (T -> T -> T) -> T -> T.
Definition nil {A : Type} (f : A -> A -> A) (d : A) := d.
Definition cons {A : Type} (v' : A) (c_cons : t_list _) (f : A -> A -> A) (v'' : A) :=
f (c_cons f v'') v'.
Fixpoint list_correspodence (A : Type) (v' : A) (z : A -> A -> A) (xs : list func v'):=
let fix curry_list {y : A} {z' : A -> A -> A} (l : list z' y) :=
match l with
|Acons x y => cons x (curry_list y)
|Anil _ _ y => cons y nil
end in (@curry_list _ _ xs) z (let fix minimal_case {y' : A} {functor : A -> A -> A} (a : list functor y') {struct a} :=
match a with
|Acons x y => minimal_case y
|Anil _ x _ => x
end in minimal_case xs).
Theorem z_next_list_coorresp : forall {A} (z : A -> A -> A) (x y' : A) (x' : list z x), z (list_correspodence x') y' = list_correspodence (Acons y' x').
intros.
generalize (Acons y' x').
intros.
unfold list_correspodence.
(*reflexivity should works ?*)
Qed.
z_next_list_coorres实际上是一个需要在另一个理论中证明目标的引理(v'_list x =(list_correspodence x))。
我一直在尝试使用一些有限的范围来证明list_correspodence并且运行良好,似乎定义相同,但对于coq没有。
在这里list_correspondence
是一个虚假的Fixpoint
(即fix
)(它没有进行递归调用),这会妨碍减少。
您可以通过破坏其减少的参数来强制减少fix
:
destruct x'.
- reflexivity.
- reflexivity.
或者你可以首先避免使用Fixpoint
。请改用Definition
。
你可能会遇到一个带有隐式参数的奇怪错误,这可以通过添加类型签名(如下所示)来避免,或者通过不隐式标记本地函数curry_list
的参数来避免:
Definition list_correspodence (A : Type) (v' : A) (func : A -> A -> A) (xs : list func v')
: A :=
(* ^ add this *)