Changeset 10


Ignore:
Timestamp:
Jul 6, 2010, 11:53:23 AM (10 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:
3 added
7 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/AST.ma

    r9 r10  
    2121include "Integers.ma".
    2222include "Floats.ma".
     23include "binary/positive.ma".
    2324
    2425(* * * Syntactic elements *)
     
    2627(* * Identifiers (names of local variables, of global symbols and functions,
    2728  etc) are represented by the type [positive] of positive integers. *)
     29
     30ndefinition ident ≝ Pos.
     31
     32ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
     33#x y; nlapply (pos_compare_to_Prop x y); ncases (pos_compare x y);
     34##[ #H; @2; /2/; ##| #H; @1; //; ##| #H; @2; /2/ ##] nqed.
     35
    2836(*
    29 Definition ident := positive.
    30 
    31 Definition ident_eq := peq.
    32 *)
    3337(* XXX: we use nats for now, but if in future we use binary like compcert
    3438        then the maps will be easier to define. *)
     
    4549  ##]
    4650##] nqed.
    47 
     51*)
    4852(* * The intermediate languages are weakly typed, using only two types:
    4953  [Tint] for integers and pointers, and [Tfloat] for floating-point
  • C-semantics/Cexec.ma

    r9 r10  
    429429  on d:decide to ? + (¬?).
    430430
     431ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P.
     432#P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##| napply Error ##] nqed.
     433
     434ncoercion decide_inject2 :
     435  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P ≝ dodecide2
     436  on d:decide to res ?.
     437
    431438alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
    432439alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
     
    438445#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    439446
    440 (* Not very happy about this. *)
    441 nlet rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
     447nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
    442448match t1 with
    443449[ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ]
    444450| 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 ]
    445451| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
    446 | Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
     452| Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
    447453| Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒
    448     match type_eq_dec t t' with [ inl _ ⇒
    449       match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]
    450 | Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match typelist_eq_dec tl tl' with [ inl _ ⇒
    451     match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]
     454    match assert_type_eq t t' with [ OK _ ⇒
     455      match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
     456| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒
     457    match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
    452458| Tstruct i fl ⇒
    453459    match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
    454       match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
     460      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
    455461| Tunion i fl ⇒
    456462    match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
    457       match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
     463      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] |  _ ⇒ dn ]
    458464| Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
    459465]
    460 and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
     466and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝
    461467match tl1 with
    462468[ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ]
    463469| Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒
    464     match type_eq_dec t1 t2 with [ inl _ ⇒
    465       match typelist_eq_dec ts1 ts2 with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
     470    match assert_type_eq t1 t2 with [ OK _ ⇒
     471      match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
    466472]
    467 and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
     473and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝
    468474match fl1 with
    469475[ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ]
    470476| Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒
    471477    match ident_eq i1 i2 with [ inl _ ⇒
    472       match type_eq_dec t1 t2 with [ inl _ ⇒
    473         match fieldlist_eq_dec fs1 fs2 with [ inl _ ⇒ dy | _ ⇒ dn ]
     478      match assert_type_eq t1 t2 with [ OK _ ⇒
     479        match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy | _ ⇒ dn ]
    474480        | _ ⇒ dn ] | _ ⇒ dn ] ]
    475481].
    476482(* A poor man's clear, otherwise automation picks up recursive calls without
    477483   checking that the argument is smaller. *)
    478 ngeneralize in type_eq_dec;
    479 ngeneralize in typelist_eq_dec;
    480 ngeneralize in fieldlist_eq_dec; #avoid1 avoid2 avoid3 avoid4 avoid5 avoid6;
    481 ndestruct; //; @; #H; ndestruct;
    482 ##[ nelim c8; /2/
    483 ##| nelim c6; /2/
    484 ##| nelim c4; /2/
    485 ##| nelim c4; /2/
    486 ##| nelim c8; /2/
    487 ##| nelim c6; /2/
    488 ##| nelim c8; /2/
    489 ##| nelim c6; /2/
    490 ##| nelim c8; /2/
    491 ##| nelim c6; /2/
    492 ##| nelim c8; /2/
    493 ##| nelim c6; /2/
    494 ##| nelim c4; /2/
    495 ##| nelim c8; /2/
    496 ##| nelim c6; /2/
    497 ##| nelim c12; /2/
    498 ##| nelim c10; /2/
    499 ##| nelim c8; /2/
    500 ##] nqed.
    501 
    502 ndefinition are_equal : ∀A:Type. (∀x,y:A.(x=y)+(x≠y)) → ∀x,y:A. res (x=y) ≝
    503 λA,dec,x,y.
    504 match dec … x y with
    505 [ inl p ⇒ OK ? p
    506 | inr _ ⇒ Error ?
    507 ].
     484ngeneralize in assert_type_eq;
     485ngeneralize in assert_typelist_eq;
     486ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //;
     487(* XXX: I have no idea why the first // didn't catch these. *)
     488//; //; //; //; //; //; //; //; //;
     489nqed.
    508490
    509491nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
     
    527509    vargs ← exec_exprlist ge e m al;:
    528510    fd ← opt_to_res ? (find_funct Genv ? ge vf);:
    529     p ← are_equal ? type_eq_dec (type_of_fundef fd) (typeof a);:
     511    p ← assert_type_eq (type_of_fundef fd) (typeof a);:
    530512    k' ← match lhs with
    531513         [ None ⇒ OK ? (Kcall (None ?) f e k)
  • C-semantics/Coqlib.ma

    r3 r10  
    1818    library. *)
    1919
    20 include "arithmetics/Z.ma".
     20include "binary/Z.ma".
    2121include "datatypes/sums.ma".
    2222include "datatypes/list.ma".
     
    347347  auto.
    348348Qed.
    349 
    350 (** Properties of powers of two. *)
    351 
    352 Lemma two_power_nat_O : two_power_nat O = 1.
    353 Proof. reflexivity. Qed.
    354 
    355 Lemma two_power_nat_pos : forall n : nat, two_power_nat n > 0.
    356 Proof.
    357   induction n. rewrite two_power_nat_O. omega.
    358   rewrite two_power_nat_S. omega.
    359 Qed.
    360 
    361 Lemma two_power_nat_two_p:
    362   forall x, two_power_nat x = two_p (Z_of_nat x).
    363 Proof.
    364   induction x. auto.
    365   rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega.
    366 Qed.
    367 
     349*)
     350(* * Properties of powers of two. *)
     351
     352nlemma two_power_nat_O : two_power_nat O = one.
     353//; nqed.
     354
     355nlemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0.
     356//; nqed.
     357
     358nlemma two_power_nat_two_p:
     359  ∀x. Z_two_power_nat x = two_p (Z_of_nat x).
     360#x; ncases x;
     361##[ //;
     362##| nnormalize; #p; nelim p; //; #p' H; nrewrite > (nat_succ_pos …); //;
     363##] nqed.
     364(*
    368365Lemma two_p_monotone:
    369366  forall x y, 0 <= x <= y -> two_p x <= two_p y.
     
    577574(* * Alignment: [align n amount] returns the smallest multiple of [amount]
    578575  greater than or equal to [n]. *)
    579 naxiom align : Z → Z → Z.
    580 (*
     576(*naxiom align : Z → Z → Z.*)
     577
    581578ndefinition align ≝ λn: Z. λamount: Z.
    582579  ((n + amount - 1) / amount) * amount.
    583 
     580(*
    584581Lemma align_le: forall x y, y > 0 -> x <= align x y.
    585582Proof.
  • C-semantics/Integers.ma

    r9 r10  
    1717
    1818include "arithmetics/nat.ma".
    19 include "arithmetics/Z.ma".
     19include "binary/Z.ma".
    2020include "extralib.ma".
    2121
     
    6262*)
    6363
    64 naxiom two_power_nat : nat → Z.
     64(*naxiom two_power_nat : nat → Z.*)
    6565
    6666ndefinition wordsize : nat ≝ 32.
    67 ndefinition modulus : Z ≝ two_power_nat wordsize.
     67ndefinition modulus : Z ≝ Z_two_power_nat wordsize.
    6868ndefinition half_modulus : Z ≝ modulus / 2.
    6969ndefinition max_unsigned : Z ≝ modulus - 1.
     
    7575nnormalize; //; nqed.
    7676
    77 (*
    78 Remark modulus_power:
     77nremark modulus_power:
    7978  modulus = two_p (Z_of_nat wordsize).
    80 Proof.
    81   unfold modulus. apply two_power_nat_two_p.
    82 Qed.
    83 
    84 Remark modulus_pos:
     79//; nqed.
     80
     81nremark modulus_pos:
    8582  modulus > 0.
    86 Proof.
    87   rewrite modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega.
    88 Qed.
    89 *)
     83//; nqed.
     84
    9085(* * Representation of machine integers *)
    9186
  • C-semantics/Maps.ma

    r3 r10  
    172172*)
    173173
    174 naxiom PTree : TREE ident.
     174(* XXX: need real tree impl *)
     175nlet rec assoc_get (A:Type) (i:ident) (l:list (ident × A)) on l ≝
     176match l with
     177[ nil ⇒ None ?
     178| cons h t ⇒
     179  match h with [ mk_pair hi ha ⇒
     180    match ident_eq i hi with [ inl _ ⇒ Some ? ha | inr _ ⇒ assoc_get A i t ] ]
     181].
     182
     183naxiom assoc_tree_eq: ∀A: Type. ∀x,y: A. (x=y) + (x≠y) →
     184      ∀a,b: list (ident × A). (a = b) + (a ≠ b).
     185naxiom assoc_remove: ∀A: Type. ident → list (ident × A) → list (ident × A).
     186naxiom assoc_tree_map: ∀A,B: Type. (ident → A → B) → list (ident × A) → list (ident × B).
     187naxiom assoc_elements: ∀A: Type. list (ident × A) → list (ident × A).
     188naxiom assoc_tree_fold: ∀A,B: Type. (B → ident → A → B) → list (ident × A) → B → B.
     189
     190ndefinition PTree : TREE ident ≝
     191mk_TREE ?
     192  ident_eq
     193  (λA. list (ident × A))
     194  assoc_tree_eq
     195  (λA. nil ?)
     196  assoc_get
     197  (λA,i,a,l.〈i,a〉::l)
     198  assoc_remove
     199  assoc_tree_map
     200  assoc_elements
     201  assoc_tree_fold.
    175202
    176203(*
  • C-semantics/Mem.ma

    r9 r10  
    2525*)
    2626
    27 include "arithmetics/Z.ma".
     27include "arithmetics/nat.ma".
     28include "binary/Z.ma".
    2829include "datatypes/sums.ma".
    2930include "datatypes/list.ma".
     
    127128  | Mfloat64 => 7].
    128129
     130alias symbol "plus" (instance 2) = "integer plus".
    129131nlemma size_chunk_pred:
    130132  ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk.
     
    164166nlemma align_size_chunk_divides:
    165167  ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
    166 #chunk;ncases chunk;nnormalize;@;//;##[ napply 2; ##| // ##]
     168#chunk;ncases chunk;nnormalize;/3/;
    167169nqed.
    168170
     
    176178(* The initial store. *)
    177179
    178 ndefinition oneZ ≝ pos O.
     180ndefinition oneZ ≝ pos one.
    179181
    180182nremark one_pos: OZ < oneZ.
     
    186188
    187189ndefinition empty: mem ≝
    188   mk_mem (λx.empty_block OZ OZ) (pos O) one_pos.
     190  mk_mem (λx.empty_block OZ OZ) (pos one) one_pos.
    189191
    190192ndefinition nullptr: block ≝ OZ.
     
    501503nchange in ⊢ (??(???%)?) with (update ????);
    502504nwhd in ⊢(??%?);nrewrite > (update_s content …);
    503 nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false …);//;napply sym_neq;//;
     505nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false … (sym_neq … H));//;
    504506nqed.
    505507
     
    512514nlapply (eqZb_to_Prop p1 p2); ncases (eqZb p1 p2); #Hp;
    513515##[nrewrite > Hp;
    514    nlapply (eqb_to_Prop n1 n2);ncases (eqb n1 n2); #Hn;
     516   napply (eqb_elim n1 n2); #Hn;
    515517   ##[nrewrite > Hn;@; @; //;
    516518   ##|@2;/2/]
     
    10551057##|nrewrite > (size_chunk_pred …) in H1;nrewrite > (size_chunk_pred …);
    10561058   #H1;napply nmk;#Hfalse;nelim H1;#H4;napply H4;
    1057    napply (eq_f ?? (λx.Z_of_nat (1 + x)) ???);//##]
     1059   napply (eq_f ?? (λx.1 + x) ???);//##]
    10581060nqed.
    10591061
     
    15821584    ##| napply (Zleb_true_to_Zle … H2)
    15831585    ##| nwhd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon
    1584     ##| napply (witness ?? (abs ofs)); nnormalize; nrewrite > (Zplus_z_OZ ?); //
     1586    ##| ncases ofs; /2/;
    15851587    ##]
    15861588##| *; #Hval;#Hlo;#Hhi;#Hal;
     
    16991701##| #ineq; @1; @1; napply ineq;
    17001702##] nqed.
    1701 
     1703(*  XXX: reenable once I've sorted out performance a bit
    17021704ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem.
    17031705  ∀b1,b1',delta1,b2,b2',delta2.
     
    23652367    ##]
    23662368##] nqed.
    2367 (*  XXX: reenable once I've sorted out Integers.ma a bit
     2369
    23682370nlemma valid_pointer_inject_no_overflow:
    23692371  ∀f,m1,m2,b,ofs,b',x.
  • C-semantics/extralib.ma

    r3 r10  
    1313(**************************************************************************)
    1414
    15 include "arithmetics/Z.ma".
    1615include "datatypes/sums.ma".
    1716include "datatypes/list.ma".
    1817include "Plogic/equality.ma".
     18include "binary/Z.ma".
     19include "binary/positive.ma".
    1920
    2021nlemma eq_rect_Type0_r:
     
    6162
    6263(* XXX: divides goes to arithmetics *)
    63 ninductive divides (n,m:nat) : Prop ≝
    64 | witness : ∀p:nat.m = times n p → divides n m.
    65 interpretation "divides" 'divides n m = (divides n m).
    66 interpretation "not divides" 'ndivides n m = (Not (divides n m)).
    67 
    68 ndefinition dividesZ ≝ λx,y:Z. abs x ∣ abs y.
     64ninductive dividesP (n,m:Pos) : Prop ≝
     65| witness : ∀p:Pos.m = times n p → dividesP n m.
     66interpretation "positive divides" 'divides n m = (dividesP n m).
     67interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)).
     68
     69ndefinition dividesZ : Z → Z → Prop ≝
     70λx,y. match x with
     71[ OZ ⇒ False
     72| pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
     73| neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
     74].
     75
    6976interpretation "integer divides" 'divides n m = (dividesZ n m).
    7077interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)).
    7178
    7279(* should be proved in nat.ma, but it's not! *)
    73 naxiom eqb_to_Prop : ∀n,m.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     80naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     81
     82nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     83#n m; napply eqb_elim; //; nqed.
    7484
    7585nlemma injective_Z_of_nat : injective ? ? Z_of_nat.
     
    7787#n;#m;ncases n;ncases m;nnormalize;//;
    7888##[ ##1,2: #n';#H;ndestruct
    79 ##| #n';#m'; #H; ndestruct; //
     89##| #n';#m'; #H; ndestruct; nrewrite > (succ_pos_of_nat_inj … e0); //
    8090##] nqed.
    8191
     
    92102nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
    93103#x;#y;
    94 #n;
    95 nelim n; ##[ ##2: #n'; #IH; ##]
     104napply pos_elim
     105 ##[ ##2: #n'; #IH; ##]
    96106nrewrite > (Zplus_Zsucc_Zpred y ?);
    97 nwhd in ⊢ (?→??(??%));
    98 ##[ #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);
     107##[ nrewrite > (Zpred_Zsucc (pos n'));
     108 #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);
    99109    napply Zsucc_le;
    100110##| #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le;
     
    115125/3/; #H; nrewrite > H; //; nqed.
    116126
     127ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
     128#x y; ncases x;
     129##[ ncases y;
     130  ##[ ##1,2: //
     131  ##| #n; napply False_ind;
     132  ##]
     133##| #n; ncases y;
     134  ##[ nnormalize; napply False_ind;
     135  ##| #m; napply (pos_cases … n); /2/;
     136  ##| #m; nnormalize; napply False_ind;
     137  ##]
     138##| #n; ncases y; /2/;
     139##] nqed.
     140   
    117141ntheorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
    118 #n;#m;#p; nlapply (Z_compare_to_Prop n p); nelim (Z_compare n p);
    119 ##[ //;
    120 ##| #H; nrewrite > H; #A;#B; napply False_ind; nlapply (Zlt_to_Zle … A);
    121     #C; nlapply (transitive_Zle … C B); nelim p; /2/; #n';nelim n'; /2/;
    122 ##| #A; #B; #C; nlapply (transitive_Zlt … A B); #D;
    123     napply False_ind; nlapply (Zlt_to_Zle … D);
    124     #E; nlapply (transitive_Zle … E C); nelim p; /2/; #n';nelim n'; /2/;
    125 ##] nqed.
    126 
    127 nlemma decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
     142#n m p Hlt Hle; nrewrite < (Zpred_Zsucc n); napply Zle_to_Zlt;
     143napply (transitive_Zle … Hle); /2/;
     144nqed.
     145
     146ndefinition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
    128147#z1;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H;
    129148##[@;//
     
    180199    match y with
    181200    [ OZ ⇒ false
    182     | pos m ⇒ leb (S n) m
     201    | pos m ⇒ leb (succ n) m
    183202    | neg m ⇒ false ]
    184203  | neg n ⇒
     
    186205    [ OZ ⇒ true
    187206    | pos m ⇒ true
    188     | neg m ⇒ leb (S m) n ]].
     207    | neg m ⇒ leb (succ m) n ]].
    189208
    190209
     
    205224
    206225ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
    207 #n;#m;ncases n;ncases m; nnormalize; /2/;
     226#n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct;
    208227nqed.
    209228
     
    225244
    226245ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
    227 #n;#m;ncases n;ncases m; nnormalize; /2/;
    228 ##[ #n';#m';ncases n';nnormalize;
    229   ##[ ##2: #n';#H; napply not_le_to_not_le_S_S; napply leb_false_to_not_le; ##]
    230   //;
    231 ##| #n';#m';ncases m';nnormalize;
    232   ##[ ##2: #m';#H; napply not_le_to_not_le_S_S; napply leb_false_to_not_le; ##]
    233   //;
    234 ##] nqed.
     246#n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct;
     247nqed.
    235248
    236249ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
     
    258271
    259272(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
    260 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 }.
    261 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 }.
     273notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
     274notation < "'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 }.
    262275interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
    263276
     
    280293(* division *)
    281294
    282 nlet rec divide_aux (b,m,n,p:nat) on b ≝
    283   if leb (S m) n then 〈p,m〉 else
    284   match b with
    285   [ O ⇒ 〈p,m〉
    286   | S b' ⇒ divide_aux b' (m-n) n (S p)
    287   ].
    288 
    289 ndefinition divide ≝ λm,n. divide_aux m m n O.
     295ninductive natp : Type ≝
     296| pzero : natp
     297| ppos  : Pos → natp.
     298
     299ndefinition natp0 ≝
     300λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
     301
     302ndefinition natp1 ≝
     303λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
     304
     305nlet rec divide (m,n:Pos) on m ≝
     306match m with
     307[ one ⇒
     308  match n with
     309  [ one ⇒ 〈ppos one,pzero〉
     310  | _ ⇒ 〈pzero,ppos one〉
     311  ]
     312| p0 m' ⇒
     313  match divide m' n with
     314  [ mk_pair q r ⇒
     315    match r with
     316    [ pzero ⇒ 〈natp0 q,pzero〉
     317    | ppos r' ⇒
     318      match partial_minus (p0 r') n with
     319      [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉
     320      | MinusZero ⇒ 〈natp1 q, pzero〉
     321      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
     322      ]
     323    ]
     324  ]
     325| p1 m' ⇒
     326  match divide m' n with
     327  [ mk_pair q r ⇒
     328    match r with
     329    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
     330    | ppos r' ⇒
     331      match partial_minus (p1 r') n with
     332      [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉
     333      | MinusZero ⇒ 〈natp1 q, pzero〉
     334      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
     335      ]
     336    ]
     337  ]
     338].
     339
    290340ndefinition div ≝ λm,n. fst ?? (divide m n).
    291341ndefinition mod ≝ λm,n. snd ?? (divide m n).
     
    306356nqed.
    307357
    308 nlemma minus_plus_distrib: ∀n,m,p. m-(n+p) = m-n-p.
    309 #n;nelim n; //; #n';#IH;#m;#p;nnormalize;
    310 nelim m; //; nqed.
     358nlemma pred_minus: ∀n,m. pred n - m = pred (n-m).
     359napply pos_elim; /3/;
     360nqed.
     361
     362nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
     363napply pos_elim;
     364##[ //
     365##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/;
     366##] nqed.
    311367
    312368ntheorem plus_minus_r:
    313 ∀m,n,p:nat. m ≤ n → p+(n-m) = (p+n)-m.
     369∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
    314370#m;#n;#p;#le;nrewrite > (symmetric_plus …);
    315371nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.
    316372
    317 nlemma plus_minus_le: ∀m,n,p. m≤n → m+p-n≤p.
     373nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
    318374#m;#n;#p;nelim m;/2/; nqed.
    319 
     375(*
    320376nlemma le_to_minus: ∀m,n. m≤n → m-n = 0.
    321377#m;#n;nelim n;
     
    324380    nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/
    325381##] nqed.
    326 
    327 nlemma minus_times_distrib_l: ∀n,m,p:nat. p*m-p*n = p*(m-n).
    328 #n;#m;#p;nelim (decidable_le n m);#le;
    329 ##[ nelim p; //;#p'; #IH; nnormalize; nrewrite > (minus_plus_distrib …);
    330     nrewrite < (plus_minus … le); nrewrite < IH;
     382*)
     383nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
     384#n;#m;#p;(*nelim (decidable_lt n m);*)#lt;
     385(*##[*) napply (pos_elim … p); //;#p'; #IH;
     386    nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);
     387    nrewrite > (minus_plus_distrib …);
     388    nrewrite < (plus_minus … lt); nrewrite < IH;
    331389    nrewrite > (plus_minus_r …); /2/;
    332 ##|
    333 nlapply (not_le_to_lt … le); #lt;
    334 nelim p; //; #p';
    335  ncut (m-n = 0); ##[ /3/ ##]
    336   #mn; nrewrite > mn; nrewrite < (times_n_O …); #H;
    337   nnormalize; napply sym_eq; napply  le_n_O_to_eq; nrewrite < H;
     390nqed.
     391(*##|
     392nlapply (not_lt_to_le … lt); #le;
     393napply (pos_elim … p); //; #p';
     394 ncut (m-n = one); ##[ /3/ ##]
     395  #mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …);
     396  #H; nrewrite < H in ⊢ (???%);
     397  napply sym_eq; napply  le_n_one_to_eq; nrewrite < H;
    338398  nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l;
    339399  /2/;
     
    346406napply False_ind; napply (absurd ? H ( not_le_Sn_n n));
    347407nqed.
    348 
    349 nlemma divide_aux_ok : ∀b,m,n,p,dv,md:nat.
    350  n > 0 → b ≥ m →
    351  divide_aux b m n p = 〈dv,md〉 →
    352  m + p*n = dv*n + md ∧ md < n.
    353 #b;nelim b;
    354 ##[ #m;#n;#p;#dv;#md;#npos;#bound;
    355     nwhd in ⊢ (??%% → ?); nelim (leb (S m) n); nwhd in ⊢ (??%% → ?); #H;
    356     ndestruct;
    357     @; /2/
    358 ##| #b';#IH;#m;#n;#p;#dv;#md;
    359  #npos; #bound; nwhd in ⊢ (??%? → ?); napply leb_elim;
    360   ##[ #Hlt; nwhd in ⊢ (??%? → ?); #H;
    361     ndestruct;
    362     /2/;
    363   ##| #Hnlt; ncut (n≤m); ##[ nlapply (not_le_to_lt … Hnlt); /2/; ##]
    364       #Hnm; nwhd in ⊢ (??%? → ?); #H;
    365       nlapply (IH … H); ##[ napply le_S_S_to_le; napply (transitive_le ? m);  //;
    366                             nrewrite < (minus_Sn_m …); //; napply (lt_O_n_elim …npos); #n';
    367                             nrewrite > (minus_S_S …); /2/;
    368                         ##| //
    369                         ##| nnormalize; nrewrite < (associative_plus …); nrewrite < (plus_minus_m_m …); //;
    370                         ##]
    371   ##] nqed.
    372 
    373 ntheorem divide_divides: ∀m,n,dv,md:nat.
    374  n > 0 → divide m n = 〈dv,md〉 → m = dv * n + md ∧ md < n.
    375 #m;#n;#dv;#md;#npos; nwhd in ⊢ (??%? → ?); #DIVIDE;
    376 nlapply (divide_aux_ok … DIVIDE); //; nqed.
    377 
    378 nlemma mod0_divides: ∀m,n,dv:nat.
    379   m>0 → divide n m = 〈dv,O〉 → m∣n.
    380 #m;#n;#dv;#mpos;#DIVIDE;@ dv; nlapply (divide_divides … DIVIDE); //; *; //;
    381 nqed.
    382 
    383 nlemma divides_mod0: ∀dv,m,n:nat.
    384   m>0 → n = dv*m → divide n m = 〈dv,O〉.
    385 #dv;#m;#n;#mpos;#DIV;nlapply (refl ? (divide n m));
    386 nelim (divide n m) in ⊢ (???% → ?); #dv';#md'; #DIVIDE;
    387 nlapply (divide_divides … mpos DIVIDE); *;
    388 nrewrite > DIV in ⊢ (% → ?); #H; nlapply (plus_to_minus … H);
    389 nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv' …);
    390 nrewrite > (minus_times_distrib_l …);
    391 nelim (decidable_le dv dv');
    392 ##[ #le; ncut (dv-dv' = 0); ##[ /2/ ##]
    393     #eq; nrewrite > eq; nrewrite < (times_n_O …); #md0; #_;
    394     nrewrite > DIVIDE; nrewrite < md0 in H ⊢ %; nrewrite < (plus_n_O …);
    395     #H; ncut (dv = dv');  ##[ napply le_to_le_to_eq; //;
    396     napply (le_times_to_le m); //; ##]
    397      //;
    398 ##| #nle; ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
    399     #Hdv; #H; ncut (md' ≥ m); /2/; #A;#B; napply False_ind;
    400     napply (absurd ? A (lt_to_not_le … B));
    401 ##] nqed.
    402 
    403 nlemma dec_divides_1: ∀m,n:nat. m>0 → (m∣n) + ¬(m∣n).
    404 #m;#n;#mpos; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
    405 #dv;#md; ncases md;
    406 ##[ #H; @1; napply mod0_divides; //;
     408*)
     409
     410nlet rec natp_plus (n,m:natp) ≝
     411match n with
     412[ pzero ⇒ m
     413| ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]
     414].
     415
     416nlet rec natp_times (n,m:natp) ≝
     417match n with
     418[ pzero ⇒ pzero
     419| ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]
     420].
     421
     422ninductive natp_lt : natp → Pos → Prop ≝
     423| plt_zero : ∀n. natp_lt pzero n
     424| plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.
     425
     426nlemma lt_p0: ∀n:Pos. one < p0 n.
     427#n; nnormalize; /2/; nqed.
     428
     429nlemma lt_p1: ∀n:Pos. one < p1 n.
     430#n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed.
     431
     432nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
     433#m; nelim m;
     434##[ //;
     435##| ##2,3: #m' IH; nnormalize; nrewrite > IH; //;
     436##] nqed.
     437
     438nlemma 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).
     439#n P Q; napply succ_elim; /2/; nqed.
     440
     441nlemma partial_minus_to_Prop: ∀n,m.
     442  match partial_minus n m with
     443  [ MinusNeg ⇒ n < m
     444  | MinusZero ⇒ n = m
     445  | MinusPos r ⇒ n = m+r
     446  ].
     447#n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m);
     448nnormalize; ncases (partial_minus n m); /2/; nqed.
     449
     450nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
     451#n m lt; nelim lt; /2/;
     452nqed.
     453
     454nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
     455#n m lt; napply (transitive_lt ? (p0 m) ?); /2/;
     456nqed.
     457
     458nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
     459#n m lt; ninversion lt;
     460##[ #H; nrewrite > (succ_injective … H); //;
     461##| #p H1 H2 H3;nrewrite > (succ_injective … H3);
     462    napply (transitive_lt ? (p0 p) ?); /2/;
     463##]
     464nqed.
     465
     466nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
     467#n m lt; nelim lt; /2/;
     468nqed.
     469
     470
     471
     472nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
     473#n m lt;ninversion lt;
     474##[ #p H; ndestruct;
     475##| #n' m' lt e1 e2; ndestruct; //;
     476##] nqed.
     477
     478nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
     479#a b; /2/; nqed.
     480
     481nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
     482#a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed.
     483
     484nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
     485/2/; nqed.
     486
     487nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
     488#A B a1 a2 b1 b2 H; ndestruct; //;
     489nqed.
     490
     491nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
     492#A B a1 a2 b1 b2 H; ndestruct; //;
     493nqed.
     494
     495ntheorem divide_ok : ∀m,n,dv,md.
     496 divide m n = 〈dv,md〉 →
     497 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
     498#m n; napply (pos_cases … n);
     499##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/;
     500##| #n'; nelim m;
     501  ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
     502  ##| #m' IH dv md; nnormalize;
     503      nlapply (refl ? (divide m' (succ n')));
     504      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
     505      #dv' md' DIVr; nelim (IH … DIVr);
     506      nnormalize; ncases md';
     507      ##[ ncases dv'; nnormalize;
     508        ##[ #H; ndestruct;
     509        ##| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
     510        ##]
     511      ##| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
     512          nnormalize; #n md'' Hr1 Hr2;
     513          nlapply (plt_lt … Hr2); #Hr2';
     514          nlapply (partial_minus_to_Prop md'' n);
     515          ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize;
     516          #lt; #e; ndestruct; @; /2/; napply plt_pos;
     517          ##[ ##1,3,5,7: napply double_lt1; /2/;
     518          ##| ##2,4: napply double_lt3; /2/;
     519          ##| ##*: napply double_lt2; /2/;
     520          ##]
     521      ##]
     522  ##| #m' IH dv md; nwhd in ⊢ (??%? → ?);
     523      nlapply (refl ? (divide m' (succ n')));
     524      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
     525      #dv' md' DIVr; nelim (IH … DIVr);
     526      nwhd in ⊢ (? → ? → ??%? → ?); ncases md';
     527      ##[ ncases dv'; nnormalize;
     528        ##[ #H; ndestruct;
     529        ##| #dv'' Hr1 Hr2; #H; ndestruct; /3/;
     530        ##]
     531      ##| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
     532          nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2;
     533          nlapply (plt_lt … Hr2); #Hr2';
     534          nwhd in ⊢ (??%? → ?);
     535          nlapply (partial_minus_to_Prop (p0 md'') (succ n'));
     536          ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##]
     537          ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize;
     538          #Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##]
     539          #lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##]
     540          nrewrite < (pair_eq1 … e); nrewrite < (pair_eq2 … e);
     541          nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos;
     542          ##[ ncut (succ n' + r'' < p0 (succ n')); /2/;
     543          ##| ncut (succ n' + r'' < p0 (succ n')); /2/;
     544          ##| /2/;
     545          ##| /2/;
     546          ##]
     547      ##]
     548  ##]
     549##] nqed.
     550
     551nlemma mod0_divides: ∀m,n,dv:Pos.
     552  divide n m = 〈ppos dv,pzero〉 → m∣n.
     553#m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *;
     554nnormalize; #H; ndestruct; //;
     555nqed.
     556
     557nlemma divides_mod0: ∀dv,m,n:Pos.
     558  n = dv*m → divide n m = 〈ppos dv,pzero〉.
     559#dv;#m;#n;#DIV;nlapply (refl ? (divide n m));
     560nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE;
     561nlapply (divide_ok … DIVIDE); *;
     562ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##]
     563ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE;  nnormalize;
     564nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct;
     565##[ nlapply (plus_to_minus … e0);
     566    nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …);
     567    ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt;
     568    nrewrite > (minus_times_distrib_l …); //;
     569
     570 (*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
     571    #Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind;
     572    napply (absurd ? B (lt_to_not_le … A));
     573
     574##| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/;
     575
     576##| nrewrite > DIVIDE; ncut (dv = dv''); /2/;
     577##]
     578nqed.
     579
     580nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
     581#m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
     582#dv;#md; ncases md; ncases dv;
     583##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct
     584##| #dv'; #H; @1; napply mod0_divides; /2/;
    407585##| #md'; #DIVIDES; @2; napply nmk; *; #dv';
    408     nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); //;
     586    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
    409587    nrewrite > DIVIDES; #H';
    410588    ndestruct;
    411 ##] nqed.
    412 
    413 nlemma dec_divides: ∀m,n:nat. (m∣n) + ¬(m∣n).
    414 #m;#n; ncases m; /2/;
    415 ncases n;
    416 ##[ @1; @ O; //;
    417 ##| #n'; @ 2; @; *; /2/
     589##| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv';
     590    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
     591    nrewrite > DIVIDES; #H';
     592    ndestruct;
    418593##] nqed.
    419594
    420595ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
    421 #p;#q;napply dec_divides; nqed.
    422 
     596#p;#q;ncases p;
     597##[ ncases q; nnormalize; ##[ @2; /2/; ##| ##*: #m; @2; /2/; ##]
     598##| ##*: #n; ncases q; nnormalize; /2/;
     599##] nqed.
     600
     601ndefinition natp_to_Z ≝
     602λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
     603
     604ndefinition natp_to_negZ ≝
     605λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].
    423606
    424607(* TODO: check these definitions are right.  They are supposed to be the same
    425608   as Zdiv/Zmod in Coq. *)
    426609ndefinition divZ ≝ λx,y.
    427   match divide (abs x) (abs y) with
    428   [ mk_pair q r ⇒
    429     match x with
     610  match x with
     611  [ OZ ⇒ OZ
     612  | pos n ⇒
     613    match y with
    430614    [ OZ ⇒ OZ
    431     | pos m ⇒
    432       match y with
    433       [ OZ ⇒ OZ
    434       | pos n ⇒ q
    435       | neg n ⇒ match r with [ O ⇒ -q | _ ⇒ -(S q) ]
    436       ]
    437     | neg m ⇒
    438       match y return λ_.Z with
    439       [ OZ ⇒ OZ
    440       | pos n ⇒ match r with [ O ⇒ -q | _ ⇒ -(S q) ]
    441       | neg n ⇒ q
    442       ]
     615    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
     616    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
     617                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
     618    ]
     619  | neg n ⇒
     620    match y with
     621    [ OZ ⇒ OZ
     622    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
     623                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
     624    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
    443625    ]
    444626  ].
    445627
    446628ndefinition modZ ≝ λx,y.
    447   match divide (abs x) (abs y) with
    448   [ mk_pair q r ⇒
    449     match x with
     629  match x with
     630  [ OZ ⇒ OZ
     631  | pos n ⇒
     632    match y with
    450633    [ OZ ⇒ OZ
    451     | pos m ⇒
    452       match y return λ_.Z with
    453       [ OZ ⇒ OZ
    454       | pos n ⇒ r
    455       | neg n ⇒ match r with [ O ⇒ O | _ ⇒ y-r ]
    456       ]
    457     | neg m ⇒
    458       match y return λ_.Z with
    459       [ OZ ⇒ OZ
    460       | pos n ⇒ match r with [ O ⇒ O | _ ⇒ y+r ]
    461       | neg n ⇒ r
    462       ]
     634    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
     635    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
     636                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
     637    ]
     638  | neg n ⇒
     639    match y with
     640    [ OZ ⇒ OZ
     641    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
     642                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
     643    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
    463644    ]
    464645  ].
Note: See TracChangeset for help on using the changeset viewer.