The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

T.Tsokos AT cs.bham.ac.uk
 wrote:
> On Jul 3 2008, Adam Chlipala wrote:
>
> > T.Tsokos AT cs.bham.ac.uk
> >  wrote:
> > > 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?
> >
> > It is puzzling that you bother to maintain proofs that the axioms 
> > hold for particular natural numbers, when you have already asserted 
> > that the axioms hold for all naturals.  With the axioms in place, we 
> > can prove that [nat_embedded] is isomorphic to [nat].
>
> Interesting point. However, by "embedding" these axioms, I (think I) 
> am trying define/describe a specific subset of natural numbers and 
> prove some properties for this subset. If the property holds for the 
> superset, I reckon it doesn't automatically hold for the subset too.

If you are using the keyword [Axiom], then you are _not_ "embedding the 
axioms."  You are asserting them for all naturals.  Maybe previous 
replies have led you away from using the [Axiom] keyword, in which case 
all is well. ;-)