Coqで次の補題をどのように証明できますか？

Question

私は、次の補題のためにパッと消えるコックを記述しようとしています：

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)一部を簡素化することができませんでしだ。

Answer 1

最初にccに再帰呼び出しがないので、この定義を平文で定義する必要があります（FixpointではなくDefinitionを使用）。

第二には、あなたがM.findとM.addの行動について推論したい場合、あなたは これらの関数についての事を述べる定理をご覧ください： M.find_2、M.add_2、M.E.eq_decを定理、そしてM.add_1は有用であろう（私はこれらの補題を見つけましたSearchコマンドを使用して）。したがって、ccを展開してから、（M.find n m）の値で理由を推論してから、これらの 定理を使用して、ステートメントで発生する関数について論理的に進んでください。この問題では、機能M.MapsToが重要な役割を果たすことに注意してください。

テーブルについての推論では初歩的な演習のように見えるので、私はむしろあなたに解答を与えません。