Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (9 years ago)
Author:
mulligan
Message:

Moved over to standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Util.ma

    r246 r465  
    1 include "Nat.ma".
     1include "arithmetics/nat.ma".
     2include "datatypes/pairs.ma".
     3include "datatypes/sums.ma".
     4include "datatypes/list.ma".
     5
     6nlet rec fold_left_i_aux (A: Type[0]) (B: Type[0])
     7                         (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
     8  match l with
     9    [ nil ⇒ x
     10    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
     11    ].
     12
     13ndefinition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
     14
    215
    316ndefinition function_apply ≝
     
    1326interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
    1427
    15 nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: Nat) on n ≝
     28nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
    1629  match n with
    17     [ Z ⇒ a
     30    [ O ⇒ a
    1831    | S o ⇒ f (iterate A f a o)
    1932    ].
     33   
     34notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     35 with precedence 10
     36for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }.
     37
     38
     39notation "⊥" with precedence 90
     40  for @{ match ? in False with [ ] }.
     41
     42nlet rec if_then_else (A: Type[0]) (b: bool) (t: A) (f: A) on b ≝
     43  match b with
     44    [ true ⇒ t
     45    | false ⇒ f
     46    ].
     47   
     48notation "hvbox('if' b 'then' t 'else' f)"
     49  non associative with precedence 83
     50  for @{ 'if_then_else $b $t $f }.
     51
     52interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
     53
     54nlet rec exclusive_disjunction (b: bool) (c: bool) on b ≝
     55  match b with
     56    [ true ⇒
     57      match c with
     58        [ false ⇒ true
     59        | true ⇒ false
     60        ]
     61    | false ⇒
     62      match c with
     63        [ false ⇒ false
     64        | true ⇒ true
     65        ]
     66    ].
     67
     68ndefinition ltb ≝
     69  λm, n: nat.
     70    leb (S m) n.
     71   
     72ndefinition geb ≝
     73  λm, n: nat.
     74    ltb n m.
     75
     76ndefinition gtb ≝
     77  λm, n: nat.
     78    leb n m.
     79
     80interpretation "Nat less than" 'lt m n = (ltb m n).
     81interpretation "Nat greater than" 'gt m n = (gtb m n).
     82interpretation "Nat greater than eq" 'geq m n = (geb m n).
     83
     84nlet rec division_aux (m: nat) (n : nat) (p: nat) ≝
     85  match ltb n p with
     86    [ true ⇒ O
     87    | false ⇒
     88      match m with
     89        [ O ⇒ O
     90        | (S q) ⇒ S (division_aux q (n - (S p)) p)
     91        ]
     92    ].
     93   
     94ndefinition division ≝
     95  λm, n: nat.
     96    match n with
     97      [ O ⇒ S m
     98      | S o ⇒ division_aux m m o
     99      ].
     100     
     101notation "hvbox(n break ÷ m)"
     102  right associative with precedence 47
     103  for @{ 'division $n $m }.
     104 
     105interpretation "Nat division" 'division n m = (division n m).
     106
     107nlet rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
     108  match leb n p with
     109    [ true ⇒ n
     110    | false ⇒
     111      match m with
     112        [ O ⇒ n
     113        | S o ⇒ modulus_aux o (n - (S p)) p
     114        ]
     115    ].
     116   
     117ndefinition modulus ≝
     118  λm, n: nat.
     119    match n with
     120      [ O ⇒ m
     121      | S o ⇒ modulus_aux m m o
     122      ].
     123   
     124notation "hvbox(n break 'mod' m)"
     125  right associative with precedence 47
     126  for @{ 'modulus $n $m }.
     127 
     128interpretation "Nat modulus" 'modulus m n = (modulus m n).
     129
     130ndefinition divide_with_remainder ≝
     131  λm, n: nat.
     132    mk_pair ? ? (m ÷ n) (modulus m n).
     133   
     134nlet rec exponential (m: nat) (n: nat) on n ≝
     135  match n with
     136    [ O ⇒ S O
     137    | S o ⇒ m * exponential m o
     138    ].
     139
     140interpretation "Nat exponential" 'exp n m = (exponential n m).
     141   
     142notation "hvbox(a break ⊎ b)"
     143 left associative with precedence 50
     144for @{ 'disjoint_union $a $b }.
     145interpretation "sum" 'disjoint_union A B = (Sum A B).
     146
     147ntheorem less_than_or_equal_monotone:
     148  ∀m, n: nat.
     149    m ≤ n → (S m) ≤ (S n).
     150 #m n H; nelim H; /2/.
     151nqed.
     152
     153ntheorem less_than_or_equal_b_complete: ∀m,n. leb m n = false → ¬(m ≤ n).
     154 #m; nelim m; nnormalize
     155  [ #n H; ndestruct | #y H1 z; ncases z; nnormalize
     156    [ #H; /2/ | /3/ ]
     157nqed.
     158
     159ntheorem less_than_or_equal_b_correct: ∀m,n. leb m n = true → m ≤ n.
     160 #m; nelim m; //; #y H1 z; ncases z; nnormalize
     161  [ #H; ndestruct | /3/ ]
     162nqed.
     163
     164ndefinition less_than_or_equal_b_elim:
     165 ∀m,n. ∀P: bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) →
     166  P (leb m n).
     167 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n);
     168 nlapply (less_than_or_equal_b_complete m n);
     169 ncases (leb m n); /3/.
     170nqed.
Note: See TracChangeset for help on using the changeset viewer.