coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq tatic help

From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] coq tatic help
Date: Tue, 19 Mar 2019 01:17:45 +1100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f41.google.com
Ironport-data: A9a23:Rfdpy6Igbl2MzvblFE//H55yUtVLeRNe4xZyt3CvOczKTyvbOAc1So pxb03L0HSaGd6GD18aEfMd5EVI3TqD1mAxV7Qlv5bhzn5p2LTOdtUN+ugJKWd0VvZy7osapx XwVLp+0+uHl7mBUxGJYQTKEPyLPZmxZI7gNFwyYrJpe7bkeQq17KL6rbYX/r3GTW8Eb1oPwA 3plTK68zMDVmJ2L4hsUgVmJMdnUXR/ZOH0Tzr5KUkM0yijMzKzlGsqhHNxfE3vttsh5cTZB5 ZE/RDqwAnWpVE/MF3NHFaPYpynoVkipSRlMB5c8CLQ/UAjhcYgo11kW/Awoo2h9do1bLYj2U 9eByzyapx429agMuOFoU01hnzOD5PuO7ynptZ6oEgTB5iMeGHcKf3RhDbbEcYI5yGB1czbZM Ky98plMfmDRqeQmP05otxXi8HQX12VZGotUZJw4oqQ5dD5CCFsP/pWoqS99BPhzdFCu3RO1j B5F//F3YQhb9RT9fA7MjNVzMBudiUtnOK5/9bWk06BBA6xbnF9vkoQROfJZ3Wnevmh+q6hNz +j6ZF8P8Uu8UJ2U2kfWwsmz2Y8+xOzUnBku6lOdz4NsiGGcY3NTg4WmTzw0JHoSWLAXTOHGd sMki+P9M4whehRhBKcugqtaO30yJUNaca5CMUPbGpIskWsYDyvtk54+9PGWHVgXhk79uPVLE kLvAD6V2l4R4uDPYSKdEijJKIYiM4AJpCGO9/FvDk/c+sMJJMgIlN4BkfXqRCRAO4Bk0HR/a 1YBgpYNwHAWgO68hMv3wW+JAU33Y2hxeUIZ9GvQyn6gIFSFt71jkdnUW14NlBfjrAv48wllY 61IoQKSkxnL0DhAbs352DMH4VGA9k3Pw1pWKS06F7+gdJVW1jQxTiTvvHLWsr2X2/OWIaTwT gLx8OgNfM7VA==
Ironport-phdr: 9a23:lWRAxR3WsBiHUGLvsmDT+DRfVm0co7zxezQtwd8Zse0VLPad9pjvdH bS+e9qxAeQG9mCs7Qc0qL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFc VGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHOfwlEniaxba5vJx iqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UK dXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4K dxUBLnhykHODw5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo68ap YPD+kfMuZDr4n2ukcOrRqwBAa2HuPvyyJDi3jz3a0n0OQuDxrG3Aw8H9IPvnXbts/1NKYIXe C0zanIzCnDb/ZN1Dfy7YjHaBEhofWWUb1sdsrRzFAiGgXYhVuTsYzoJy2Z2vgJvmSB7OdtVf ijh3M5pwxyuDSiydogh4/UjYwP0F/E7z92wIMtKN24VkF7ZdmkHYNVty6ANot2RtouQm9tuC on07EGt5G2cDUQxJQowB7fbPOHc4yW7R75SOmRJjJ4iGpkeLK5mRmy7VCtxvPgWsSwylpHrS pInsPRunwT1BHf8MeKRuZl8kekwzmP1gTT6u9eIUAzkKrWM5shwqMzlpUNqkTDHjP2mET4ja CMbEUk+/Kk6+XmYrXnup+cMpR5ig77Mqs0m8y/Bf40PRQJX2ie4ei8zqHs/VXlQLVWif07ir XWsJfDJcgCuqG5BxJV3Z045hakDzam1cwYkmMdIFJEfhKHlYnpNEvULPD2F/fsy2irxTxs3r XNOqDrKpTLNHnK1rn7Lphn7EsJzRcwwMtfr45VFbgbIbqnX1LyucfYEh4mOha1hefmCcl4/o wbUGOLRKSeNfWB4hez+uszLrzUN8cuszHnJq19vqO8vToCgVYYOJKR894XZXS/RKk0JkyYZT /zh45EHztT+AU5S+PuhRuJVjsBPy/jDZJ53SkyDcedNamGQ4mshLKb2yLiR89ZY2lHDhaHFn K6LtzYCcdJUzqbJ4paqhJBTaKoEtZz2hSntQu8wL1ifLLZ

You have already introduced it, so try

unfold ea_in_range in H. See the difference:

unfold ea_in_range.  intros.

and yours is

intros.
unfold ea_in_range.

- Mukesh

On Tue, 19 Mar 2019 at 12:41 am, 朱立平 <zlponline AT 163.com> wrote:

Thanks Maximilian.

But after apply tatics:

intros.
unfold ea_in_range.

It seems unfold does nothing.

1 subgoals
a : nat
H : ea_in_range a
______________________________________(1/1)
a + 3 < 6

Can you proove the goal for me?


At 2019-03-17 20:01:19, "Maximilian Wuttke" <s8mawutt AT stud.uni-saarland.de> wrote:
>`omega` doesn't unfold definitions.
>You need to unfold `ea_in_range` first.
>
>```
>Lemma test2:
>  forall a, ea_in_range a -> a+3<6.
>Proof.
>  unfold ea_in_range.
>  intros.
>  omega.
>Qed.
>```
>
>
>On 17/03/2019 12:27, 朱立平 wrote:
>> Since omega works in the following proof.
>> Require Import ZArith.
>> 
>> /Lemma test1:/
>> /  forall a, a<3 -> a+3<6./
>> /Proof./
>> /intros./
>> /omega./
>> /Qed./
>> 
>> I wonder why error occurs at this:
>> /Definition ea_in_range (ea:nat) : Prop := ea < 3./
>> 
>> /Lemma test2:/
>> /  forall a, ea_in_range a -> a+3<6./
>> /Proof./
>> /intros./
>> /omega.  /
>> Error: Omega can't solve this system
>> 
>> Best Regards,
>> Julian
>> 
>> 
>>  
>> 
>

[Coq-Club] coq tatic help, 朱立平, 03/17/2019
- Re: [Coq-Club] coq tatic help, Maximilian Wuttke, 03/17/2019
  - Re:[Coq-Club] coq tatic help, 朱立平, 03/18/2019
    - Re: [Coq-Club] coq tatic help, Gaëtan Gilbert, 03/18/2019
      - Re: [Coq-Club] coq tatic help, Zhu, 03/20/2019
    - Re: [Coq-Club] coq tatic help, mukesh tiwari, 03/18/2019