应用程序定义失败 "unable to unify Prop with [goal]"
Applying a Program Definition fails with "unable to unify Prop with [goal]"
在 Coq 中,我使用以下方法展示了 append
在向量上的结合性:
Require Import Coq.Vectors.VectorDef Omega.
Program Definition t_app_assoc v p q r (a : t v p) (b : t v q) (c : t v r) :=
append (append a b) c = append a (append b c).
Next Obligation. omega. Qed.
我现在想在证明中应用这个等式。下面是我希望用 t_app_assoc
证明的最简单的目标。当然可以通过simpl
来证明——这只是一个例子。
Goal (append (append (nil nat) (nil _)) (nil _)
= append (nil _) (append (nil _) (nil _))).
apply t_app_assoc.
此 apply
失败:
Error: Unable to unify "Prop" with
"append (append (nil nat) (nil nat)) (nil nat) =
append (nil nat) (append (nil nat) (nil nat))".
如何申请t_app_assoc
?还是有更好的方法来定义它?我以为我需要 Program Definition
,因为简单地使用 Lemma
会导致类型错误,因为 t v (p + (q + r))
和 t v (p + q + r)
与 Coq 不同。
序言
我猜你想做的是证明向量串联是结合的,然后将这个事实用作引理。
但是您定义的 t_app_assoc
具有以下类型:
t_app_assoc
: forall (v : Type) (p q r : nat), t v p -> t v q -> t v r -> Prop
您基本上想要使用 :
而不是 :=
,如下所示。
From Coq Require Import Vector Arith.
Import VectorNotations.
Import EqNotations. (* rew notation, see below *)
Section Append.
Variable A : Type.
Variable p q r : nat.
Variables (a : t A p) (b : t A q) (c : t A r).
Fail Lemma t_app_assoc :
append (append a b) c = append a (append b c).
不幸的是,我们甚至不能使用通常的齐次等式来陈述这样的引理。
左侧有以下类型:
Check append (append a b) c : t A (p + q + r).
而右边的类型是
Check append a (append b c) : t A (p + (q + r)).
由于 t A (p + q + r)
与 t A (p + (q + r))
不同,我们不能使用 =
来说明上述引理。
让我描述一些解决此问题的方法:
rew
符号
Lemma t_app_assoc_rew :
append (append a b) c = rew (plus_assoc _ _ _) in
append a (append b c).
Admitted.
这里只是利用自然数的加法结合律将RHS的类型强制转换为t A (p + q + r)
.
要使其正常工作,需要先 Import EqNotations.
。
cast
函数
这是一个常见问题,因此 Vector
库的作者决定提供具有以下类型的 cast
函数:
cast :
forall (A : Type) (m : nat),
Vector.t A m -> forall n : nat, m = n -> Vector.t A n
让我展示一下如何使用它来证明向量的结合律。但是我们先证明下面的辅助引理:
Lemma uncast {X n} {v : Vector.t X n} e :
cast v e = v.
Proof. induction v as [|??? IH]; simpl; rewrite ?IH; reflexivity. Qed.
现在我们都准备好了:
Lemma t_app_assoc_cast (a : t A p) (b : t A q) (c : t A r) :
append (append a b) c = cast (append a (append b c)) (plus_assoc _ _ _).
Proof.
generalize (Nat.add_assoc p q r).
induction a as [|h p' a' IH]; intros e.
- now rewrite uncast.
- simpl; f_equal. apply IH.
Qed.
异构等式(a.k.a.John Major 等式)
Lemma t_app_assoc_jmeq :
append (append a b) c ~= append a (append b c).
Admitted.
End Append.
如果比较齐次相等的定义
Inductive eq (A : Type) (x : A) : A -> Prop :=
eq_refl : x = x.
以及异构相等性的定义
Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
JMeq_refl : x ~= x.
你会看到 JMeq
的 LHS 和 RHS 不必是同一类型,这就是为什么 t_app_assoc_jmeq
的语句看起来比前面的语句简单一些。
向量的其他方法
参见例如
和 this one;
我也找到 this answer
也很有用。
在 Coq 中,我使用以下方法展示了 append
在向量上的结合性:
Require Import Coq.Vectors.VectorDef Omega.
Program Definition t_app_assoc v p q r (a : t v p) (b : t v q) (c : t v r) :=
append (append a b) c = append a (append b c).
Next Obligation. omega. Qed.
我现在想在证明中应用这个等式。下面是我希望用 t_app_assoc
证明的最简单的目标。当然可以通过simpl
来证明——这只是一个例子。
Goal (append (append (nil nat) (nil _)) (nil _)
= append (nil _) (append (nil _) (nil _))).
apply t_app_assoc.
此 apply
失败:
Error: Unable to unify "Prop" with
"append (append (nil nat) (nil nat)) (nil nat) =
append (nil nat) (append (nil nat) (nil nat))".
如何申请t_app_assoc
?还是有更好的方法来定义它?我以为我需要 Program Definition
,因为简单地使用 Lemma
会导致类型错误,因为 t v (p + (q + r))
和 t v (p + q + r)
与 Coq 不同。
序言
我猜你想做的是证明向量串联是结合的,然后将这个事实用作引理。
但是您定义的 t_app_assoc
具有以下类型:
t_app_assoc
: forall (v : Type) (p q r : nat), t v p -> t v q -> t v r -> Prop
您基本上想要使用 :
而不是 :=
,如下所示。
From Coq Require Import Vector Arith.
Import VectorNotations.
Import EqNotations. (* rew notation, see below *)
Section Append.
Variable A : Type.
Variable p q r : nat.
Variables (a : t A p) (b : t A q) (c : t A r).
Fail Lemma t_app_assoc :
append (append a b) c = append a (append b c).
不幸的是,我们甚至不能使用通常的齐次等式来陈述这样的引理。
左侧有以下类型:
Check append (append a b) c : t A (p + q + r).
而右边的类型是
Check append a (append b c) : t A (p + (q + r)).
由于 t A (p + q + r)
与 t A (p + (q + r))
不同,我们不能使用 =
来说明上述引理。
让我描述一些解决此问题的方法:
rew
符号
Lemma t_app_assoc_rew :
append (append a b) c = rew (plus_assoc _ _ _) in
append a (append b c).
Admitted.
这里只是利用自然数的加法结合律将RHS的类型强制转换为t A (p + q + r)
.
要使其正常工作,需要先 Import EqNotations.
。
cast
函数
这是一个常见问题,因此 Vector
库的作者决定提供具有以下类型的 cast
函数:
cast :
forall (A : Type) (m : nat),
Vector.t A m -> forall n : nat, m = n -> Vector.t A n
让我展示一下如何使用它来证明向量的结合律。但是我们先证明下面的辅助引理:
Lemma uncast {X n} {v : Vector.t X n} e :
cast v e = v.
Proof. induction v as [|??? IH]; simpl; rewrite ?IH; reflexivity. Qed.
现在我们都准备好了:
Lemma t_app_assoc_cast (a : t A p) (b : t A q) (c : t A r) :
append (append a b) c = cast (append a (append b c)) (plus_assoc _ _ _).
Proof.
generalize (Nat.add_assoc p q r).
induction a as [|h p' a' IH]; intros e.
- now rewrite uncast.
- simpl; f_equal. apply IH.
Qed.
异构等式(a.k.a.John Major 等式)
Lemma t_app_assoc_jmeq :
append (append a b) c ~= append a (append b c).
Admitted.
End Append.
如果比较齐次相等的定义
Inductive eq (A : Type) (x : A) : A -> Prop :=
eq_refl : x = x.
以及异构相等性的定义
Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
JMeq_refl : x ~= x.
你会看到 JMeq
的 LHS 和 RHS 不必是同一类型,这就是为什么 t_app_assoc_jmeq
的语句看起来比前面的语句简单一些。
向量的其他方法
参见例如