coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re:[Coq-Club] coq tatic help

From: 朱立平 <zlponline AT 163.com>
To: coq-club AT inria.fr
Subject: Re:[Coq-Club] coq tatic help
Date: Mon, 18 Mar 2019 21:40:36 +0800 (CST)
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 m13-134.163.com
Ironport-data: A9a23:ArPqn6u2RVhaI0unRNllGpVypOfnOphVZqKwV/efNrXauYHJ1xXLvW +MZoIHD06BiMWHgqK9dqnvJlanpTnBWXHBZ+0pAVIscDKmIb8AC8uWAWEyYxItbL5sJyT7Zt 32XlXuXcmBgJQCrYQD2LD0eCC21K2L44yIDH2u75QShBc+eVQ+J2bYtuE6rHvx/tAWEKr92Q X8z1YRU9OhtQ7TY1tNySq3Rbrv5zgWoTdlMSH9STfhODyYi2lerYtNi2W4W2MU3Q1mQ9MB3m hWcEKNojHxVgeKRlRV/hDHhGmy3N5M0XxevvEXVeyyTDaDyfU4wwBAhBDmoXHa8bBw72nzzH /BTJ4LYMiPp4W3y2HdBB4AO2vqWwoLwgdwy6Wz1BhFItXI5q8wNqBqCuEOaa+iZJhjOUGSH0 P/m3lfOiQFuHKkjRuOAptuY6fHwYvjgz38ZPQVW8AB5QDd5gDr4PwjpEAWbSRPmVwpZiv2Q+ k085q/rG/vTFcfJiU4e/mftmYespkzTRLAUSzvdb69Oa7Dj0/TqbSHwvG1REVsevHvWYg9rd zfufep5ZfUBoQfVHMoWi0ueRhFvelQw3c+1lXe20l1TD5sfq7jZi9JkJi63gh37pVdfP0Hzd idMxOPi+Uh7o1Oif4xyYvpl9SI/GpnqVio02Tuz9CMd1fR7rutl5Y5ynzBX2I8rzKq/Ah1Za ASGchZEG15I7+L/qkOD6mrC+02QvtTs4X7567FgezupEf97+WQTLJ3uBhvEp+KLva7jK1zp2 vOchw6lWXcXPOkWvSVB1xTIxFwx5ztaPGWyvkSbGXfueb87epTR19bIbstijSlvsnyf1OiIe nvdKO+sa2V2nKaa+JvUVNKDH/YeS3SjT84Clu0nvXMI+7HviuSni6XWatubBa1f5VO6Fplpx dUR285jA==
Ironport-phdr: 9a23:gjJJFxZXzGMPtsihi8ZjKJ//LSx+4OfEezUN459isYplN5qZocS4bn LW6fgltlLVR4KTs6sC17OO9fi5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7Fs kRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCehbb9oMB m6sBjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3Tb pDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8q xlSgLniD0fOj44/m/ZitJ+gr9BrhympRN/zZLbb46WOvdlZKzRYckXSnFbU8pNSyJMBJ63YY sVD+oGOOZVt5H7oEYKqBi5HAypBP7kxzhJh3/yxa061OIhEQXH3AwmAd0Dq2nYodT7OasITe +1y6zIwCzFYvhL2jn98JDFfg4/rf2QR758bMncxVQ1Gw/YgFics5HpMj2a2+gVrmSX8vdsWf iyh2MksQ18rTqiyt0yhoXXho8YzE3P+z9jz4YvP9K4TVZ2Yd66H5tUsCGXL452Tt4sTm1xpS o3xLILtYSmcCULxpkr3QLQa/uCc4SQ4xLjUvieIStgiX57Zr6zmwy+/VWjx+HhTMW4zVhHoj BYntTCuX0BzxnT5dKGSvt58EehwzGP1wXL5+BFJUA0ja3bK5glwr4xkJocr1/OEjL3lUj4lq OZakIk+u2w5+T9frrmvoOcN5NzigzmLqsundW/Df0kPQgKQmiU4v+x1Kbj/E38WLVFlOc6kq jfsJDAJMQUvLS1AwFP0tVr1xHqBDC/ld8cgHMvLVRfeRvBgZK6FUvJJaVGiV51LYHkxCVv3/ fAOrznD72UcCOFm7DkK+Uuo3VAwRY+mIgMr6lfDasMdaqqBx3B8efABxp8CDSahubqDNIkid EbADnKW/TFdvqM6hmD4ed9e7DdNr9Qgy70Lr0e39CriHY4nVEHeqz4j8JJMzazGfE0ehzFM0 qpuc8IFCIxhiR7VPbj2Q/bD2UVbHG3Dfox

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