coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Ramkumar Ramachandra <artagnon AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] [NEWBIE] Applying Nat.eq_dec
Date: Thu, 4 Jan 2018 18:47:46 -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-yb0-f174.google.com
Ironport-phdr: 9a23:MQzWKRBi64ywclsHI+i/UyQJP3N1i/DPJgcQr6AfoPdwSPv7oMbcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNzA3/mLKhMJukK1WuwiuqwBlzoPOfI2ZKPhzc6XAdt0aX2pBWcNRWjRdDIymaosPDPcBPeNCoInnulAAsQGxBQy2C+zzyj9HnHn20rAg0+s7DArL2xYvH8gSsHvOo9X1MqASUeauwanHyDXMdfJW2TPn5IfUdRAhpOiBULRtesTS0UkiDx3JgkmUpID/PD6Y1v4Bv3aG4+duT+6jlmwqpg53rzOy3MkjkJPJiZgQyl3c9SV23oI1JdqgRU5+e9GkEZ9QuziaNoRtXs8uWm9otDs4x7AJo5K7cy8KyJMoxx7bdfOLaZSH4hXmVOqJIDd4gmxqeK6nihqs7UStzvfwW8q03VpQsCZJj9fBumoQ2xHR5cWLUv598V2g2TaL2QDT8OZEIUUsmKXBMZ4h3qQ/lpUVsUTEGC/7g0r2jKqMeUUl/uik8fjoYrLjppOELY97lhn+Mrgymsy4Gek3Lg8OX3GC9eug0L3j4Fb2Ta5Rjvw2l6nZqIrVKd4apq6/GQ9V05ws5wyxDze8g5wkmiwMK0sAcxaahaDoPUvPKbb2F6SRmVOpxQ1iwvPbO7T7Sq/EK3HIkL7ncax0oxpV0hY6wtZY4bpbD7gAJLT4XUqn54+QNQMwLwHhm7WvM956zI5LAW8=

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

[Coq-Club] [NEWBIE] Applying Nat.eq_dec, Ramkumar Ramachandra, 01/05/2018
- Re: [Coq-Club] [NEWBIE] Applying Nat.eq_dec, Ramkumar Ramachandra, 01/05/2018
  - Re: [Coq-Club] [NEWBIE] Applying Nat.eq_dec, Yao Li, 01/05/2018
    - Re: [Coq-Club] [NEWBIE] Applying Nat.eq_dec, Ramkumar Ramachandra, 01/06/2018
      - Re: [Coq-Club] [NEWBIE] Applying Nat.eq_dec, Yao Li, 01/06/2018
- Re: [Coq-Club] [NEWBIE] Applying Nat.eq_dec, ikdc, 01/07/2018