строки и добавить в Coq

Question

В моих доказательствах я достиг цели, похожей на следующую: (Фактические типы разные (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. 

Answer 1

Можно ли принять разрешимое равенство на key? Затем вы можете продолжить анализ случаев, если элементы записи попарно равны или нет. Например, используя CPDT тактику Адам Chlipala, я получаю это:

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.