coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: 朱立平 <zlponline AT 163.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] coq tatic help
Date: Sun, 17 Mar 2019 19:27:26 +0800 (CST)
Authentication-results: mail2-smtp-roc.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-57.163.com
Ironport-phdr: 9a23:ljL3zh37etrJ5BK3smDT+DRfVm0co7zxezQtwd8ZsewfLvad9pjvdHbS+e9qxAeQG9mCs7Qc0qL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHOfwlEniaxba5vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLoiSkJOT4n/m/KkMJ+i75Urx2iqRFk2YHYfJuYO+Fkc6/BYd0XQ3dKUMZLVyxGB4Oxd5MJCPcFOOVftoz4p0YFoBy/BAmoHOPvzTlIhnv33a08zessChzK0Q0uEt4UrHvUq9D1Ob4UXOuoz6fI1S3OY+1I1Tvh8oTEbxMsreyWUb5tf8fd00kiGgHdglmNtIDpIimZ2vkOvmSB4OdtV/ijh3A7pw1spDWk290ihZPTho0Pz1DJ7SV5z5gxJd2/UEN7ZMOoHZVJuyyaNYZ6WN4uTmBmtSog1rIGvpu7cDALyJQh2RHfd+SKf5aW7h7/TuqdPDR1iG9/dL6iiRu+60itx+/kWsmxyllKry5FktfWtnAK0hze8smGSv9l/kem3zaP0wHT6udaLk0viKbWKpAszqQsmZoUtETPBjX2l1nujK+KakUk/fCl5PjgYrX/v5OTK4t0ihzlPak1gcy+AeE4MhAUUGSB+OS80qfj/UzjT7lQgP02iPqRjJePb88cv+uyBxJf+ocl8Re2STm8mpxMln4eaVlBZRivjo7zOliILuquXtmlhFH5LrPCDV4TdunzBo3KKHzClrrJJOgmrUVbzVxgnphk+5tIB+RZc7rIUUjruYmAV05rA0mP2+/iTe5F+MYbUGOLDLWeNfKA6AHToOkoJrvVPdNHiHPGM/EgosXWozohg1ZML/D3ht0cb3XqRq07cXXcWmLlh5I6KUlPvgc6S7W02ljbCnsOODDrAfl67TY+Wtqr

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