[744] | 1 | include "arithmetics/nat.ma". |
---|
| 2 | |
---|
| 3 | inductive nat_compared : nat → nat → Type[0] ≝ |
---|
| 4 | | nat_lt : ∀n,m:nat. nat_compared n (n+S m) |
---|
| 5 | | nat_eq : ∀n:nat. nat_compared n n |
---|
| 6 | | nat_gt : ∀n,m:nat. nat_compared (m+S n) m. |
---|
| 7 | |
---|
| 8 | let rec nat_compare (n:nat) (m:nat) : nat_compared n m ≝ |
---|
| 9 | match n return λx. nat_compared x m with |
---|
| 10 | [ O ⇒ match m return λy. nat_compared O y with [ O ⇒ nat_eq ? | S m' ⇒ nat_lt ?? ] |
---|
| 11 | | S n' ⇒ |
---|
| 12 | match m return λy. nat_compared (S n') y with |
---|
| 13 | [ O ⇒ nat_gt n' O |
---|
| 14 | | S m' ⇒ match nat_compare n' m' return λx,y.λ_. nat_compared (S x) (S y) with |
---|
| 15 | [ nat_lt x y ⇒ nat_lt ?? |
---|
| 16 | | nat_eq x ⇒ nat_eq ? |
---|
| 17 | | nat_gt x y ⇒ nat_gt ? (S y) |
---|
| 18 | ] |
---|
| 19 | ] |
---|
| 20 | ]. |
---|
| 21 | |
---|
[961] | 22 | lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n. |
---|
| 23 | #n elim n |
---|
| 24 | [ @refl |
---|
| 25 | | #m #IH whd in ⊢ (??%?) > IH @refl |
---|
| 26 | ] qed. |
---|
| 27 | |
---|
| 28 | lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m. |
---|
| 29 | #n #m elim n |
---|
| 30 | [ // |
---|
| 31 | | #n' #IH whd in ⊢ (??%?) > IH @refl |
---|
| 32 | ] qed. |
---|
| 33 | |
---|
| 34 | lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m. |
---|
| 35 | #n #m elim m |
---|
| 36 | [ // |
---|
| 37 | | #m' #IH whd in ⊢ (??%?) > IH @refl |
---|
| 38 | ] qed. |
---|
| 39 | |
---|
[744] | 40 | lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n. |
---|
| 41 | #m #n #o #H whd in ⊢ (??%) @leb_elim #H' |
---|
| 42 | [ @(transitive_le ? m ? H H') |
---|
| 43 | | @H |
---|
| 44 | ] qed. |
---|
| 45 | |
---|
| 46 | lemma max_r : ∀m,n,o:nat. o ≤ n → o ≤ max m n. |
---|
| 47 | #m #n #o #H whd in ⊢ (??%) @leb_elim #H' |
---|
| 48 | [ @H |
---|
| 49 | | @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) // |
---|
| 50 | ] qed. |
---|
| 51 | |
---|
| 52 | |
---|
| 53 | (* "Fast" proofs: some proofs get reduced during normalization (in particular, |
---|
| 54 | some functions which use a proof for rewriting are applied to constants and |
---|
| 55 | get reduced during a proof or while matita is searching for a term; |
---|
| 56 | they may also be normalized during testing), and so here are some more |
---|
| 57 | efficient versions. Perhaps they could be replaced using some kind of proof |
---|
| 58 | irrelevance? *) |
---|
| 59 | |
---|
| 60 | let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝ |
---|
| 61 | match n return λn'.∀m.S(n'+m) = n'+S m with |
---|
| 62 | [ O ⇒ λm.refl ?? |
---|
| 63 | | S n' ⇒ λm. ? |
---|
| 64 | ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed. |
---|
| 65 | |
---|
| 66 | let rec plus_n_O_faster (n:nat) : n = n + O ≝ |
---|
| 67 | match n return λn.n=n+O with |
---|
| 68 | [ O ⇒ refl ?? |
---|
| 69 | | S n' ⇒ match plus_n_O_faster n' return λx.λ_.S n'=S x with [ refl ⇒ refl ?? ] |
---|
| 70 | ]. |
---|
| 71 | |
---|
| 72 | let rec commutative_plus_faster (n,m:nat) : n+m = m+n ≝ |
---|
| 73 | match n return λn.n+m = m+n with |
---|
| 74 | [ O ⇒ plus_n_O_faster ? |
---|
| 75 | | S n' ⇒ ? |
---|
| 76 | ]. @(match plus_n_Sm_fast m n' return λx.λ_. ? = x with [ refl ⇒ ? ]) |
---|
| 77 | @(match commutative_plus_faster n' m return λx.λ_.? = S x with [refl ⇒ ?]) @refl qed. |
---|
| 78 | |
---|