Changeset 2310 for src/utilities/binary/positive.ma

Timestamp:

Aug 31, 2012, 12:50:41 PM (8 years ago)

Author:

garnier

Message:

Moved a lemma from switchRemoval to positive.

File:

• src/utilities/binary/positive.ma (modified) (1 diff)

src/utilities/binary/positive.ma

@@ -1178 +1178 @@
 qed.
 
+lemma max_one_neutral : ∀v. max v one = v.
+* // qed.
+
+(* Auxilliary lemmas to prove associative_max. *)
+lemma reflexive_leb : ∀a. leb a a = true.
+#a @(le_to_leb_true a a) // qed.
+
+lemma le_S_weaken : ∀a,b. le (succ a) b → le a b.
+#a #b /2/ qed.
+
+lemma le_S_contradiction_1 : ∀a. le (succ a) a → False.
+* /2 by absurd/ qed.
+
+lemma le_S_contradiction_2 : ∀a,b. le (succ a) b → le (succ b) a → False.
+#a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2))
+#Heq @(le_S_contradiction_1 a) destruct // qed.
+
+lemma le_S_contradiction_3 : ∀a,b,c. le (succ a) b → le (succ b) c → le (succ c) a → False.
+#a #b #c #H1 #H2 #H3 lapply (transitive_le … H1 (le_S_weaken ?? H2)) #H4
+@(le_S_contradiction_2 … H3 H4)
+qed.
+
+(* There ought to be a simpler proof. *)
+lemma associative_max : associative ? max.
+#a #b #c
+whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c);
+lapply (pos_compare_to_Prop a b)
+cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
+[ 1: >(le_to_leb_true a b) normalize nodelta /2/
+     lapply (pos_compare_to_Prop b c)
+     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
+     [ 1: >(le_to_leb_true b c) normalize nodelta
+          lapply (pos_compare_to_Prop a c)
+          cases (pos_compare a c) whd in ⊢ (% → ?); #Hac
+          [ 1: >(le_to_leb_true a c) /2/
+          | 2: destruct cases (leb c c) //
+          | 3: (* There is an obvious contradiction in the hypotheses. omega, I miss you *)
+               @(False_ind … (le_S_contradiction_3 ??? Hab Hbc Hac))            
+          ]
+          @le_S_weaken //
+     | 2: destruct
+          cases (leb c c) normalize nodelta
+          >(le_to_leb_true a c) /2/
+     | 3: >(not_le_to_leb_false b c) normalize nodelta /2/
+          >(le_to_leb_true a b) /2/
+     ]
+| 2: destruct (Hab) >reflexive_leb normalize nodelta
+     lapply (pos_compare_to_Prop b c)
+     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
+     [ 1: >(le_to_leb_true b c) normalize nodelta
+          >(le_to_leb_true b c) normalize nodelta
+          /2/
+     | 2: destruct >reflexive_leb normalize nodelta
+          >reflexive_leb //
+     | 3: >(not_le_to_leb_false b c) normalize nodelta
+          >reflexive_leb /2/ ]
+| 3: >(not_le_to_leb_false a b) normalize nodelta /2/
+     lapply (pos_compare_to_Prop b c)
+     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
+     [ 1: >(le_to_leb_true b c) normalize nodelta /2/
+     | 2: destruct >reflexive_leb normalize nodelta @refl
+     | 3: >(not_le_to_leb_false b c) normalize nodelta
+          >(not_le_to_leb_false a b) normalize nodelta
+          >(not_le_to_leb_false a c) normalize nodelta
+          lapply (transitive_le … Hbc (le_S_weaken … Hab))
+          #Hca /2/
+     ]
+] qed.
 
 lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.