Changeset 10 for C-semantics

Timestamp:

Jul 6, 2010, 11:53:23 AM (11 years ago)

Author:

campbell

Message:

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

Location:

C-semantics

Files:

• AST.ma (modified) (3 diffs)
• Cexec.ma (modified) (3 diffs)
• Coqlib.ma (modified) (3 diffs)
• Integers.ma (modified) (3 diffs)
• Maps.ma (modified) (1 diff)
• Mem.ma (modified) (11 diffs)
• binary (added)
• binary/Z.ma (added)
• binary/positive.ma (added)
• extralib.ma (modified) (14 diffs)

C-semantics/AST.ma

@@ -21 +21 @@
 include "Integers.ma".
 include "Floats.ma".
+include "binary/positive.ma".
 
 (* * * Syntactic elements *)
@@ -26 +27 @@
 (* * Identifiers (names of local variables, of global symbols and functions,
   etc) are represented by the type [positive] of positive integers. *)
+
+ndefinition ident ≝ Pos.
+
+ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
+#x y; nlapply (pos_compare_to_Prop x y); ncases (pos_compare x y);
+##[ #H; @2; /2/; ##| #H; @1; //; ##| #H; @2; /2/ ##] nqed.
+
 (*
-Definition ident := positive.
-
-Definition ident_eq := peq.
-*)
 (* XXX: we use nats for now, but if in future we use binary like compcert
         then the maps will be easier to define. *)
@@ -45 +49 @@
   ##]
 ##] nqed. 
-
+*)
 (* * The intermediate languages are weakly typed, using only two types:
   [Tint] for integers and pointers, and [Tfloat] for floating-point

C-semantics/Cexec.ma

@@ -429 +429 @@
   on d:decide to ? + (¬?).
 
+ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P.
+#P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##| napply Error ##] nqed. 
+
+ncoercion decide_inject2 :
+  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P ≝ dodecide2
+  on d:decide to res ?.
+
 alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
 alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
@@ -438 +445 @@
 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
 
-(* Not very happy about this. *)
-nlet rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
+nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
 match t1 with
 [ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ]
 | Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
 | Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
-| Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
+| Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
 | Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒
-    match type_eq_dec t t' with [ inl _ ⇒
-      match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]
-| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match typelist_eq_dec tl tl' with [ inl _ ⇒ 
-    match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]
+    match assert_type_eq t t' with [ OK _ ⇒
+      match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
+| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒ 
+    match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
 | Tstruct i fl ⇒
     match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
-      match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
+      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
 | Tunion i fl ⇒
     match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
-      match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
+      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] |  _ ⇒ dn ]
 | Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
 ]
-and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
+and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝
 match tl1 with
 [ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ]
 | Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒ 
-    match type_eq_dec t1 t2 with [ inl _ ⇒
-      match typelist_eq_dec ts1 ts2 with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
+    match assert_type_eq t1 t2 with [ OK _ ⇒
+      match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
 ]
-and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
+and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝
 match fl1 with
 [ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ]
 | Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒ 
     match ident_eq i1 i2 with [ inl _ ⇒
-      match type_eq_dec t1 t2 with [ inl _ ⇒
-        match fieldlist_eq_dec fs1 fs2 with [ inl _ ⇒ dy | _ ⇒ dn ]
+      match assert_type_eq t1 t2 with [ OK _ ⇒
+        match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy | _ ⇒ dn ]
         | _ ⇒ dn ] | _ ⇒ dn ] ]
 ].
 (* A poor man's clear, otherwise automation picks up recursive calls without
    checking that the argument is smaller. *)
