include "basics/types.ma". include "arithmetics/nat.ma". include "utilities/option.ma". (* JHM: here, for definiteness; used in ASM/ASM.ma *) let rec nat_bound_opt (N:nat) (n:nat) : option (n < N) ≝ match N return λy. option (n < y) with [ O ⇒ None ? | S N' ⇒ match n return λx. option (x < S N') with [ O ⇒ (return (lt_O_S ?)) | S n' ⇒ (! prf ← nat_bound_opt N' n' ; return (le_S_S ?? prf)) ] ]. inductive nat_compared : nat → nat → Type[0] ≝ | nat_lt : ∀n,m:nat. nat_compared n (n+S m) | nat_eq : ∀n:nat. nat_compared n n | nat_gt : ∀n,m:nat. nat_compared (m+S n) m. let rec nat_compare (n:nat) (m:nat) : nat_compared n m ≝ match n return λx. nat_compared x m with [ O ⇒ match m return λy. nat_compared O y with [ O ⇒ nat_eq ? | S m' ⇒ nat_lt ?? ] | S n' ⇒ match m return λy. nat_compared (S n') y with [ O ⇒ nat_gt n' O | S m' ⇒ match nat_compare n' m' return λx,y.λ_. nat_compared (S x) (S y) with [ nat_lt x y ⇒ nat_lt ?? | nat_eq x ⇒ nat_eq ? | nat_gt x y ⇒ nat_gt ? (S y) ] ] ]. lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n. #n elim n [ @refl | #m #IH whd in ⊢ (??%?); >IH @refl ] qed. lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m. #n #m elim n [ // | #n' #IH whd in ⊢ (??%?); >IH @refl ] qed. lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m. #n #m elim m [ // | #m' #IH whd in ⊢ (??%?); >IH @refl ] qed. let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝ match n return λn.Sum (n=m) (n≠m) with [ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??) | S m' ⇒ inr ??? ] | S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ??? | S m' ⇒ match eq_nat_dec n' m' with [ inl E ⇒ inl ??? | inr NE ⇒ inr ??? ] ] ]. [ 1,2: % #E destruct | >E @refl | % #E destruct cases NE /2/ ] qed. lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n. #m #n #o #H whd in ⊢ (??%); @leb_elim #H' [ @(transitive_le ? m ? H H') | @H ] qed. lemma max_r : ∀m,n,o:nat. o ≤ n → o ≤ max m n. #m #n #o #H whd in ⊢ (??%); @leb_elim #H' [ @H | @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) // ] qed. lemma max_O_n : ∀n. max O n = n. * // qed. lemma max_n_O : ∀n. max n O = n. * // qed. lemma associative_max : associative nat max. #n #m #o normalize @(leb_elim n m) [ normalize @(leb_elim m o) normalize #H1 #H2 [ >(le_to_leb_true n o) /2/ | >(le_to_leb_true n m) // ] | normalize @(leb_elim m o) normalize #H1 #H2 [ % | >(not_le_to_leb_false … H2) >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/ ] ] qed. lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m. /2/ qed. lemma le_plus_k: ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k. #n #m elim m -m; [ #Hn % [ @O | <(le_n_O_to_eq n Hn) // ] | #m #Hind #Hn cases (le_to_or_lt_eq … Hn) -Hn; #Hn [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k) | >Hk // ] | % [ @O | IH >associative_plus in ⊢ (???%); <(associative_plus ? p) in ⊢ (???%); >(commutative_plus_faster ? p) in ⊢ (???%); >(associative_plus p) @associative_plus qed. lemma times_n_Sm_fast : ∀n,m.n + n * m = n * S m. #n elim n -n [ #m % ] #n #IH #m normalize (commutative_plus_faster n) >associative_plus >IH % qed. lemma commutative_times_fast : commutative ? times. #n elim n -n [ #m IH % qed. (* notation for sum *) notation > "Σ_{ ident i ∈ l } f" with precedence 20 for @{'fold plus 0 (λ\${ident i}.true) (λ\${ident i}. \$f) \$l}. notation < "hvbox(Σ_{ ident i break ∈ l } break f)" with precedence 20 for @{'fold plus 0 (λ\${ident i}:\$X.true) (λ\${ident i}:\$Y. \$f) \$l}.