How can I prove following lemma in Coq?

Question

I am trying to write a Coq poof for the following lemma:

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.

I'm unable to simplify (M.add k k m) part.

What is M? Can you add necessary imports? Also, what have you tried doing and at what point are you unable to simplify (M.add k k m). It would be helpful if you could list all tactics used up to the point that you get stuck. — Matt
You shouldn't be able to look into the contents of stuff in a module, you should only use the lemmas defined in the module to reason about the abstract data type M. In this case it is sufficient to use the lemmas M.add_1, M.add_2, M.find_1, M.find_2. — larsr

Yves Yves · Accepted Answer · 2017-09-23T12:23:49

First, there is no recursive call in cc, so you should make this definition a plain definition (using keyword Definition instead of Fixpoint).

Second, if you want to reason about the behavior of M.find and M.add, you should look at the theorems stating things about these functions: theorems M.find_2, M.add_2, M.E.eq_dec, and M.add_1 will be useful (I found these lemmas by using the Search command). So start by unfolding cc, then reason by cases on the value of (M.find n m), then use these theorems to progress logically about the functions occurring in your statements. Please note that function M.MapsTo plays a key role in this problem.

I would rather not give you the solution because it looks like an elementary exercise in reasoning about tables.

How can I prove following lemma in Coq?

1 Answers