include "arithmetics/nat.ma". include "basics/list.ma". include "basics/types.ma". definition if_then_else ≝ λA: Type[0]. λb: bool. λt: A. λf: A. 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). let 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 ]. definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝ match l with [ nil ⇒ r | cons h t ⇒ revapp T t (h::r) ]. definition rev ≝ λT:Type[0].λl. revapp T l [ ]. lemma eq_rect_Type0_r : ∀A: Type[0]. ∀a:A. ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. #A #a #P #H #x #p generalize in match H generalize in match P cases p // qed. notation "hvbox(t⌈o ↦ h⌉)" with precedence 45 for @{ match (? : \$o=\$h) with [ refl ⇒ \$t ] }. definition 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). let 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 [ pair \${ident x} \${ident y} ⇒ \$s ] }. notation "⊥" with precedence 90 for @{ match ? in False with [ ] }. let 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 ] ]. definition ltb ≝ λm, n: nat. leb (S m) n. definition geb ≝ λm, n: nat. ltb n m. definition 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). let 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) ] ]. definition 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). let 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 ] ]. definition 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). definition divide_with_remainder ≝ λm, n: nat. pair ? ? (m ÷ n) (modulus m n). let 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). theorem less_than_or_equal_monotone: ∀m, n: nat. m ≤ n → (S m) ≤ (S n). #m #n #H elim H /2/ qed. theorem less_than_or_equal_b_complete: ∀m, n: nat. leb m n = false → ¬(m ≤ n). #m; elim m; normalize [ #n #H destruct | #y #H1 #z cases z normalize [ #H /2/ | /3/ ] ] qed. theorem less_than_or_equal_b_correct: ∀m, n: nat. leb m n = true → m ≤ n. #m elim m // #y #H1 #z cases z normalize [ #H destruct | /3/ ] qed. definition less_than_or_equal_b_elim: ∀m, n: nat. ∀P: bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n). #m #n #P #H1 #H2; lapply (less_than_or_equal_b_correct m n) lapply (less_than_or_equal_b_complete m n) cases (leb m n) /3/ qed.