 Timestamp:
 Aug 31, 2012, 12:50:41 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/binary/positive.ma
r1628 r2310 1178 1178 qed. 1179 1179 1180 lemma max_one_neutral : ∀v. max v one = v. 1181 * // qed. 1182 1183 (* Auxilliary lemmas to prove associative_max. *) 1184 lemma reflexive_leb : ∀a. leb a a = true. 1185 #a @(le_to_leb_true a a) // qed. 1186 1187 lemma le_S_weaken : ∀a,b. le (succ a) b → le a b. 1188 #a #b /2/ qed. 1189 1190 lemma le_S_contradiction_1 : ∀a. le (succ a) a → False. 1191 * /2 by absurd/ qed. 1192 1193 lemma le_S_contradiction_2 : ∀a,b. le (succ a) b → le (succ b) a → False. 1194 #a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2)) 1195 #Heq @(le_S_contradiction_1 a) destruct // qed. 1196 1197 lemma le_S_contradiction_3 : ∀a,b,c. le (succ a) b → le (succ b) c → le (succ c) a → False. 1198 #a #b #c #H1 #H2 #H3 lapply (transitive_le … H1 (le_S_weaken ?? H2)) #H4 1199 @(le_S_contradiction_2 … H3 H4) 1200 qed. 1201 1202 (* There ought to be a simpler proof. *) 1203 lemma associative_max : associative ? max. 1204 #a #b #c 1205 whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c); 1206 lapply (pos_compare_to_Prop a b) 1207 cases (pos_compare a b) whd in ⊢ (% → ?); #Hab 1208 [ 1: >(le_to_leb_true a b) normalize nodelta /2/ 1209 lapply (pos_compare_to_Prop b c) 1210 cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc 1211 [ 1: >(le_to_leb_true b c) normalize nodelta 1212 lapply (pos_compare_to_Prop a c) 1213 cases (pos_compare a c) whd in ⊢ (% → ?); #Hac 1214 [ 1: >(le_to_leb_true a c) /2/ 1215  2: destruct cases (leb c c) // 1216  3: (* There is an obvious contradiction in the hypotheses. omega, I miss you *) 1217 @(False_ind … (le_S_contradiction_3 ??? Hab Hbc Hac)) 1218 ] 1219 @le_S_weaken // 1220  2: destruct 1221 cases (leb c c) normalize nodelta 1222 >(le_to_leb_true a c) /2/ 1223  3: >(not_le_to_leb_false b c) normalize nodelta /2/ 1224 >(le_to_leb_true a b) /2/ 1225 ] 1226  2: destruct (Hab) >reflexive_leb normalize nodelta 1227 lapply (pos_compare_to_Prop b c) 1228 cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc 1229 [ 1: >(le_to_leb_true b c) normalize nodelta 1230 >(le_to_leb_true b c) normalize nodelta 1231 /2/ 1232  2: destruct >reflexive_leb normalize nodelta 1233 >reflexive_leb // 1234  3: >(not_le_to_leb_false b c) normalize nodelta 1235 >reflexive_leb /2/ ] 1236  3: >(not_le_to_leb_false a b) normalize nodelta /2/ 1237 lapply (pos_compare_to_Prop b c) 1238 cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc 1239 [ 1: >(le_to_leb_true b c) normalize nodelta /2/ 1240  2: destruct >reflexive_leb normalize nodelta @refl 1241  3: >(not_le_to_leb_false b c) normalize nodelta 1242 >(not_le_to_leb_false a b) normalize nodelta 1243 >(not_le_to_leb_false a c) normalize nodelta 1244 lapply (transitive_le … Hbc (le_S_weaken … Hab)) 1245 #Hca /2/ 1246 ] 1247 ] qed. 1180 1248 1181 1249 lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
Note: See TracChangeset
for help on using the changeset viewer.