The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Chauvin,

if you have many lemmas which depend on several variables, the section 
mechanism might be interesting for you. It allows to declare variables which 
are shared by several lemmas and can later be generalized when the section is 
closed. See the below example:

Section Test.

Variable x : nat.

Lemma incx: 1+x=S x. 
Proof. reflexivity. Qed.

(* Signature of incx inside section: incx : 1 + x = S x *)

End Test.

(* Signature of incx outside of section: incx : forall x : nat, 1 + x = S x *)

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of CHAUVIN Barnabe
Sent: Monday, January 12, 2015 8:51 PM
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Store several theorems in a kind of Record

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