1 | include "basics/types.ma". |
---|
2 | include "arithmetics/nat.ma". |
---|
3 | include "utilities/option.ma". |
---|
4 | |
---|
5 | (* JHM: here, for definiteness; used in ASM/ASM.ma *) |
---|
6 | let rec nat_bound_opt (N:nat) (n:nat) : option (n < N) ≝ |
---|
7 | match N return λy. option (n < y) with |
---|
8 | [ O ⇒ None ? |
---|
9 | | S N' ⇒ |
---|
10 | match n return λx. option (x < S N') with |
---|
11 | [ O ⇒ (return (lt_O_S ?)) |
---|
12 | | S n' ⇒ (! prf ← nat_bound_opt N' n' ; return (le_S_S ?? prf)) |
---|
13 | ] |
---|
14 | ]. |
---|
15 | |
---|
16 | lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z. |
---|
17 | #x0 elim x0 |
---|
18 | [ #y %{y} %2 % |
---|
19 | | #x #IH * |
---|
20 | [ %{(S x)} %1 % |
---|
21 | | #y cases (IH y) #z * |
---|
22 | [ #H %{z} %1 >H // |
---|
23 | | #H %{z} %2 >H // |
---|
24 | ] |
---|
25 | ] |
---|
26 | ] qed. |
---|
27 | |
---|
28 | inductive nat_compared : nat → nat → Type[0] ≝ |
---|
29 | | nat_lt : ∀n,m:nat. nat_compared n (n+S m) |
---|
30 | | nat_eq : ∀n:nat. nat_compared n n |
---|
31 | | nat_gt : ∀n,m:nat. nat_compared (m+S n) m. |
---|
32 | |
---|
33 | let rec nat_compare (n:nat) (m:nat) : nat_compared n m ≝ |
---|
34 | match n return λx. nat_compared x m with |
---|
35 | [ O ⇒ match m return λy. nat_compared O y with [ O ⇒ nat_eq ? | S m' ⇒ nat_lt ?? ] |
---|
36 | | S n' ⇒ |
---|
37 | match m return λy. nat_compared (S n') y with |
---|
38 | [ O ⇒ nat_gt n' O |
---|
39 | | S m' ⇒ match nat_compare n' m' return λx,y.λ_. nat_compared (S x) (S y) with |
---|
40 | [ nat_lt x y ⇒ nat_lt ?? |
---|
41 | | nat_eq x ⇒ nat_eq ? |
---|
42 | | nat_gt x y ⇒ nat_gt ? (S y) |
---|
43 | ] |
---|
44 | ] |
---|
45 | ]. |
---|
46 | |
---|
47 | lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n. |
---|
48 | #n elim n |
---|
49 | [ @refl |
---|
50 | | #m #IH whd in ⊢ (??%?); >IH @refl |
---|
51 | ] qed. |
---|
52 | |
---|
53 | lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m. |
---|
54 | #n #m elim n |
---|
55 | [ // |
---|
56 | | #n' #IH whd in ⊢ (??%?); >IH @refl |
---|
57 | ] qed. |
---|
58 | |
---|
59 | lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m. |
---|
60 | #n #m elim m |
---|
61 | [ // |
---|
62 | | #m' #IH whd in ⊢ (??%?); >IH @refl |
---|
63 | ] qed. |
---|
64 | |
---|
65 | |
---|
66 | let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝ |
---|
67 | match n return λn.Sum (n=m) (n≠m) with |
---|
68 | [ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??) | S m' ⇒ inr ??? ] |
---|
69 | | S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ??? | S m' ⇒ |
---|
70 | match eq_nat_dec n' m' with [ inl E ⇒ inl ??? | inr NE ⇒ inr ??? ] ] |
---|
71 | ]. |
---|
72 | [ 1,2: % #E destruct |
---|
73 | | >E @refl |
---|
74 | | % #E destruct cases NE /2/ |
---|
75 | ] qed. |
---|
76 | |
---|
77 | lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n. |
---|
78 | #m #n #o #H whd in ⊢ (??%); @leb_elim #H' |
---|
79 | [ @(transitive_le ? m ? H H') |
---|
80 | | @H |
---|
81 | ] qed. |
---|
82 | |
---|
83 | lemma max_r : ∀m,n,o:nat. o ≤ n → o ≤ max m n. |
---|
84 | #m #n #o #H whd in ⊢ (??%); @leb_elim #H' |
---|
85 | [ @H |
---|
86 | | @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) // |
---|
87 | ] qed. |
---|
88 | |
---|
89 | lemma max_O_n : ∀n. max O n = n. |
---|
90 | * // |
---|
91 | qed. |
---|
92 | |
---|
93 | lemma max_n_O : ∀n. max n O = n. |
---|
94 | * // |
---|
95 | qed. |
---|
96 | |
---|
97 | lemma associative_max : associative nat max. |
---|
98 | #n #m #o normalize |
---|
99 | @(leb_elim n m) |
---|
100 | [ normalize @(leb_elim m o) normalize #H1 #H2 |
---|
101 | [ >(le_to_leb_true n o) /2/ |
---|
102 | | >(le_to_leb_true n m) // |
---|
103 | ] |
---|
104 | | normalize @(leb_elim m o) normalize #H1 #H2 |
---|
105 | [ % |
---|
106 | | >(not_le_to_leb_false … H2) |
---|
107 | >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/ |
---|
108 | ] |
---|
109 | ] qed. |
---|
110 | |
---|
111 | lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m. |
---|
112 | /2/ qed. |
---|
113 | |
---|
114 | lemma le_plus_k: |
---|
115 | ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k. |
---|
116 | #n #m elim m -m; |
---|
117 | [ #Hn % [ @O | <(le_n_O_to_eq n Hn) // ] |
---|
118 | | #m #Hind #Hn cases (le_to_or_lt_eq … Hn) -Hn; #Hn |
---|
119 | [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k) | >Hk // ] |
---|
120 | | % [ @O | <Hn // ] |
---|
121 | ] |
---|
122 | ] |
---|
123 | qed. |
---|
124 | |
---|
125 | lemma eq_plus_S_to_lt: |
---|
126 | ∀n,m,p:ℕ.n = m + (S p) → m < n. |
---|
127 | #n #m #p /2 by lt_plus_to_lt_l/ |
---|
128 | qed. |
---|
129 | |
---|
130 | (* "Fast" proofs: some proofs get reduced during normalization (in particular, |
---|
131 | some functions which use a proof for rewriting are applied to constants and |
---|
132 | get reduced during a proof or while matita is searching for a term; |
---|
133 | they may also be normalized during testing), and so here are some more |
---|
134 | efficient versions. Perhaps they could be replaced using some kind of proof |
---|
135 | irrelevance? *) |
---|
136 | |
---|
137 | let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝ |
---|
138 | match n return λn'.∀m.S(n'+m) = n'+S m with |
---|
139 | [ O ⇒ λm.refl ?? |
---|
140 | | S n' ⇒ λm. ? |
---|
141 | ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed. |
---|
142 | |
---|
143 | let rec plus_n_O_faster (n:nat) : n = n + O ≝ |
---|
144 | match n return λn.n=n+O with |
---|
145 | [ O ⇒ refl ?? |
---|
146 | | S n' ⇒ match plus_n_O_faster n' return λx.λ_.S n'=S x with [ refl ⇒ refl ?? ] |
---|
147 | ]. |
---|
148 | |
---|
149 | let rec commutative_plus_faster (n,m:nat) : n+m = m+n ≝ |
---|
150 | match n return λn.n+m = m+n with |
---|
151 | [ O ⇒ plus_n_O_faster ? |
---|
152 | | S n' ⇒ ? |
---|
153 | ]. @(match plus_n_Sm_fast m n' return λx.λ_. ? = x with [ refl ⇒ ? ]) |
---|
154 | @(match commutative_plus_faster n' m return λx.λ_.? = S x with [refl ⇒ ?]) @refl qed. |
---|
155 | |
---|
156 | lemma distributive_times_plus_fast : distributive ? times plus. |
---|
157 | #n elim n [ #m #p % ] |
---|
158 | #n' #IH #m #p normalize |
---|
159 | >IH |
---|
160 | >associative_plus in ⊢ (???%); |
---|
161 | <(associative_plus ? p) in ⊢ (???%); |
---|
162 | >(commutative_plus_faster ? p) in ⊢ (???%); |
---|
163 | >(associative_plus p) |
---|
164 | @associative_plus |
---|
165 | qed. |
---|
166 | |
---|
167 | lemma times_n_Sm_fast : ∀n,m.n + n * m = n * S m. |
---|
168 | #n elim n -n |
---|
169 | [ #m % ] |
---|
170 | #n #IH #m normalize <IH |
---|
171 | <associative_plus >(commutative_plus_faster n) |
---|
172 | >associative_plus >IH % |
---|
173 | qed. |
---|
174 | |
---|
175 | lemma commutative_times_fast : commutative ? times. |
---|
176 | #n elim n -n |
---|
177 | [ #m <times_n_O % ] |
---|
178 | #n #IH #m normalize <times_n_Sm_fast >IH % |
---|
179 | qed. |
---|
180 | |
---|
181 | (* notation for sum *) |
---|
182 | notation > "Σ_{ ident i ∈ l } f" |
---|
183 | with precedence 20 |
---|
184 | for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}. |
---|
185 | notation < "hvbox(Σ_{ ident i break ∈ l } break f)" |
---|
186 | with precedence 20 |
---|
187 | for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}. |
---|
188 | |
---|