include "arithmetics/nat.ma". 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. 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. (* "Fast" proofs: some proofs get reduced during normalization (in particular, some functions which use a proof for rewriting are applied to constants and get reduced during a proof or while matita is searching for a term; they may also be normalized during testing), and so here are some more efficient versions. Perhaps they could be replaced using some kind of proof irrelevance? *) let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝ match n return λn'.∀m.S(n'+m) = n'+S m with [ O ⇒ λm.refl ?? | S n' ⇒ λm. ? ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed. let rec plus_n_O_faster (n:nat) : n = n + O ≝ match n return λn.n=n+O with [ O ⇒ refl ?? | S n' ⇒ match plus_n_O_faster n' return λx.λ_.S n'=S x with [ refl ⇒ refl ?? ] ]. let rec commutative_plus_faster (n,m:nat) : n+m = m+n ≝ match n return λn.n+m = m+n with [ O ⇒ plus_n_O_faster ? | S n' ⇒ ? ]. @(match plus_n_Sm_fast m n' return λx.λ_. ? = x with [ refl ⇒ ? ]) @(match commutative_plus_faster n' m return λx.λ_.? = S x with [refl ⇒ ?]) @refl qed.