The Coq mailing list

[CHAUVIN Barnabe <barnabe.chauvin AT gmail.com>]

I answer myself :

jrw give me a very solution on IRC :

Define two theorems (including the case hypothesis) :
    Theorem thm1 : P=0 -> ...
    Theorem thm2 : P<>0 -> ...
(For example, if the different cases depend on the value of P)
And then use an extra theorem that include both :
    Theorem thm : ...
Which is easy to prove with [destruct]

On 12/01/2015 20:51, CHAUVIN Barnabe wrote:
> Hello club !
>
> I am trying to define some theorems, and I am having difficulty :
>
> Let's say I have a variable P.
>
> I want to define a theorem that depend on the value of P (If it is 
> zero or not actually). The problem is that it makes the theorem very 
> big (i.e. a lot of hypothesis), because of the different cases.
> (The proof also depend on that value, but this is not the main problem).
>
> Thus, I was wondering whether it would be possible to define a kind of 
> record (By analogy with [Record]) that would store several theorems 
> (In fact, it would to the same theorems, but with a value-hypothesis 
> diference).
> Each of these theorems would have a condition (a kind of predicate) 
> that would decide which one has to be used when using [apply] for 
> example.
>
> Actually, I can define these theorems as usual, by using different 
> names (like theorem1, theorem2 ...), but I really want only one name, 
> to be able to use it as a single theorem in other proofs (like when 
> using [apply] for instance).
>
> Thanks for your help, I don't know if it is really clear ... I don't 
> know at all if it exists or not, that's why I am asking here ..
>
> Barnabé Chauvin