-ngeneralize in type_eq_dec;
-ngeneralize in typelist_eq_dec;
-ngeneralize in fieldlist_eq_dec; #avoid1 avoid2 avoid3 avoid4 avoid5 avoid6;
-ndestruct; //; @; #H; ndestruct;
-##[ nelim c8; /2/
-##| nelim c6; /2/
-##| nelim c4; /2/
-##| nelim c4; /2/
-##| nelim c8; /2/
-##| nelim c6; /2/
-##| nelim c8; /2/
-##| nelim c6; /2/
-##| nelim c8; /2/
-##| nelim c6; /2/
-##| nelim c8; /2/
-##| nelim c6; /2/
-##| nelim c4; /2/
-##| nelim c8; /2/
-##| nelim c6; /2/
-##| nelim c12; /2/
-##| nelim c10; /2/
-##| nelim c8; /2/
-##] nqed. 
-
-ndefinition are_equal : ∀A:Type. (∀x,y:A.(x=y)+(x≠y)) → ∀x,y:A. res (x=y) ≝
-λA,dec,x,y.
-match dec … x y with
-[ inl p ⇒ OK ? p
-| inr _ ⇒ Error ?
-].
+ngeneralize in assert_type_eq;
+ngeneralize in assert_typelist_eq;
+ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //;
+(* XXX: I have no idea why the first // didn't catch these. *)
+//; //; //; //; //; //; //; //; //;
+nqed.
 
 nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
@@ -527 +509 @@
     vargs ← exec_exprlist ge e m al;:
     fd ← opt_to_res ? (find_funct Genv ? ge vf);:
-    p ← are_equal ? type_eq_dec (type_of_fundef fd) (typeof a);:
+    p ← assert_type_eq (type_of_fundef fd) (typeof a);:
     k' ← match lhs with
          [ None ⇒ OK ? (Kcall (None ?) f e k)

C-semantics/Coqlib.ma

@@ -18 +18 @@
     library. *)
 
-include "arithmetics/Z.ma".
+include "binary/Z.ma".
 include "datatypes/sums.ma".
 include "datatypes/list.ma".
@@ -347 +347 @@
   auto.
 Qed.
-
-(** Properties of powers of two. *)
-
-Lemma two_power_nat_O : two_power_nat O = 1.
-Proof. reflexivity. Qed.
-
-Lemma two_power_nat_pos : forall n : nat, two_power_nat n > 0.
-Proof.
-  induction n. rewrite two_power_nat_O. omega.
-  rewrite two_power_nat_S. omega.
-Qed.
-
-Lemma two_power_nat_two_p:
-  forall x, two_power_nat x = two_p (Z_of_nat x).
-Proof.
-  induction x. auto. 
-  rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega.
-Qed.
-
+*)
+(* * Properties of powers of two. *)
+
+nlemma two_power_nat_O : two_power_nat O = one.
+//; nqed.
+
+nlemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0.
+//; nqed.
+
+nlemma two_power_nat_two_p:
+  ∀x. Z_two_power_nat x = two_p (Z_of_nat x).
+#x; ncases x;
+##[ //;
+##| nnormalize; #p; nelim p; //; #p' H; nrewrite > (nat_succ_pos …); //;
+##] nqed.
+(*
 Lemma two_p_monotone:
   forall x y, 0 <= x <= y -> two_p x <= two_p y.
@@ -577 +574 @@
 (* * Alignment: [align n amount] returns the smallest multiple of [amount]
   greater than or equal to [n]. *)
-naxiom align : Z → Z → Z.
-(*
+(*naxiom align : Z → Z → Z.*)
+
 ndefinition align ≝ λn: Z. λamount: Z.
   ((n + amount - 1) / amount) * amount.
-
+(*
 Lemma align_le: forall x y, y > 0 -> x <= align x y.
 Proof.

C-semantics/Integers.ma

@@ -17 +17 @@
 
 include "arithmetics/nat.ma".
-include "arithmetics/Z.ma".
+include "binary/Z.ma".
 include "extralib.ma".
 
@@ -62 +62 @@
 *)
 
-naxiom two_power_nat : nat → Z.
+(*naxiom two_power_nat : nat → Z.*)
 
 ndefinition wordsize : nat ≝ 32.
-ndefinition modulus : Z ≝ two_power_nat wordsize.
+ndefinition modulus : Z ≝ Z_two_power_nat wordsize.
 ndefinition half_modulus : Z ≝ modulus / 2.
 ndefinition max_unsigned : Z ≝ modulus - 1.
@@ -75 +75 @@
 nnormalize; //; nqed.
 
-(*
-Remark modulus_power:
+nremark modulus_power:
   modulus = two_p (Z_of_nat wordsize).
-Proof.
-  unfold modulus. apply two_power_nat_two_p.
-Qed.
-
-Remark modulus_pos:
+//; nqed.
+
+nremark modulus_pos:
   modulus > 0.
-Proof.
-  rewrite modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega.
-Qed.
-*)
+//; nqed.
+
 (* * Representation of machine integers *)
 

C-semantics/Maps.ma

@@ -172 +172 @@
 *)
 
-naxiom PTree : TREE ident.
+(* XXX: need real tree impl *)
+nlet rec assoc_get (A:Type) (i:ident) (l:list (ident × A)) on l ≝
+match l with
+[ nil ⇒ None ?
+| cons h t ⇒
+  match h with [ mk_pair hi ha ⇒
+    match ident_eq i hi with [ inl _ ⇒ Some ? ha | inr _ ⇒ assoc_get A i t ] ]
+].
+
+naxiom assoc_tree_eq: ∀A: Type. ∀x,y: A. (x=y) + (x≠y) →
+      ∀a,b: list (ident × A). (a = b) + (a ≠ b).
+naxiom assoc_remove: ∀A: Type. ident → list (ident × A) → list (ident × A).
+naxiom assoc_tree_map: ∀A,B: Type. (ident → A → B) → list (ident × A) → list (ident × B).
+naxiom assoc_elements: ∀A: Type. list (ident × A) → list (ident × A).
+naxiom assoc_tree_fold: ∀A,B: Type. (B → ident → A → B) → list (ident × A) → B → B.
+
+ndefinition PTree : TREE ident ≝
+mk_TREE ?
+  ident_eq
+  (λA. list (ident × A))
+  assoc_tree_eq
+  (λA. nil ?)
+  assoc_get
+  (λA,i,a,l.〈i,a〉::l)
+  assoc_remove
+  assoc_tree_map
+  assoc_elements
+  assoc_tree_fold.
 
 (*

C-semantics/Mem.ma

@@ -25 +25 @@
 *)
 
-include "arithmetics/Z.ma".
+include "arithmetics/nat.ma".
+include "binary/Z.ma".
 include "datatypes/sums.ma".
 include "datatypes/list.ma".
@@ -127 +128 @@
   | Mfloat64 => 7].
 
