coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq tatic help

From: Zhu <zlponline AT 163.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] coq tatic help
Date: Wed, 20 Mar 2019 12:06:34 +0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=zlponline AT 163.com; spf=Pass smtp.mailfrom=zlponline AT 163.com; spf=None smtp.helo=postmaster AT m12-14.163.com
Ironport-phdr: 9a23:q9r55RBRWxW2gT6T3E81UyQJP3N1i/DPJgcQr6AfoPdwSPr8ocbcNUDSrc9gkEXOFd2Cra4d06yI7uu+ByQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagfb9+NhS7oAXeusQXgIZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9Rwgq1HrxyuqBJxzZPXboGbNvVwYKTTfdIBSGpdR8ZRUjBNAoOgY4YNCecKIOZWr5P6p1sLtRaxBgmsBP7ywTJPh3722bU60+MnEQHC3QwgGcwBvW/JoNj0OqoeS/y6zK7NzTjaaf5dxDTz6JDQfxw/v/2AQah8fdfSxEUyDQ/Jk0ucpZb4Mz6azugBrnWX4uh6We6yhWMqqht9rzuuy8s2ioTEiYQYwU3e+ypj2oY6P9i4RVZ7YdG6FJtQsDmXN45rTs88Wm1kpSk3xqcbtZO6ciUG0ogoxxnaa/CfcoiI5AzsVPqJLDtmmn5pZKiziwux/ES90OHwS9e43ExXoidKitXMs2oC1x3X6siJUPt9+UKh1C6O1gDX8uFEJkY0la7aK54n3LE9jYcfvEXNEyPshEr2i6qWel0++ue08+TnfqnmppiEOoBojQH+K70ildC7AeQlKQcDRHOb+OS51L3750L1WrRKjvsskqnYqp/WP8obprTqSzNSh40k8lO0Cyqs+NUeh3gOalxfKzydiI28CVHTaKTqCe+4hVCtljpDnq6deLbmB8OefTD4jL79cOMluAZnww0pwIUHvsMGOvQ6OPv2H3TJmpndBx49PRazxre1UYsmkIgZXDDWW/PLAObpqVaNo9kXDayUfoZE6m+jcL4u4Pu81SZky29YRrGg2N4sUF79HvliJBzHM3+12JJYTSFT4FF4R+vv2gWP

Thank you.

> 在 2019年3月18日，21:42，Gaëtan Gilbert
> <gaetan.gilbert AT skyskimmer.net>
> 写道：
>
> Try "unfold ea_in_range in H"
>
> Gaëtan Gilbert
>
>> On 18/03/2019 14:40, 朱立平 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