The Coq mailing list

[Andrej Bauer <Andrej.Bauer AT fmf.uni-lj.si>]

T.Tsokos AT cs.bham.ac.uk
 wrote:
> Dear all,
> I am trying to do the following. Assuming I define 2 axioms:
> Axiom first_axiom : forall (A: ...) ... .
> Axiom second_axiom: forall (A: ...) ... .
>
> Let's say I would like to define a construct of a natural number 
> "embedding" the two properties described by the above axioms. Is there a 
> way to do something like that (as if in sig, where the axioms provide a 
> certificate):
>
> Definition nat_embedded := {n:nat | first_axiom holds /\ second_axiom 
> holds}.
>
> so that I can prove properties on "nat_embedded" later on, that preserve 
> the two axioms as well?

First give your properties names and define them:

Definition p1 (x : A) := .... property 1 ....
Definition p2 (x : A) := .... property 2 ....

Then you state your axioms:

Axiom axiom1: forall x : A, p1 x.
Axiom axiom2: forall x : A, p2 x.

You can refer to p1 and p2 whenever you like, e.g.

Definition nat_embedded := {n : nat | p1 n /\ p2 n }.

Best regards,

Andrej