串地图和勒柯克

Question

加在我的证据，我达到了目标，寻找类似以下内容：（实际的类型是不同的（ZM：StringMap.string String.string，关键和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. 

Answer 1

有没有可能在key上承担可判决的等同性？然后，您可以通过案例分析进一步了解记录元素是否相等。例如，使用亚当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成分是不相等的。希望这可以帮助。

免责声明：我宁愿在勒柯克初学者，我希望你得到更多的合格帮助在这里，或者你也可以尝试勒柯克俱乐部的邮件列表。