search

math-comp / mcb

Mathematical Components (the Book)
Other
140 stars 25 forks source link

Question on the Cheatsheet #68

Closed francoisthire closed 5 years ago

francoisthire commented 5 years ago

Let's say I want to prove the following silly theorem

  Theorem test (x y : nat) : if x < y then x < S y else true.
  Proof.

I would do use the case tactic to destruct (x < y). However, to prove the if branch, I need to remember the equation x < y = true.

Hence, I would start my proof this way

  case eqxy: (x < y).

But there is no mention on the cheat sheet whether it is possible to remember this equation using the case tactic. I know it is not possible to put everything on a cheat sheet, but such thing happens often when I am proving things. However, since I am not completely used to the ssreflect language, maybe there is a more idiomatic way to achieve the same goal.

anton-trunov commented 5 years ago

maybe there is a more idiomatic way to achieve the same goal

I would prove a goal like that with ltngtP:

From mathcomp Require Import all_ssreflect.

Theorem test x y : if x < y then x < S y else true.
Proof. by rewrite ltnS; case: ltngtP. Qed.