Require Import FMapAVL.
Require Import OrderedTypeEx.
Module M := FMapAVL.Make(Nat_as_OT).
Fixpoint cc (n: nat) (c: M.t nat):bool :=
match M.find n c with
| None => false
| Some e => 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.
Proof.
intros.
inversion H.
Environment before calling inversion H:
1 subgoals
n : nat
k : nat
m : M.t nat
H : cc n m = true
______________________________________(1/1)
cc n (M.add k k m) = true
Based on my understanding of inversion tactic, using tactic inversion H, should be able to predict M.find n m = Some e. But it just duplicates H.
Can someone please help me with how Coq is interpreting things here?
Inversion works when the hypothesis' main predicate is an inductive predicate. Here the main predicate of hypothesis H is an equality, and it happens that deep inside equality is represented by an inductive predicate. So inversion think it can work.
Intuitively, inversion tries to help you reason on what constructor could have been used, and this reasoning is made by adding equality statements that correspond to the constraints that have to be satisfied when this constructor is used to prove the hypothesis.
In your case, equality is represented by an inductive definition with only one constructor. So inversion looks at what the constraints for using this constructor are: the two members of the equality should be the same. So inversion adds a new equality stating that the two sides of the equality should be the same. This is why you see this duplication of the hypothesis.
It just happens that inversion is not the right tactic to use here.
In a previous answer to one of your questions, I wrote that you should not use Fixpoint to define the function cc, because this function is not recursive. Please follow my advise and write
Definition cc (n: nat) (c: M.t nat):bool :=
match M.find n c with
| None => false
| Some e => true
end.
This will make the rest of the proofs easier (we can also solve your problem with cc defined using Fixpoint but it adds unnecessary complications). My answer to your question now supposes that you did follow this
piece of advice. Here is how to progress about your proof.
Proof.
intros n k m H; unfold cc in H.
At this point your hypothesis H contains an equality between a pattern matching statement and true. What you want is to study the two possible computations of this match statement, by performing the same case analysis in your proof. Here is how to do it.
case_eq (M.find n m); [intros v Hfind | intros Hfind].
After this, you will have two goals. One has H : match ... with ... end = true and Hfind : M.find n m = Some v, the other has H : match M.find n m with ... end = true and Hfind : M.find n m = None. Using Hfind to rewrite in H you will change the hypothesis into H : false = true, that will be solvable using discriminate. Keep this in mind for later.
For the first goal, you should be able to progress again by unfold cc.
Now what is the value of M.find n (M.add k k m)? If n is k this value is Some k. If n is different from k the value of M.find n (M.add k k m) is the same as the value of M.find n m. We already gave a name to this value, this name is v and the hypothesis Hfind says so.
To produce the case analysis on whether n is equal to k I suggest you write destruct (M.E.eq_dec k n) as [kn | knn].
So you will have a first goal with hypothesis kn : k = n. In that case I suggest you prove an intermediate fact by typing the following command.
assert (step : M.find n (M.add k k m) = Some k).
This you should be able to prove using M.find_1, M.add_1.
Once you are finished with this proof, rewrite with step and then conclude.
Then you will have a second goal with hypothesis knn : k <> n, for this one you have to prove a different intermediate statement, which you prove by using again M.find_1, but then you use M.add_2 and M.find_2.