The Coq mailing list

[Yao Li <liyao AT seas.upenn.edu>]

I think FMapFacts contains something you need?

Best,

Yao

On 5 Jan 2018, at 6:13 PM, Ramkumar Ramachandra <artagnon AT gmail.com> wrote:

Thanks much!

I have a more general question about proving engineering facts about Maps. Stuff like the one I showed above, or even this other place where I got stuck:

Lemma mapElements_add : forall (n : nat) (m : registration),

M.elements (elt := registration) (M.add n m [| |]) = (n |-> m) :: nil.

Proof.

intros.

unfold M.elements; unfold M.Raw.elements.

• n: nat
• m: registration

• 1/1M.Raw.elements_aux nil (M.this (M.add n m [| |])) = (n |-> m) :: nil

... am I doing something wrong, because the Standard Library doesn't seem to have anything that I can use? Must I prove all these elementary properties of Maps before I proceed to use them in larger proofs?

Thanks.

Ram

On Fri, Jan 5, 2018 at 1:59 PM, Yao Li <liyao AT seas.upenn.edu> wrote:

In your first proof: your goal is falsehood, but you also have a contradiction in your hypothesis. The “contradiction” tactic should be able to solve the goal.

Your second proof seems to be on the wrong track. I guess what you are trying to say is that [a] always equals to [a], but that is not what [trivialEq] is actually saying...

A general lemma that may be useful to you is:

Lemma eq_dec_refl_branch {A} : forall a (b c : A),

    (if Nat.eq_dec a a then b else c) = b.
Proof. intros. destruct (Nat.eq_dec a a); auto; contradiction. Qed.

Best,

Yao

On 5 Jan 2018, at 4:12 PM, Ramkumar Ramachandra <artagnon AT gmail.com> wrote:

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