Ssreflect Users Discussion List

[Georges Gonthier <>]

  You're giving three inputs, so I'm not sure which two are puzzling you...
In any case, it's not the meaning of elim, but the meaning of the "push" 
tactical (": ..."), which for this boils down to Coq's primitive "generalize" 
tactic.
  The meaning of tac: ... a_term is to
     - replace all instances of "a_term" in the goal by a fresh variable, and 
binding that variable with a forall quantifier, e.g., changing G(a_term) into 
forall X : T, G(X), where T is the inferred type of "a_term".
     - then running tac: ... recursively.
   That first step can be run in isolation by entering move: a_term, since 
"move" is essentially a no-op in ssreflect.
   If "a_term" is syntactically a variable Z of the proof context (not the 
section context), then it is also deleted from that context, and its name (Z 
here) is reused for X, so the first step amounts to moving Z from above the 
sequent line ================== to right below it.
  If "a_term" does not occur in the goal then Coq displays the new quantified 
goal as
    T -> G
Again, if "a_term" is a proof context assumption, then it is also erased, 
giving the impression that it has "changed" into an explicit assumption.
  All of your examples are of the latter (non-dependent) kind, but with 
"a_term" a new explicit term rather than an existing assumption. In all those 
cases the intermediate goal will be T -> G, where T is the TYPE of "a_term". 
Using the Check command to view the types of the "pushed" term for each of 
the terms below will confirm this
   n < S(n) : bool             (* a Boolean expression *)
   ltnSn n : n < n.+1          (* a proof that n < n.+1 "holds" *)
   (n < S(n))%coq_nat : Prop   (* a (provable) Proposition *)
Note that ssreflect displays S(n) as n.+1, and that there is a hidden 
coercion in the middle case : with the Set Printing Coercions switch on, it 
would be displayed as
  ltnSn n : is_true (n < n.+1)
The coercion is the ssreflect way of telling Coq that proving that a Boolean 
expression e holds means proving that e = true holds.

  Cheers,

Georges

-----Original Message-----
From: Jean-Jacques Levy [] 
Sent: 31 May 2010 12:45
To: 
Subject: meaning of elim

Beginner's question: why I get 2 different answers to following inputs ? -JJ-

> elim: n (n < S(n) )

2 subgoals
  
  ============================
   bool -> reflect (ev 0) (evenb 0)

subgoal 2 is:
 forall n : nat,
 (bool -> reflect (ev n) (evenb n)) -> bool -> reflect (ev n.+1) (evenb n.+1)

> elim: n (ltnSn n).

   0 < 1 -> reflect (ev 0) (evenb 0)

subgoal 2 is:
 forall n : nat,
 (n < n.+1 -> reflect (ev n) (evenb n)) ->
 n.+1 < n.+2 -> reflect (ev n.+1) (evenb n.+1)

>  elim: n (n < S(n))%coq_nat.

2 subgoals
  
  ============================
   Prop -> reflect (ev 0) (evenb 0)

subgoal 2 is:
 forall n : nat,
 (Prop -> reflect (ev n) (evenb n)) -> Prop -> reflect (ev n.+1) (evenb n.+1)