Ssreflect Users Discussion List

[Enrico Tassi <>]

On Tue, Apr 15, 2014 at 03:30:23PM +0200, Marcus Ramos wrote:
> I also couldn´t find a (nat) lemma like "forall n: nat, (n = 0) -> n <= 0".
> Does it exist anywhere?

Its absense is a feature, and also the simplest example of the small
scale reflection style of defining things.

If you know n = 0, you just rewrite it and obtain the goal "0 <= k" that
is trivially true by computation for any k (and also in your special case
where k is 0).  Try that:

  Lemma test1 n k : n = 0 -> n <= k.
  Proof. move=> H; rerite H.  (* stop here *) simpl.  (* and here *)
  
And if you have n == 0, you can use the eqP view to obtain n = 0, like in

  Lemma test1 n k : n == 0 -> n <= k.
  Proof. move/eqP=> H; rerite H /=.

or shortly

  Proof. by move/eqP->. Qed.

So this lemma is not there because it would be "empty", if you have n=0, or
just a view application if you have n==0.

Cheers
-- 
Enrico Tassi