Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] [NEWBIE] Applying Nat.eq_dec

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [NEWBIE] Applying Nat.eq_dec


Chronological Thread 
  • From: Ramkumar Ramachandra <artagnon AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] [NEWBIE] Applying Nat.eq_dec
  • Date: Fri, 5 Jan 2018 15:13:20 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=artagnon AT gmail.com; spf=Pass smtp.mailfrom=artagnon AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f178.google.com
  • Ironport-phdr: 9a23:gnR6RxXSAjXLrRSFctoyBM2K0YnV8LGtZVwlr6E/grcLSJyIuqrYYxWGt8tkgFKBZ4jH8fUM07OQ7/i5HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9vIBmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7VhMx+jKxVrhG8qRJh34HZe5uaOOZkc67HYd8WWWhMU8BMXCJBGIO8aI4PAvIdM+lCqon9pEYOrR6kCgm2Gejh1iVHhnrs0qIm0+QuCwfG0xE6H90UrX/Zq8/6NL0OUe+vw6nIyzLDb/VN1Dfy7YjHaBEhofWWUb1sdsrRzFAiGgXYhVuTsYzoJy2Z2vgJvmSB7OdtVfijh3Mmpg1suDSj28Uhh4rPi4kI0F7L7z95z5wwJdCgSE50f9qkEJxIuiGfLYR2Q8ciT3houSc01rEKoJC7cDUIxZkk3RLfZPuHc4+H4hLnSumdOyt3hHVgeL6nhhay91avyvHkW8WqzFpHqjBJn9rMu3wXyhDe69WLRuFg8kqj2juDzwXT5ftFIUAwm6rbMZkhwrsom5UJq0TDAjX5mErwjK+RcEUp4eeo6+H9bbXnop+QLZN7igb7Mqg2gMywHfw4MhQSX2ic4emzyLrj/VTgTLpWiv02j7LWvYvBJcUbo665GxVa3pwi6xa5FTem0c4XkWMJLFJfK1q7iN3iPEiLK/TlB9++hU6tmXFl3aPoJLrkV6/EK3velb77NYx07kdXyAM1wcpWr8ZdEK0IL/T0XGf+sdXZClkyNAnikLWvM8l0yo5LATHHOaSeKq6H6VI=

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






Archive powered by MHonArc 2.6.18.

Top of Page