search

coq-community / coq-art

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
https://coq-community.org/coq-art/
MIT License
110 stars 22 forks source link

typo of `cond_rewrite_example` #18

Closed yoshihiro503 closed 3 years ago

yoshihiro503 commented 3 years ago

Is the first < of the statement of cond_rewrite_example a mistake for <=?

Since these premises lead to contradictions, any consequence can be proved. For example:

Goal : forall n:nat, 8 < n+6 ->  3+n < 6 -> 0 = 1.
Proof.
  intros. omega.
Qed.
Casteran commented 3 years ago

I changes omega for lia, and corrected the lemma conditional_rewrite_example too

yoshihiro503 commented 3 years ago

I see. Thank you for merging. I didn't know that omega tactic has been deprecated. Thanks a lot.

Casteran commented 3 years ago

Well, It’s going to be deprecated in future versions of Coq. Using it now is not an error yet. Thank you for reporting!

Le 25 janv. 2021 à 15:37, YOSHIHIRO Imai notifications@github.com a écrit :

I see. Thank you for merging. I didn't know that omega tactic has been deprecated. Thanks a lot.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/coq-community/coq-art/pull/18#issuecomment-766859328, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCQNNIKL3G46NJIIAJDS3V6Y7ANCNFSM4WRZJ7GA.