include "basics/list.ma". include "basics/types.ma". include "arithmetics/nat.ma". 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. let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝ match n return λo. o < length A l → A with [ O ⇒ match l return λm. 0 < length A m → A with [ nil ⇒ λabsd1. ? | cons hd tl ⇒ λprf1. hd ] | S n' ⇒ match l return λm. S n' < length A m → A with [ nil ⇒ λabsd2. ? | cons hd tl ⇒ λprf2. safe_nth A n' tl ? ] ] ?. [ 1: @ p | 4: normalize in prf2 normalize @ le_S_S_to_le assumption | 2: normalize in absd1; cases (not_le_Sn_O O) # H elim (H absd1) | 3: normalize in absd2; cases (not_le_Sn_O (S n')) # H elim (H absd2) ] qed. let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝ match n with [ O ⇒ match l with [ nil ⇒ [ ] | cons hd tl ⇒ l ] | S n ⇒ match l with [ nil ⇒ [ ] | cons hd tl ⇒ hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n ] ]. definition nub_by ≝ λA: Type[0]. λf: A → A → bool. λl: list A. nub_by_internal A f l (length ? l). let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝ match l with [ nil ⇒ false | cons hd tl ⇒ orb (eq a hd) (member A eq a tl) ]. let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝ match n with [ O ⇒ [ ] | S n ⇒ match l with [ nil ⇒ [ ] | cons hd tl ⇒ hd :: take A n tl ] ]. let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝ match n with [ O ⇒ l | S n ⇒ match l with [ nil ⇒ [ ] | cons hd tl ⇒ drop A n tl ] ]. definition list_split ≝ λA: Type[0]. λn: nat. λl: list A. 〈take A n l, drop A n l〉. let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B) (l: list A) on l: list B ≝ match l with [ nil ⇒ nil ? | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl) ]. definition mapi ≝ λA, B: Type[0]. λf: nat → A → B. λl: list A. mapi_internal A B 0 f l. let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝ match l with [ nil ⇒ Some ? (nil (A × B)) | cons hd tl ⇒ match r with [ nil ⇒ None ? | cons hd' tl' ⇒ match zip ? ? tl tl' with [ None ⇒ None ? | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail) ] ] ]. let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝ match l with [ nil ⇒ a | cons hd tl ⇒ foldl A B f (f a hd) tl ]. definition flatten ≝ λA: Type[0]. λl: list (list A). foldl ? ? (append ?) [ ] l. definition if_then_else ≝ λA: Type[0]. λb: bool. λt: A. λf: A. match b with [ true ⇒ t | false ⇒ f ]. let rec rev (A: Type[0]) (l: list A) on l ≝ match l with [ nil ⇒ nil A | cons hd tl ⇒ (rev A tl) @ [ hd ] ]. (* notation "hvbox('if' b 'then' t 'else' f)" non associative with precedence 83 for @{ 'if_then_else $b$t $f }. *) notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else$e $t$f }. notation < "'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 }. 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. 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 ] }. (* Yeah, I probably ought to do something more general... *) notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)" with precedence 90 for @{ 'triple$a $b$c}. interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z). notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)" with precedence 10 for @{ match $t with [ pair${fresh xy} ${ident z} ⇒ match${fresh xy} 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. (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *) let rec eq_nat (n: nat) (m: nat) on n: bool ≝ match n with [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ] | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ] ]. (* dpm: conflicts with library definitions 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 (S 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 | #n #H lapply (H1 … H) /2/ ] 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.