+alias symbol "plus" (instance 2) = "integer plus".
 nlemma size_chunk_pred:
   ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk.
@@ -164 +166 @@
 nlemma align_size_chunk_divides:
   ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
-#chunk;ncases chunk;nnormalize;@;//;##[ napply 2; ##| // ##]
+#chunk;ncases chunk;nnormalize;/3/;
 nqed.
 
@@ -176 +178 @@
 (* The initial store. *)
 
-ndefinition oneZ ≝ pos O.
+ndefinition oneZ ≝ pos one.
 
 nremark one_pos: OZ < oneZ.
@@ -186 +188 @@
 
 ndefinition empty: mem ≝ 
-  mk_mem (λx.empty_block OZ OZ) (pos O) one_pos.
+  mk_mem (λx.empty_block OZ OZ) (pos one) one_pos.
 
 ndefinition nullptr: block ≝ OZ.
@@ -501 +503 @@
 nchange in ⊢ (??(???%)?) with (update ????);
 nwhd in ⊢(??%?);nrewrite > (update_s content …);
-nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false …);//;napply sym_neq;//;
+nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false … (sym_neq … H));//;
 nqed.
 
@@ -512 +514 @@
 nlapply (eqZb_to_Prop p1 p2); ncases (eqZb p1 p2); #Hp;
 ##[nrewrite > Hp;
-   nlapply (eqb_to_Prop n1 n2);ncases (eqb n1 n2); #Hn;
+   napply (eqb_elim n1 n2); #Hn;
    ##[nrewrite > Hn;@; @; //;
    ##|@2;/2/]
@@ -1055 +1057 @@
 ##|nrewrite > (size_chunk_pred …) in H1;nrewrite > (size_chunk_pred …);
    #H1;napply nmk;#Hfalse;nelim H1;#H4;napply H4;
-   napply (eq_f ?? (λx.Z_of_nat (1 + x)) ???);//##]
+   napply (eq_f ?? (λx.1 + x) ???);//##]
 nqed.
 
@@ -1582 +1584 @@
     ##| napply (Zleb_true_to_Zle … H2)
     ##| nwhd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon
-    ##| napply (witness ?? (abs ofs)); nnormalize; nrewrite > (Zplus_z_OZ ?); //
+    ##| ncases ofs; /2/;
     ##]
 ##| *; #Hval;#Hlo;#Hhi;#Hal;
@@ -1699 +1701 @@
 ##| #ineq; @1; @1; napply ineq;
 ##] nqed.
