Changeset 2310


Ignore:
Timestamp:
Aug 31, 2012, 12:50:41 PM (7 years ago)
Author:
garnier
Message:

Moved a lemma from switchRemoval to positive.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/binary/positive.ma

    r1628 r2310  
    11781178qed.
    11791179
     1180lemma max_one_neutral : ∀v. max v one = v.
     1181* // qed.
     1182
     1183(* Auxilliary lemmas to prove associative_max. *)
     1184lemma reflexive_leb : ∀a. leb a a = true.
     1185#a @(le_to_leb_true a a) // qed.
     1186
     1187lemma le_S_weaken : ∀a,b. le (succ a) b → le a b.
     1188#a #b /2/ qed.
     1189
     1190lemma le_S_contradiction_1 : ∀a. le (succ a) a → False.
     1191* /2 by absurd/ qed.
     1192
     1193lemma 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
     1197lemma 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)
     1200qed.
     1201
     1202(* There ought to be a simpler proof. *)
     1203lemma associative_max : associative ? max.
     1204#a #b #c
     1205whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c);
     1206lapply (pos_compare_to_Prop a b)
     1207cases (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.
    11801248
    11811249lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
Note: See TracChangeset for help on using the changeset viewer.