The Coq mailing list

[Jevgenijs Sallinens <jevgenijs AT dva.lv>]

Quoting Aaron Bohannon 
<bohannon AT cis.upenn.edu>:

> On Jan 19, 2006, at 10:46 AM, Jevgenijs Sallinens wrote:
> 
> > I think it is more interesting to include (decidable) equality as one 
> > of
> > axiomatization elements,
> 
> Thank you for your suggestion.  However, the decidability of equality 
> is derivable given the signature I provided--as are discrimination and 
> injectivity of constructors.
> 

I mean something like following (just ideas, no details).
Then you are able to apply this theory to implementations of NAT
with abstract equality (different from Leibniz equality, which is
computational equality,related with specific structure used for representation
of natural numbers).
Such an equality together with its properties is called setoid.
Unfortunately Coq doesn't provide simple reasoning with setoids,
so some user written tacics required to help with complicated cases.

Best Regards,
Jevgenijs.

Module Type NAT.

    Parameter N : Set.
   
    Parameter equal:N -> N -> Prop.
    
    Axiom equal_refl .....
    Axiom equal_sym .....
    Axiom equal_trans .....
    Axiom decide_equality ....
    
    Parameter zero : N.
    Parameter succ : N -> N.
    Axiom succ_inv: forall n1 n2, equal n1 n2 -> equal (succ n1) (succ n2). 

    (* Induction principle. *)
    Axiom N_induction :
      forall P : N -> Prop,
      (forall n1 n2, equal n1 n2 -> P n1 -> P n2) -> 
      P zero ->
      (forall n : N, P n -> P (succ n)) ->
      forall n : N, P n.

   and so on .........................
 
 End NAT.


-------------------------------------------------
This mail sent through IMP: http://webmail.dva.lv/