Ssreflect Users Discussion List

[Georges Gonthier <>]

  It's a matter of taste I guess, but I favour using the equation-generation 
feature of ssreflect over reimplementing it with low-level occurrence 
selection,
e.g.,
   move=> n1 n2; move Dn2: n2 => n2rec dummies.
  case Dn1: n1 n2rec / dummies => [|n dummies] in Dn2 *.

  -- Georges

-----Original Message-----
From: Enrico Tassi [] 
Sent: 28 January 2014 18:54
To: 
Subject: Re: [ssreflect] Equation on two parameters

On Tue, Jan 28, 2014 at 10:27:48AM -0800, Beta Ziliani wrote:
> Hi ssrs,
> 
> Does anybody knows how to generate equations for two parameters using 
> the [case: _ _/] tactic?
> 
> Take for example the following dumb example:
> 
> Inductive dummy : nat -> nat -> Prop :=
>   | zero : dummy 0 0
>   | uno : forall n, dummy n n -> dummy (n.+1) (n.+1).
> 
> Goal forall n1 n2 : nat, dummy n1 n2 -> n1 = n2.
> move=>n1 n2.
> case H: _ _/.
> 
> at this point, I have two goals, each of them with an equation H : n1 
> = 0 and H : n1 = _n_.+1 respectively.
> 
> What I'm interested in is in having also an equation for n2. According 
> to the manual this is not possible, but is there a way of achieving 
> this without having to fall back to inversion?

I guess you have 2 possibilities.  One is to generate an equation by hand for 
the other index and used an occurrence selection to rule out one side of that 
equation (untested):

  move=> d; case H: _ {-2}_ / d (erefl n)

The other is to define stuff like (untested):

  Lemma dummyP n m : forall d : dummy n m -> dummy_spec n m d

  Inductive dummy_spec n m d :=
  | first_case : n = m -> n = 0 -> dummy_spec ..
  | other_case : x, n = m -> n = x.+1 -> .... 

And the use the following idiom to case on terms of type dummy:

  case/dummyP

Sorry, I've no Coq at hand,
Ciao
--
Enrico Tassi