The Coq mailing list

[T.Tsokos AT cs.bham.ac.uk]

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.

Regards,
Theo.

ps: my model works on lists, I just gave an example with natural numbers 
trying to simplify the technicalities and concentrate on the "structural" 
question of mine.