The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

Now I have an additional Lemma which I'm not able to apply, due to "Cannot change D, it is used in conclusion". 

Lemma trivialEq : forall a : M.key, {a = a} + {a <> a} -> True.

Proof.

trivial.

Qed.

Lemma keyInMap : forall a b, M.find (elt := nat) a [a |-> b] = Some b.

Proof.

intros.

unfold update. unfold fst. unfold snd.

rewrite F.add_o.

unfold Nat_as_OT.eq_dec.

remember (Nat.eq_dec a a) as D.

apply trivialEq in D.

My hypothesis and goals window looks like this in the last step:

• a: M.key
• b: nat
• D: {a = a} + {a <> a}
• HeqD: D = Nat.eq_dec a a

• 1/1(if D then Some b else M.find (elt:=nat) a [ ]) = Some b

Why do I get the error? I have all the right types for unification.

Thanks.

Ram

On Thu, Jan 4, 2018 at 6:47 PM, Ramkumar Ramachandra <artagnon AT gmail.com> wrote:

Hi folks,

I'm trying to use Coq to prove that M.find (referring to FMapAVL) finds an element that exists in the map. Here's my progress so far:

Lemma keyInMap : forall a b, M.find (elt := nat) a [a |-> b] = Some b.

Proof.

intros.

unfold update. unfold fst. unfold snd.

rewrite F.add_o.

unfold Nat_as_OT.eq_dec.

remember (Nat.eq_dec a a) as D.

induction D.

reflexivity.

rewrite F.empty_o.

Qed.

Somehow, I get stuck with this to prove:

• a: M.key
• b: nat
• b0: a <> a
• HeqD: right b0 = Nat.eq_dec a a

• 1/1None = Some b

Which is a falsehood, so I think I did the wrong thing by using "induction D". To eliminate one of the cases of the `if`, I will need to apply `Nat.eq_dec`, and I'm unable to apply it for some strange reason.

Some pointers would be appreciated.

Thanks.

Ram