coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: ikdc <ikdc AT mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] [NEWBIE] Applying Nat.eq_dec
Date: Sun, 07 Jan 2018 16:26:00 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ikdc AT mit.edu; spf=Pass smtp.mailfrom=ikdc AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-7.mit.edu
Importance: Normal
Ironport-phdr: 9a23:S21KKxwZ6rMgRxbXCy+O+j09IxM/srCxBDY+r6Qd1e8RIJqq85mqBkHD//Il1AaPAd2Craocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HObwlSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHmlSkJNDw2/mHJhMNzlqxUoR2uqABwzYPPYIGaL+Bzcr/Bcd8GR2dMWNtaWSxbAoO7aosCF+sBPeVFoIbhulADqhq+BQqxC+zz0TJIg3723bEg3+s/DA7GwRUtEtQTu3rXtNX4LLoeXOOvwKTK1znObvBb1S3z5YXJahwtvPKBUah0fMbL10UiFBnJgkiNpYHjIjibzP4Cs3KB4OplTe+vi3AoqwV2ojW328gsj4jIipsQyl/e9CV5xJ01KsOkR0Jiet6rDIFftyecN4RoWMMuWmNltDw/yr0HpZ63ZjYFx4k6xxLHavyHdZaH4g77WeqMIjp0nnBodKi+ihux60StxOzxWtGx0FlQrypFltfMtmoK1xzW8sWHS/h98Vq91juU0gDT6/1ELVoqmqXGNp4t2qQwmYYLsUTfAi/2n137g7ORdkU94+Sn9+DnYqj9qZKHLI91igT+Mrw0lcClAOQ4NBIOX2mB9uim2r3j5x6xfLIfhfov16LdrZryJMIBp6f/DRUG/Jwk7kO+DDutmIAZnnUMBFdEZFSKg5W/aAKGG+zxEfrq2wfkqzxs3f2TZrA=

Your assumption a <> a is a contradiction, so you should be able to prove your goal.

On Jan 4, 2018 21:47, 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

[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