Changeset 1599


Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

Location:
src
Files:
1 deleted
31 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1485 r1599  
    2222         of add_with_carries *)
    2323     if last_carry then
    24       let bit ≝ exclusive_disjunction (exclusive_disjunction b c) true in
     24      let bit ≝ xorb (xorb b c) true in
    2525      let carry ≝ carry_of b c true in
    2626       〈bit:::lower_bits, carry:::carries〉
    2727     else
    28       let bit ≝ exclusive_disjunction (exclusive_disjunction b c) false in
     28      let bit ≝ xorb (xorb b c) false in
    2929      let carry ≝ carry_of b c false in
    3030       〈bit:::lower_bits, carry:::carries〉     
     
    4343     let 〈lower_bits, borrows〉 ≝ r in
    4444     let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in
    45      let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_borrow in
     45     let bit ≝ xorb (xorb b c) last_borrow in
    4646     let borrow ≝ borrow_of b c last_borrow in
    4747       〈bit:::lower_bits, borrow:::borrows〉
     
    6060    let 〈result, carries〉 ≝ add_with_carries n b c carry in
    6161    let cy_flag ≝ get_index_v ?? carries 0 ? in
    62     let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
     62    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
    6363    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
    6464      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
     
    7676    let 〈result, carries〉 ≝ sub_with_borrows n b c carry in
    7777    let cy_flag ≝ get_index_v ?? carries 0 ? in
    78     let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
     78    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
    7979    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
    8080      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
     
    311311      [ VEmpty ⇒ false
    312312      | VCons _ bwpn _ ⇒
    313         if exclusive_disjunction bwn bwpn then
     313        if xorb bwn bwpn then
    314314          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
    315315        else
     
    349349        let 〈c1,r〉 ≝ d in
    350350          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
    351            (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
     351           (xorb (xorb b1 b2) c1) ::: r〉)
    352352     〈d, [[ ]]〉 ? b c.
    353353   
  • src/ASM/BitVector.ma

    r1521 r1599  
    8787  λb: BitVector n.
    8888  λc: BitVector n.
    89     zip_with ? ? ? n (exclusive_disjunction) b c.
     89    zip_with ? ? ? n xorb b c.
    9090   
    9191interpretation "BitVector exclusive disjunction"
    92   'exclusive_disjunction b c = (exclusive_disjunction ? b c).
     92  'exclusive_disjunction b c = (xorb b c).
    9393   
    9494definition negation_bv ≝
  • src/ASM/JMCoercions.ma

    r1335 r1599  
    11include "basics/jmeq.ma".
    22include "basics/types.ma".
    3 include "basics/list.ma".
     3include "basics/lists/list.ma".
    44
    55definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
  • src/ASM/Status.ma

    r1588 r1599  
    11081108lemma snd_fetch_pseudo_instruction:
    11091109 ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
    1110  #l #ppc whd in ⊢ (??%?); whd in ⊢ (?? match % with [_ ⇒ ?]?); @pair_elim'
    1111  #lft #rgt @pair_elim' #x #y #_ @pair_elim' #a #b #_ normalize #H
    1112  generalize in match (pair_destruct_2 ????? H); normalize #K >K %
     1110 #l #ppc whd in ⊢ (??(???%)?); @pair_elim
     1111 #lft #rgt @pair_elim #x #y #_ #_ %
    11131112qed.
    11141113
  • src/ASM/String.ma

    r698 r1599  
    1 include "basics/list.ma".
     1include "basics/lists/list.ma".
    22
    33include "ASM/Char.ma".
  • src/ASM/Util.ma

    r1598 r1599  
    1 include "basics/list.ma".
     1include "basics/lists/list.ma".
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
    4 
    5 include "utilities/pair.ma".
    64include "ASM/JMCoercions.ma".
    75
     
    649647
    650648   
    651 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
    652  for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
    653 notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp break 'else' \nbsp term 48 f \nbsp)" non associative with precedence 19
    654  for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
    655 
    656649let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
    657650                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
     
    684677    | S o ⇒ f (iterate A f a o)
    685678    ].
    686 
    687 (* Yeah, I probably ought to do something more general... *)
    688 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
    689 with precedence 90 for @{ 'triple $a $b $c}.
    690 interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
    691 
    692 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
    693 with precedence 90 for @{ 'quadruple $a $b $c $d}.
    694 interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
    695 
    696 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
    697  with precedence 10
    698 for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }.
    699 
    700 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
    701  with precedence 10
    702 for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
    703 
    704 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
    705  with precedence 10
    706 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
    707 
    708 axiom pair_elim':
    709   ∀A,B,C: Type[0].
    710   ∀T: A → B → C.
    711   ∀p.
    712   ∀P: A×B → C → Prop.
    713     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
    714       P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
    715 
    716 axiom pair_elim'':
    717   ∀A,B,C,C': Type[0].
    718   ∀T: A → B → C.
    719   ∀T': A → B → C'.
    720   ∀p.
    721   ∀P: A×B → C → C' → Prop.
    722     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
    723       P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
    724 
    725 lemma pair_destruct_1:
    726  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
    727  #A #B #a #b *; /2/
    728 qed.
    729 
    730 lemma pair_destruct_2:
    731  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
    732  #A #B #a #b *; /2/
    733 qed.
    734 
    735 
    736 let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
    737   match b with
    738     [ true ⇒
    739       match c with
    740         [ false ⇒ true
    741         | true ⇒ false
    742         ]
    743     | false ⇒
    744       match c with
    745         [ false ⇒ false
    746         | true ⇒ true
    747         ]
    748     ].
    749 
    750 (* dpm: conflicts with library definitions
    751 interpretation "Nat less than" 'lt m n = (ltb m n).
    752 interpretation "Nat greater than" 'gt m n = (gtb m n).
    753 interpretation "Nat greater than eq" 'geq m n = (geb m n).
    754 *)
    755679
    756680let rec division_aux (m: nat) (n : nat) (p: nat) ≝
     
    891815  elim b
    892816  normalize
    893   [ /2/
     817  [ /2 by conj/
    894818  | # K
    895819    destruct
  • src/ASM/Vector.ma

    r1598 r1599  
    44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    55
    6 include "basics/list.ma".
     6include "basics/lists/list.ma".
    77include "basics/bool.ma".
    88include "basics/types.ma".
  • src/Clight/Cexec.ma

    r1545 r1599  
    145145
    146146definition load_value_of_type' ≝
    147 λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
     147λty,m,l. let 〈loc,ofs〉 ≝ l in load_value_of_type ty m loc ofs.
    148148
    149149axiom BadlyTypedTerm : String.
     
    185185      match ty with
    186186      [ Tpointer r _ ⇒
    187         match lo with [ pair loc ofs ⇒
     187        let 〈loc,ofs〉 ≝ lo in
    188188          match pointer_compat_dec loc r with
    189189          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
    190190          | inr _ ⇒ Error ? (msg TypeMismatch)
    191191          ]
    192         ]
    193192      | _ ⇒ Error ? (msg BadlyTypedTerm)
    194193      ]
     
    294293[ nil ⇒ 〈en, m〉
    295294| cons h vars ⇒
    296   match h with [ pair id ty ⇒
    297     match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒
     295  let 〈id,ty〉 ≝ h in
     296  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) Any in
    298297      exec_alloc_variables (add ?? en id b1) m1 vars
    299 ]]].
     298].
    300299
    301300axiom WrongNumberOfParameters : String.
     
    306305  match params with
    307306  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
    308   | cons idty params' ⇒ match idty with [ pair id ty ⇒
     307  | cons idty params' ⇒ let 〈id,ty〉 ≝ idty in
    309308      match vs with
    310309      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
     
    314313          exec_bind_parameters e m1 params' vl
    315314      ]
    316   ] ].
     315  ].
    317316
    318317let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
     
    338337definition store_value_of_type' ≝
    339338λty,m,l,v.
    340 match l with [ pair loc ofs ⇒
    341   store_value_of_type ty m loc ofs v ].
     339let 〈loc,ofs〉 ≝ l in
     340  store_value_of_type ty m loc ofs v.
    342341
    343342axiom NonsenseState : String.
     
    465464  | Sgoto lbl ⇒
    466465      match find_label lbl (fn_body f) (call_cont k) with
    467       [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
     466      [ Some sk' ⇒ let 〈s',k'〉 ≝ sk' in ret ? 〈E0, State f s' k' e m〉
    468467      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
    469468      ]
     
    473472  match f0 with
    474473  [ CL_Internal f ⇒
    475     match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒
     474    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
    476475      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
    477476      ret ? 〈E0, State f (fn_body f) k e m2〉
    478     ]
    479477  | CL_External f argtys retty ⇒
    480478      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
     
    488486    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
    489487    | Some r' ⇒
    490       match r' with [ pair l ty ⇒
     488      let 〈l,ty〉 ≝ r' in
    491489          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
    492490          ret ? 〈E0, (State f Sskip k' e m')〉
    493       ]
    494491    ]
    495492  | _ ⇒ Wrong ??? (msg NonsenseState)
  • src/Clight/Csyntax.ma

    r1224 r1599  
    327327  match params with
    328328  [ nil ⇒ Tnil
    329   | cons h rem ⇒ match h with [ pair id ty ⇒ Tcons ty (type_of_params rem) ]
     329  | cons h rem ⇒ let 〈id,ty〉 ≝ h in Tcons ty (type_of_params rem)
    330330  ].
    331331
  • src/Clight/casts.ma

    r1516 r1599  
    7676
    7777lemma split_left : ∀A,m,n,h,t.
    78   split A (S m) n (h:::t) = let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉.
     78  split A (S m) n (h:::t) = (let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉).
    7979#A #m #n #h #t normalize >split_eq' @refl
    8080qed.
  • src/Clight/test/search.c.ma

    r1238 r1599  
    215215@refl
    216216qed.
     217
     218example csc: True.
     219letin yyy ≝ (
     220let xxx ≝ (clight_to_cminor myprog) in
     221do p ← xxx ; cminor_to_rtlabs p)
     222normalize in yyy;
     223include "RTLabs/RTLabsToRTL.ma".
     224
     225example csc: True.
     226letin xxx ≝ (clight_to_cminor myprog)
     227letin yyy ≝ (do p ← xxx ; cminor_to_rtlabs p)
     228letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p)
     229@⊥ normalize in xxx;
  • src/Clight/test/sum.test.ma

    r1332 r1599  
    3333@refl
    3434qed.
     35
     36include "RTLabs/RTLabsToRTL.ma".
     37include alias "basics/lists/list.ma".
     38
     39definition take_out: ∀A. res A → A ≝
     40 λA,a. match a with [ OK x ⇒ x | Error _ ⇒ ?].
     41cases daemon
     42qed.
     43
     44example CSC: True.
     45letin xxx ≝
     46 (let p ≝ take_out … (clight_to_cminor myprog) in
     47  let p ≝ take_out … (cminor_to_rtlabs p) in
     48(*   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)) *)
     49  let p ≝ rtlabs_to_rtl p in
     50   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ joint_if_code … f]) (prog_funct … p))
     51 )
     52[2: cases daemon]
     53normalize in xxx;
     54
     55
     56[2:
     57  OK (list (codeT (prog_var_names … p) (rtl_params (prog_var_names … p)))) (list_map … (λx. match (\snd x) return λ_.codeT (prog_var_names … p) (rtl_params ?) with [External _ ⇒ ? | Internal f ⇒ ?(*joint_if_code ? (rtl_params ?) f*)]) (prog_funct … p)))
     58(*  OK ? (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)))
     59*)
     60[2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon  ]
     61normalize in xxx
     62
  • src/Cminor/initialisation.ma

    r1516 r1599  
    44include "Cminor/syntax.ma".
    55include "common/Globalenvs.ma".
    6 include "utilities/pair.ma".
    76include "utilities/deppair.ma".
    87
  • src/Cminor/toRTLabs.ma

    r1521 r1599  
    33include "Cminor/syntax.ma".
    44include "RTLabs/syntax.ma".
    5 include "utilities/pair.ma".
    65include "utilities/deppair.ma".
    76
  • src/common/AssocList.ma

    r789 r1599  
    1 include "basics/list.ma".
     1include "basics/lists/list.ma".
    22
    33definition assoc_list ≝ λA, B. list (A × B).
  • src/common/Errors.ma

    r1598 r1599  
    1616include "basics/types.ma".
    1717include "basics/logic.ma".
    18 include "basics/list.ma".
     18include "basics/lists/list.ma".
    1919include "common/PreIdentifiers.ma".
    2020include "utilities/lists.ma".
  • src/common/Events.ma

    r1516 r1599  
    2222(*include "Floats.ma".*)
    2323include "common/Values.ma".
    24 include "basics/list.ma".
     24include "basics/lists/list.ma".
    2525include "utilities/extralib.ma".
    2626include "common/CostLabel.ma".
     
    161161  match T' with
    162162  [ Econsinf' t T'' NOTEMPTY ⇒
    163       match split_traceinf' t T'' NOTEMPTY with [ pair e tl ⇒
    164       Econsinf e (traceinf_of_traceinf' tl) ]
     163      let 〈e,tl〉 ≝ split_traceinf' t T'' NOTEMPTY in
     164      Econsinf e (traceinf_of_traceinf' tl)
    165165  ].
    166166
  • src/common/Floats.ma

    r961 r1599  
    5959
    6060axiom Fcmp_ne_eq:
    61   ∀ f1,f2. Fcmp Cne f1 f2 = ¬(Fcmp Ceq f1 f2).
     61  ∀ f1,f2. Fcmp Cne f1 f2 = (¬(Fcmp Ceq f1 f2)).
    6262axiom Fcmp_le_lt_eq:
    6363  ∀ f1,f2. Fcmp Cle f1 f2 = (Fcmp Clt f1 f2 ∨ Fcmp Ceq f1 f2).
  • src/common/Globalenvs.ma

    r1583 r1599  
    495495      let init ≝ extract_init init_info in
    496496      let 〈g,st〉 ≝ g_st in
    497         match alloc_init_data st init r with [ pair st' b ⇒
     497        let 〈st',b〉 ≝ alloc_init_data st init r in
    498498          let g' ≝ add_symbol ? id b g in
    499499            〈g', st'〉
    500         ] )
     500        )
    501501    init_env vars.
    502502
  • src/common/IOMonad.ma

    r797 r1599  
    1919match v with
    2020[ Interact out k ⇒ (Interact ??? out (λres. bindIO2 ?? T1 T2 T' (k res) f))
    21 | Value v' ⇒ match v' with [ pair v1 v2 ⇒ f v1 v2 ]
     21| Value v' ⇒ let 〈v1,v2〉 ≝ v' in f v1 v2
    2222| Wrong m ⇒ Wrong ?? T' m
    2323].
  • src/common/Mem.ma

    r1545 r1599  
    2828(*include "binary/Z.ma".*)
    2929(*include "datatypes/sums.ma".*)
    30 (*include "datatypes/list.ma".*)
     30(*include "datatypes/lists/list.ma".*)
    3131(*include "Plogic/equality.ma".*)
    3232
  • src/common/SmallstepExec.ma

    r1233 r1599  
    4747match s with
    4848[ Wrong m ⇒ e_wrong ??? m
    49 | Value v ⇒ match v with [ pair t s' ⇒
     49| Value v ⇒ let 〈t,s'〉 ≝ v in
    5050    match is_final ?? exec g s' with
    5151    [ Some r ⇒ e_stop ??? t r s'
    52     | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] ]
     52    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
    5353| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
    5454].
     
    6565match s with
    6666[ Wrong m ⇒ e_wrong ??? m
    67 | Value v ⇒ match v with [ pair t s' ⇒
     67| Value v ⇒ let 〈t,s'〉 ≝ v in
    6868    match is_final ?? exec g s' with
    6969    [ Some r ⇒ e_stop ??? t r s'
    70     | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] ]
     70    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
    7171| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
    7272].
  • src/joint/BEGlobalenvs.ma

    r1408 r1599  
    447447      let 〈id, r, init〉 ≝ id_init in
    448448      let 〈g,st〉 ≝ g_st in
    449         match alloc_init_data st init r with [ pair st' b ⇒
     449      let 〈st',b〉 ≝ alloc_init_data st init r in
    450450          let g' ≝ add_symbol ? id b g in
    451451            〈g', st'〉
    452         ] )
     452    )
    453453    init_env vars.
    454454
  • src/joint/TranslateUtils.ma

    r1521 r1599  
    2121 #pars0 #globals #def #n elim n
    2222  [ %
    23   | #m whd in ⊢ (? → ??(??%)?); whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) ;
    24     cases (fresh_regs pars0 globals def m) normalize nodelta
    25     #def' #regs #EQ change with (|regs| = m)in EQ; <EQ
    26     @refl
    27  ]
     23  | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
     24    #def' #regs #EQ >EQ  normalize // ]
    2825qed.
    2926
  • src/utilities/Coqlib.ma

    r761 r1599  
    1919
    2020include "basics/types.ma".
    21 include "basics/list.ma".
     21include "basics/lists/list.ma".
    2222
    2323include "ASM/Util.ma".
  • src/utilities/adt/priority_set_adt.ma

    r1223 r1599  
    11include "basics/types.ma".
    2 include "basics/list.ma".
     2include "basics/lists/list.ma".
    33include "arithmetics/nat.ma".
    44include "common/Integers.ma".
  • src/utilities/adt/set_adt.ma

    r1463 r1599  
    11include "basics/types.ma".
    2 include "basics/list.ma".
     2include "basics/lists/list.ma".
    33include "arithmetics/nat.ma".
    44include "ASM/Util.ma".
  • src/utilities/adt/table_adt.ma

    r1296 r1599  
    11include "basics/types.ma".
    22include "basics/bool.ma".
    3 include "basics/list.ma".
     3include "basics/lists/list.ma".
    44
    55include "arithmetics/nat.ma".
  • src/utilities/binary/division.ma

    r1528 r1599  
    5050  ]
    5151| p0 m' ⇒
    52   match divide m' n with
    53   [ pair q r ⇒
     52  let 〈q,r〉 ≝ divide m' n in
    5453    match r with
    5554    [ pzero ⇒ 〈natp0 q,pzero〉
     
    6160      ]
    6261    ]
    63   ]
    6462| p1 m' ⇒
    65   match divide m' n with
    66   [ pair q r ⇒
     63  let 〈q,r〉 ≝ divide m' n in
    6764    match r with
    6865    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
     
    7471      ]
    7572    ]
    76   ]
    7773].
    7874
     
    326322    [ OZ ⇒ OZ
    327323    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
    328     | neg m ⇒ match divide n m with [ pair q r ⇒
    329                 match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
     324    | neg m ⇒ let 〈q,r〉 ≝ divide n m in
     325                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ]
    330326    ]
    331327  | neg n ⇒
    332328    match y with
    333329    [ OZ ⇒ OZ
    334     | pos m ⇒ match divide n m with [ pair q r ⇒
    335                 match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
     330    | pos m ⇒ let 〈q,r〉 ≝ divide n m in
     331                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ]
    336332    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
    337333    ]
     
    345341    [ OZ ⇒ OZ
    346342    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
    347     | neg m ⇒ match divide n m with [ pair q r ⇒
    348                 match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
     343    | neg m ⇒ let 〈q,r〉 ≝ divide n m in
     344                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ]
    349345    ]
    350346  | neg n ⇒
    351347    match y with
    352348    [ OZ ⇒ OZ
    353     | pos m ⇒ match divide n m with [ pair q r ⇒
    354                 match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
     349    | pos m ⇒ let 〈q,r〉 ≝ divide n m in
     350                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ]
    355351    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
    356352    ]
  • src/utilities/extralib.ma

    r1593 r1599  
    1414
    1515include "basics/types.ma".
    16 include "basics/list.ma".
     16include "basics/lists/list.ma".
    1717include "basics/logic.ma".
    18 include "utilities/pair.ma".
    1918include "ASM/Util.ma".
    2019
  • src/utilities/lists.ma

    r1551 r1599  
    1 include "basics/list.ma".
     1include "basics/lists/list.ma".
    22
    33let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
Note: See TracChangeset for help on using the changeset viewer.