-
+(*  XXX: reenable once I've sorted out performance a bit
 ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem.
   ∀b1,b1',delta1,b2,b2',delta2.
@@ -2365 +2367 @@
     ##]
 ##] nqed.
-(*  XXX: reenable once I've sorted out Integers.ma a bit
+
 nlemma valid_pointer_inject_no_overflow:
   ∀f,m1,m2,b,ofs,b',x.

C-semantics/extralib.ma

@@ -13 +13 @@
 (**************************************************************************)
 
-include "arithmetics/Z.ma".
 include "datatypes/sums.ma".
 include "datatypes/list.ma".
 include "Plogic/equality.ma".
+include "binary/Z.ma".
+include "binary/positive.ma".
 
 nlemma eq_rect_Type0_r:
@@ -61 +62 @@
 
 (* XXX: divides goes to arithmetics *)
-ninductive divides (n,m:nat) : Prop ≝
-| witness : ∀p:nat.m = times n p → divides n m.
-interpretation "divides" 'divides n m = (divides n m).
-interpretation "not divides" 'ndivides n m = (Not (divides n m)).
-
-ndefinition dividesZ ≝ λx,y:Z. abs x ∣ abs y.
+ninductive dividesP (n,m:Pos) : Prop ≝
+| witness : ∀p:Pos.m = times n p → dividesP n m.
+interpretation "positive divides" 'divides n m = (dividesP n m).
+interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)).
+
+ndefinition dividesZ : Z → Z → Prop ≝
+λx,y. match x with
+[ OZ ⇒ False
+| pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
+| neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
+].
+
 interpretation "integer divides" 'divides n m = (dividesZ n m).
 interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)).
 
 (* should be proved in nat.ma, but it's not! *)
-naxiom eqb_to_Prop : ∀n,m.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
+naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
+
+nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
+#n m; napply eqb_elim; //; nqed.
 
 nlemma injective_Z_of_nat : injective ? ? Z_of_nat.
@@ -77 +87 @@
 #n;#m;ncases n;ncases m;nnormalize;//;
 ##[ ##1,2: #n';#H;ndestruct
-##| #n';#m'; #H; ndestruct; //
+##| #n';#m'; #H; ndestruct; nrewrite > (succ_pos_of_nat_inj … e0); //
 ##] nqed.
 
@@ -92 +102 @@
 nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
 #x;#y;
-#n;
-nelim n; ##[ ##2: #n'; #IH; ##]
+napply pos_elim
+ ##[ ##2: #n'; #IH; ##]
 nrewrite > (Zplus_Zsucc_Zpred y ?);
-nwhd in ⊢ (?→??(??%));
-##[ #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);
+##[ nrewrite > (Zpred_Zsucc (pos n'));
+ #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);
     napply Zsucc_le;
 ##| #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le;
@@ -115 +125 @@
 /3/; #H; nrewrite > H; //; nqed.
 
+ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
+#x y; ncases x;
+##[ ncases y;
+  ##[ ##1,2: //
+  ##| #n; napply False_ind;
+  ##]
+##| #n; ncases y;
+  ##[ nnormalize; napply False_ind;
+  ##| #m; napply (pos_cases … n); /2/;
+  ##| #m; nnormalize; napply False_ind;
+  ##]
+##| #n; ncases y; /2/;
+##] nqed.
+    
 ntheorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
-#n;#m;#p; nlapply (Z_compare_to_Prop n p); nelim (Z_compare n p);
-##[ //;
-##| #H; nrewrite > H; #A;#B; napply False_ind; nlapply (Zlt_to_Zle … A);
-    #C; nlapply (transitive_Zle … C B); nelim p; /2/; #n';nelim n'; /2/;
-##| #A; #B; #C; nlapply (transitive_Zlt … A B); #D;
-    napply False_ind; nlapply (Zlt_to_Zle … D);
-    #E; nlapply (transitive_Zle … E C); nelim p; /2/; #n';nelim n'; /2/;
-##] nqed.
-
-nlemma decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
+#n m p Hlt Hle; nrewrite < (Zpred_Zsucc n); napply Zle_to_Zlt;
+napply (transitive_Zle … Hle); /2/;
+nqed.
+
+ndefinition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
 #z1;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H;
 ##[@;//
@@ -180 +199 @@
     match y with 
     [ OZ ⇒ false
-    | pos m ⇒ leb (S n) m
+    | pos m ⇒ leb (succ n) m
     | neg m ⇒ false ]
   | neg n ⇒
@@ -186 +205 @@
     [ OZ ⇒ true
     | pos m ⇒ true
-    | neg m ⇒ leb (S m) n ]].
+    | neg m ⇒ leb (succ m) n ]].
 
 
@@ -205 +224 @@
 
 ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
