The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Sun, 11 Oct 2009 18:58:02 +0200, André Hirschowitz <ah AT unice.fr> a  
écrit:

> The intended meaning is
>
> Variable Ztwo: Type.
> Variable ZtwoO: Ztwo.
> Variable ZtwoS: Ztwo ->Ztwo.
> Hypothesis Z2axiom :  forall n : Ztwo ,  ZtwoS (ZtwoS n) =n.

Ok, all that is well typed.

> This is not yet problematic. But we want to know more:
>     - at first that these assumptions are "consistent" and also
>     -some initiality, which will warrant (essential) uniqueness.

"Consistency" should be given by a model, you don't have to bother with it.
What is initiality? Well-foundness?

> Here initiality means something like
>
> "a function from Ztwo to another Type T is given by a term v of type T  
> (for ZtwoO)
> and a term r : T ->T satisfying forall x \in T, r(r x)=x.".
>
> Initiality should be witnessed by Coq constructions extending Case and  
> Fixpoint. In order to be correct, these new constructions should  
> generate proof obligations. May-be this generation could be (slighty?)  
> problematic.

I don't understand initiality

For me all what you have to do is:
Record F2:=
{ Ztwo : Set;
  ZtwoO : Ztwo;
  ZtwoS : Ztwo -> Ztwo;
  Ztwo_spe : forall n : Ztwo ,  ZtwoS (ZtwoS n) =n;
}

and

Definition proj (T : Set) (v : T) (r : T -> T) (correct_r : forall x, r (r  
x) = x) :=
Build_F2 T v r correct r.
(same as proj := Build_F2)

or

Record morphism (S1 S2 : F2) :=
{ pi : S1.(Ztwo) -> S2.(Ztwo);
  piO : pi S1.(ZtwoO) = S2.(ZtwoO);
  piS : forall x, pi (S1.(ZtwoS) x) = S2.(ZtwoS) (pi x)
}

> It may be also not so easy to identify a good class of "allowed" axioms  
> (for instance
> ZtwoO \neq ZtwoO should be rejected).

It is just model dependent...
You can as well make ZtwoO \neq ZtwoO in your hypothesis, but
you simply won't be able to instantiate Ztwo; so you keep sound

> ah
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


--
Utilisant le client e-mail révolutionnaire d'Opera :  
http://www.opera.com/mail/