私は、次の補題のためにパッと消えるコックを記述しようとしています:Coqで次の補題をどのように証明できますか?
Require Export Coq.Structures.OrderedTypeEx.
Require Import FMapAVL.
Module M := FMapAVL.Make(Nat_as_OT).
Fixpoint cc (n: nat) (c: M.t nat):bool :=
match M.find n c with
| None => false
| _ => true
end.
Lemma l: forall (n: nat) (k:nat) (m: M.t nat), cc n m = true -> cc n (M.add k k m) = true.
私は(M.add k k m)
一部を簡素化することができませんでしだ。
「M」とは何ですか?必要な輸入品を追加できますか?また、何をやって何をしようとしたのですか?あなたは '(M.add k k m)'を単純化できません。あなたが立ち往生した時点までに使用されたすべての戦術を挙げることができれば役に立ちます。 – Matt
あなたはモジュール内のものの内容を調べるべきではありません。モジュールで定義されている補題を使って、抽象データ型Mについて推論する必要があります。この場合、補題 'Mを使うだけで十分です。 「add_1」、「M.add_2」、「M.find_1」、「M.find_2」。 – larsr
補題を証明する1つの方法については、[here](https://gist.github.com/anonymous/b8173a55317b5cfc4450a1a1e172f01b)を参照してください。 – larsr