-#n;#m;ncases n;ncases m; nnormalize; /2/;
+#n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct;
 nqed.
 
@@ -225 +244 @@
 
 ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
-#n;#m;ncases n;ncases m; nnormalize; /2/;
-##[ #n';#m';ncases n';nnormalize;
-  ##[ ##2: #n';#H; napply not_le_to_not_le_S_S; napply leb_false_to_not_le; ##]
-  //;
-##| #n';#m';ncases m';nnormalize;
-  ##[ ##2: #m';#H; napply not_le_to_not_le_S_S; napply leb_false_to_not_le; ##]
-  //;
-##] nqed.
+#n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct;
+nqed.
 
 ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 
@@ -258 +271 @@
 
 (* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
-notation > "'if' term 19 e 'then' term 19 t 'else' term 68 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 68 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
 
@@ -280 +293 @@
 (* division *)
 
-nlet rec divide_aux (b,m,n,p:nat) on b ≝ 
-  if leb (S m) n then 〈p,m〉 else
-  match b with
-  [ O ⇒ 〈p,m〉
-  | S b' ⇒ divide_aux b' (m-n) n (S p)
-  ].
-
-ndefinition divide ≝ λm,n. divide_aux m m n O.
+ninductive natp : Type ≝
+| pzero : natp
+| ppos  : Pos → natp.
+
+ndefinition natp0 ≝
+λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
+
+ndefinition natp1 ≝
+λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
+
+nlet rec divide (m,n:Pos) on m ≝ 
+match m with 
+[ one ⇒
+  match n with
+  [ one ⇒ 〈ppos one,pzero〉
+  | _ ⇒ 〈pzero,ppos one〉
+  ]
+| p0 m' ⇒
+  match divide m' n with
+  [ mk_pair q r ⇒
+    match r with
+    [ pzero ⇒ 〈natp0 q,pzero〉
+    | ppos r' ⇒
+      match partial_minus (p0 r') n with
+      [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉
+      | MinusZero ⇒ 〈natp1 q, pzero〉
+      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
+      ]
+    ]
+  ]
+| p1 m' ⇒
+  match divide m' n with
+  [ mk_pair q r ⇒
+    match r with
+    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
+    | ppos r' ⇒
+      match partial_minus (p1 r') n with
+      [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉
+      | MinusZero ⇒ 〈natp1 q, pzero〉
+      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
+      ]
+    ]
+  ]
+].
+
 ndefinition div ≝ λm,n. fst ?? (divide m n).
 ndefinition mod ≝ λm,n. snd ?? (divide m n).
@@ -306 +356 @@
 nqed.
 
-nlemma minus_plus_distrib: ∀n,m,p. m-(n+p) = m-n-p.
-#n;nelim n; //; #n';#IH;#m;#p;nnormalize;
-nelim m; //; nqed.
+nlemma pred_minus: ∀n,m. pred n - m = pred (n-m).
+napply pos_elim; /3/;
+nqed.
+
+nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
+napply pos_elim;
+##[ //
+##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/;
+##] nqed.
 
 ntheorem plus_minus_r:
-∀m,n,p:nat. m ≤ n → p+(n-m) = (p+n)-m.
+∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
 #m;#n;#p;#le;nrewrite > (symmetric_plus …);
 nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.
 
-nlemma plus_minus_le: ∀m,n,p. m≤n → m+p-n≤p.
+nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
 #m;#n;#p;nelim m;/2/; nqed.
-
+(*
 nlemma le_to_minus: ∀m,n. m≤n → m-n = 0.
 #m;#n;nelim n;
@@ -324 +380 @@
     nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/
 ##] nqed.
-
-nlemma minus_times_distrib_l: ∀n,m,p:nat. p*m-p*n = p*(m-n).
-#n;#m;#p;nelim (decidable_le n m);#le;
-##[ nelim p; //;#p'; #IH; nnormalize; nrewrite > (minus_plus_distrib …);
-    nrewrite < (plus_minus … le); nrewrite < IH;
+*)
+nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
+#n;#m;#p;(*nelim (decidable_lt n m);*)#lt;
+(*##[*) napply (pos_elim … p); //;#p'; #IH;
+    nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);
+    nrewrite > (minus_plus_distrib …);
+    nrewrite < (plus_minus … lt); nrewrite < IH;
     nrewrite > (plus_minus_r …); /2/;
-##|
-nlapply (not_le_to_lt … le); #lt;
-nelim p; //; #p';
- ncut (m-n = 0); ##[ /3/ ##]
-  #mn; nrewrite > mn; nrewrite < (times_n_O …); #H;
-  nnormalize; napply sym_eq; napply  le_n_O_to_eq; nrewrite < H;
+nqed.
+(*##|
+nlapply (not_lt_to_le … lt); #le;
+napply (pos_elim … p); //; #p';
+ ncut (m-n = one); ##[ /3/ ##]
+  #mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …);
+  #H; nrewrite < H in ⊢ (???%); 
+  napply sym_eq; napply  le_n_one_to_eq; nrewrite < H;
   nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l;
   /2/;
@@ -346 +406 @@
 napply False_ind; napply (absurd ? H ( not_le_Sn_n n));
 nqed.
-
-nlemma divide_aux_ok : ∀b,m,n,p,dv,md:nat.
- n > 0 → b ≥ m →
- divide_aux b m n p = 〈dv,md〉 →
- m + p*n = dv*n + md ∧ md < n.
-#b;nelim b;
-##[ #m;#n;#p;#dv;#md;#npos;#bound;
-    nwhd in ⊢ (??%% → ?); nelim (leb (S m) n); nwhd in ⊢ (??%% → ?); #H;
-    ndestruct;
-    @; /2/
-##| #b';#IH;#m;#n;#p;#dv;#md;
- #npos; #bound; nwhd in ⊢ (??%? → ?); napply leb_elim;
-  ##[ #Hlt; nwhd in ⊢ (??%? → ?); #H;
-    ndestruct;
-    /2/;
-  ##| #Hnlt; ncut (n≤m); ##[ nlapply (not_le_to_lt … Hnlt); /2/; ##]
-      #Hnm; nwhd in ⊢ (??%? → ?); #H;
-      nlapply (IH … H); ##[ napply le_S_S_to_le; napply (transitive_le ? m);  //;
-                            nrewrite < (minus_Sn_m …); //; napply (lt_O_n_elim …npos); #n';
-                            nrewrite > (minus_S_S …); /2/;
-                        ##| //
-                        ##| nnormalize; nrewrite < (associative_plus …); nrewrite < (plus_minus_m_m …); //;
-                        ##]
-  ##] nqed.
-
-ntheorem divide_divides: ∀m,n,dv,md:nat.
- n > 0 → divide m n = 〈dv,md〉 → m = dv * n + md ∧ md < n.
-#m;#n;#dv;#md;#npos; nwhd in ⊢ (??%? → ?); #DIVIDE;
-nlapply (divide_aux_ok … DIVIDE); //; nqed.
-
-nlemma mod0_divides: ∀m,n,dv:nat.
-  m>0 → divide n m = 〈dv,O〉 → m∣n.
-#m;#n;#dv;#mpos;#DIVIDE;@ dv; nlapply (divide_divides … DIVIDE); //; *; //;
-nqed.
-
-nlemma divides_mod0: ∀dv,m,n:nat.
-  m>0 → n = dv*m → divide n m = 〈dv,O〉.
-#dv;#m;#n;#mpos;#DIV;nlapply (refl ? (divide n m));
-nelim (divide n m) in ⊢ (???% → ?); #dv';#md'; #DIVIDE;
-nlapply (divide_divides … mpos DIVIDE); *; 
-nrewrite > DIV in ⊢ (% → ?); #H; nlapply (plus_to_minus … H);
-nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv' …);
-nrewrite > (minus_times_distrib_l …);
-nelim (decidable_le dv dv');
-##[ #le; ncut (dv-dv' = 0); ##[ /2/ ##]
-    #eq; nrewrite > eq; nrewrite < (times_n_O …); #md0; #_;
-    nrewrite > DIVIDE; nrewrite < md0 in H ⊢ %; nrewrite < (plus_n_O …); 
-    #H; ncut (dv = dv');  ##[ napply le_to_le_to_eq; //;
-    napply (le_times_to_le m); //; ##]
-     //;
-##| #nle; ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
-    #Hdv; #H; ncut (md' ≥ m); /2/; #A;#B; napply False_ind;
-    napply (absurd ? A (lt_to_not_le … B));
-##] nqed.
-
-nlemma dec_divides_1: ∀m,n:nat. m>0 → (m∣n) + ¬(m∣n).
-#m;#n;#mpos; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
-#dv;#md; ncases md;
-##[ #H; @1; napply mod0_divides; //;
+*)
+
+nlet rec natp_plus (n,m:natp) ≝
+match n with
+[ pzero ⇒ m
+| ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]
+].
+
+nlet rec natp_times (n,m:natp) ≝
+match n with
+[ pzero ⇒ pzero
+| ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]
+].
+
+ninductive natp_lt : natp → Pos → Prop ≝
+| plt_zero : ∀n. natp_lt pzero n
+| plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.
+
+nlemma lt_p0: ∀n:Pos. one < p0 n.
+#n; nnormalize; /2/; nqed.
+
+nlemma lt_p1: ∀n:Pos. one < p1 n.
+#n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed.
+
+nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
+#m; nelim m;
+##[ //;
+##| ##2,3: #m' IH; nnormalize; nrewrite > IH; //;
+##] nqed.
+
+nlemma pos_nonzero2: ∀n. ∀P:Pos→Type. ∀Q:Type. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n).
+#n P Q; napply succ_elim; /2/; nqed.
+
+nlemma partial_minus_to_Prop: ∀n,m.
+  match partial_minus n m with
+  [ MinusNeg ⇒ n < m
+  | MinusZero ⇒ n = m
+  | MinusPos r ⇒ n = m+r
+  ].
+#n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m);
+nnormalize; ncases (partial_minus n m); /2/; nqed.
+
+nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
+#n m lt; nelim lt; /2/;
+nqed.
+
+nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
+#n m lt; napply (transitive_lt ? (p0 m) ?); /2/;
+nqed.
+
+nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
+#n m lt; ninversion lt;
+##[ #H; nrewrite > (succ_injective … H); //;
+##| #p H1 H2 H3;nrewrite > (succ_injective … H3);
+    napply (transitive_lt ? (p0 p) ?); /2/;
+##] 
+nqed.
+
+nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
+#n m lt; nelim lt; /2/;
+nqed.
+
+
+
+nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
+#n m lt;ninversion lt;
+##[ #p H; ndestruct;
+##| #n' m' lt e1 e2; ndestruct; //;
+##] nqed.
+
+nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
+#a b; /2/; nqed.
+
+nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
+#a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed.
+
+nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
+/2/; nqed.
+
+nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
+#A B a1 a2 b1 b2 H; ndestruct; //;
+nqed.
+
+nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
+#A B a1 a2 b1 b2 H; ndestruct; //;
+nqed.
+
+ntheorem divide_ok : ∀m,n,dv,md.
+ divide m n = 〈dv,md〉 →
+ ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
+#m n; napply (pos_cases … n);
+##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/;
+##| #n'; nelim m;
+  ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
+  ##| #m' IH dv md; nnormalize;
+      nlapply (refl ? (divide m' (succ n')));
+      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
+      #dv' md' DIVr; nelim (IH … DIVr);
+      nnormalize; ncases md';
+      ##[ ncases dv'; nnormalize;
+        ##[ #H; ndestruct;
+        ##| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
+        ##]
+      ##| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
+          nnormalize; #n md'' Hr1 Hr2;
+          nlapply (plt_lt … Hr2); #Hr2';
+          nlapply (partial_minus_to_Prop md'' n);
+          ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize;
+          #lt; #e; ndestruct; @; /2/; napply plt_pos;
+          ##[ ##1,3,5,7: napply double_lt1; /2/;
+          ##| ##2,4: napply double_lt3; /2/;
+          ##| ##*: napply double_lt2; /2/;
+          ##]
+      ##]
+  ##| #m' IH dv md; nwhd in ⊢ (??%? → ?);
+      nlapply (refl ? (divide m' (succ n')));
+      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
+      #dv' md' DIVr; nelim (IH … DIVr);
+      nwhd in ⊢ (? → ? → ??%? → ?); ncases md';
+      ##[ ncases dv'; nnormalize;
+        ##[ #H; ndestruct;
+        ##| #dv'' Hr1 Hr2; #H; ndestruct; /3/;
+        ##]
+      ##| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
+          nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2;
+          nlapply (plt_lt … Hr2); #Hr2';
+          nwhd in ⊢ (??%? → ?);
+          nlapply (partial_minus_to_Prop (p0 md'') (succ n'));
+          ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##]
+          ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize;
+          #Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##]
+          #lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##]
+          nrewrite < (pair_eq1 … e); nrewrite < (pair_eq2 … e);
+          nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos;
+          ##[ ncut (succ n' + r'' < p0 (succ n')); /2/;
+          ##| ncut (succ n' + r'' < p0 (succ n')); /2/;
+          ##| /2/;
+          ##| /2/;
+          ##]
+      ##]
+  ##]
+##] nqed.
+
+nlemma mod0_divides: ∀m,n,dv:Pos.
+  divide n m = 〈ppos dv,pzero〉 → m∣n.
+#m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *;
+nnormalize; #H; ndestruct; //;
+nqed.
+
+nlemma divides_mod0: ∀dv,m,n:Pos.
+  n = dv*m → divide n m = 〈ppos dv,pzero〉.
+#dv;#m;#n;#DIV;nlapply (refl ? (divide n m));
+nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE;
+nlapply (divide_ok … DIVIDE); *;
+ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##]
+ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE;  nnormalize;
+nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct;
+##[ nlapply (plus_to_minus … e0);
+    nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …);
+    ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt;
+    nrewrite > (minus_times_distrib_l …); //;
+
+ (*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
+    #Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind;
+    napply (absurd ? B (lt_to_not_le … A));
+
+##| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/;
+
+##| nrewrite > DIVIDE; ncut (dv = dv''); /2/;
+##]
+nqed.
+
+nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
+#m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
+#dv;#md; ncases md; ncases dv;
+##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct
+##| #dv'; #H; @1; napply mod0_divides; /2/;
 ##| #md'; #DIVIDES; @2; napply nmk; *; #dv';
-    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); //;
+    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
     nrewrite > DIVIDES; #H'; 
     ndestruct;
-##] nqed.
-
-nlemma dec_divides: ∀m,n:nat. (m∣n) + ¬(m∣n).
-#m;#n; ncases m; /2/;
-ncases n;
-##[ @1; @ O; //;
-##| #n'; @ 2; @; *; /2/
+##| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv';
+    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
+    nrewrite > DIVIDES; #H'; 
+    ndestruct;
 ##] nqed.
 
 ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
-#p;#q;napply dec_divides; nqed.
-
+#p;#q;ncases p;
+##[ ncases q; nnormalize; ##[ @2; /2/; ##| ##*: #m; @2; /2/; ##]
+##| ##*: #n; ncases q; nnormalize; /2/;
+##] nqed.
+
+ndefinition natp_to_Z ≝
+λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
+
+ndefinition natp_to_negZ ≝
+λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].
 
 (* TODO: check these definitions are right.  They are supposed to be the same
    as Zdiv/Zmod in Coq. *)
 ndefinition divZ ≝ λx,y.
