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.

言い換えると、2 つのレコードが等しくない場合、2 つのケースがあります。id_vまたはid_kコンポーネントのいずれかが等しくありません。お役に立てれば。

免責事項: 私はどちらかというと Coq の初心者です。ここでより適切なヘルプが得られることを願っています。または、Coq クラブのメーリング リストを試すこともできます。

于 2013-02-28T13:25:10.613 に答える