1

在我的证明中，我达到了一个类似于以下内容的目标：（实际类型不同（zm：StringMap.string String.string，key 和 elt 是 String.string））。在我的代码中，如果我 H: z1k <> z2k在环境中，那么它很容易，intuition congruence但如果我没有这样的假设，那么我无法证明我的目标。此外，我也无法证明v1 = v2，这有助于证明目标。请有人指导我解决此类情况。谢谢，

Parameter t : Type -> Type.
Variable key : Type.
Variable elt : Type.
Implicit Type m: t elt.
Implicit Type x y z: key.
Implicit Type e: elt.

Require String.

Record id : Type :=
build_id {
         id_v : String.string;
         id_k: key
        }.

Parameter add : key -> elt -> t elt -> t elt.
Parameter MapsTo : key -> elt -> t elt -> Prop.

Lemma MyTest: forall v1 v2 (z1k z2k zk: key) (ze z1 z2: elt) zm, 
build_id v1 z1k <> build_id v2 z2k ->
MapsTo zk ze (add z1k z1 (add z2k z2 zm)) -> 
MapsTo zk ze (add z2k z2 (add z1k z1 zm)).
Proof.
4

1 回答 1

0

是否可以在 上假设​​可判定的平等key？然后，您可以通过案例分析进一步了解记录元素是否成对相等。例如，使用 Adam Chlipala 的 CPDT 策略，我得到：

Add LoadPath "~/dev/cpdt/src".

Require String.    
Require Import CpdtTactics.

Variable key : Type.    

Record id : Type := build_id {    
  id_v : String.string;    
  id_k : key    
}.

Axiom key_dec : forall a b : key, {a = b} + {a <> b}.

Lemma unpack_build_id_ineq : forall a b x y, build_id a x <> build_id b y ->    
  (a <> b) \/ (x <> y).    
Proof.    
  intros.    
  set (H1 := String.string_dec a b).    
  set (H2 := key_dec x y).    
  crush.    
Qed.

换句话说，假设两条记录不相等，则有两种情况：要么不相等，要么id_v分量id_k不相等。希望这可以帮助。

免责声明：我是 Coq 的初学者，希望你能在这里得到更多合格的帮助，或者你也可以试试 Coq Club 邮件列表。

于 2013-02-28T13:25:10.613 回答