-  match divide (abs x) (abs y) with
-  [ mk_pair q r ⇒
-    match x with
+  match x with
+  [ OZ ⇒ OZ
+  | pos n ⇒
+    match y with
     [ OZ ⇒ OZ
-    | pos m ⇒
-      match y with
-      [ OZ ⇒ OZ
-      | pos n ⇒ q
-      | neg n ⇒ match r with [ O ⇒ -q | _ ⇒ -(S q) ]
-      ]
-    | neg m ⇒
-      match y return λ_.Z with
-      [ OZ ⇒ OZ
-      | pos n ⇒ match r with [ O ⇒ -q | _ ⇒ -(S q) ]
-      | neg n ⇒ q
-      ]
+    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
+    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
+                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
+    ]
+  | neg n ⇒
+    match y with
+    [ OZ ⇒ OZ
+    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
+                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
+    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
     ]
   ].
 
 ndefinition modZ ≝ λx,y.
-  match divide (abs x) (abs y) with
-  [ mk_pair q r ⇒
-    match x with
+  match x with
+  [ OZ ⇒ OZ
+  | pos n ⇒
+    match y with
     [ OZ ⇒ OZ
-    | pos m ⇒
-      match y return λ_.Z with
-      [ OZ ⇒ OZ
-      | pos n ⇒ r
-      | neg n ⇒ match r with [ O ⇒ O | _ ⇒ y-r ]
-      ]
-    | neg m ⇒
-      match y return λ_.Z with
-      [ OZ ⇒ OZ
-      | pos n ⇒ match r with [ O ⇒ O | _ ⇒ y+r ]
-      | neg n ⇒ r
-      ]
+    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
+    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
+                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
+    ]
+  | neg n ⇒
+    match y with
+    [ OZ ⇒ OZ
+    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
+                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
+    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
     ]
   ].