include "arithmetics/nat.ma". include "datatypes/pairs.ma". include "datatypes/sums.ma". include "datatypes/list.ma". nlet rec fold_left_i_aux (A: Type[0]) (B: Type[0]) (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝ match l with [ nil ⇒ x | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl ]. ndefinition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. ndefinition function_apply ≝ λA, B: Type[0]. λf: A → B. λa: A. f a. notation "f break \$ x" left associative with precedence 99 for @{ 'function_apply \$f \$x }. interpretation "Function application" 'function_apply f x = (function_apply ? ? f x). nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝ match n with [ O ⇒ a | S o ⇒ f (iterate A f a o) ]. notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" with precedence 10 for @{ match \$t with [ mk_pair \${ident x} \${ident y} ⇒ \$s ] }. notation "⊥" with precedence 90 for @{ match ? in False with [ ] }. nlet rec if_then_else (A: Type[0]) (b: bool) (t: A) (f: A) on b ≝ match b with [ true ⇒ t | false ⇒ f ]. notation "hvbox('if' b 'then' t 'else' f)" non associative with precedence 83 for @{ 'if_then_else \$b \$t \$f }. interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f). nlet rec exclusive_disjunction (b: bool) (c: bool) on b ≝ match b with [ true ⇒ match c with [ false ⇒ true | true ⇒ false ] | false ⇒ match c with [ false ⇒ false | true ⇒ true ] ]. ndefinition ltb ≝ λm, n: nat. leb (S m) n. ndefinition geb ≝ λm, n: nat. ltb n m. ndefinition gtb ≝ λm, n: nat. leb n m. interpretation "Nat less than" 'lt m n = (ltb m n). interpretation "Nat greater than" 'gt m n = (gtb m n). interpretation "Nat greater than eq" 'geq m n = (geb m n). nlet rec division_aux (m: nat) (n : nat) (p: nat) ≝ match ltb n p with [ true ⇒ O | false ⇒ match m with [ O ⇒ O | (S q) ⇒ S (division_aux q (n - (S p)) p) ] ]. ndefinition division ≝ λm, n: nat. match n with [ O ⇒ S m | S o ⇒ division_aux m m o ]. notation "hvbox(n break ÷ m)" right associative with precedence 47 for @{ 'division \$n \$m }. interpretation "Nat division" 'division n m = (division n m). nlet rec modulus_aux (m: nat) (n: nat) (p: nat) ≝ match leb n p with [ true ⇒ n | false ⇒ match m with [ O ⇒ n | S o ⇒ modulus_aux o (n - (S p)) p ] ]. ndefinition modulus ≝ λm, n: nat. match n with [ O ⇒ m | S o ⇒ modulus_aux m m o ]. notation "hvbox(n break 'mod' m)" right associative with precedence 47 for @{ 'modulus \$n \$m }. interpretation "Nat modulus" 'modulus m n = (modulus m n). ndefinition divide_with_remainder ≝ λm, n: nat. mk_pair ? ? (m ÷ n) (modulus m n). nlet rec exponential (m: nat) (n: nat) on n ≝ match n with [ O ⇒ S O | S o ⇒ m * exponential m o ]. interpretation "Nat exponential" 'exp n m = (exponential n m). notation "hvbox(a break ⊎ b)" left associative with precedence 50 for @{ 'disjoint_union \$a \$b }. interpretation "sum" 'disjoint_union A B = (Sum A B). ntheorem less_than_or_equal_monotone: ∀m, n: nat. m ≤ n → (S m) ≤ (S n). #m n H; nelim H; /2/. nqed. ntheorem less_than_or_equal_b_complete: ∀m,n. leb m n = false → ¬(m ≤ n). #m; nelim m; nnormalize [ #n H; ndestruct | #y H1 z; ncases z; nnormalize [ #H; /2/ | /3/ ] nqed. ntheorem less_than_or_equal_b_correct: ∀m,n. leb m n = true → m ≤ n. #m; nelim m; //; #y H1 z; ncases z; nnormalize [ #H; ndestruct | /3/ ] nqed. ndefinition less_than_or_equal_b_elim: ∀m,n. ∀P: bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n). #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n); nlapply (less_than_or_equal_b_complete m n); ncases (leb m n); /3/. nqed.