Changeset 2332 for src/Clight/frontend_misc.ma
 Timestamp:
 Sep 12, 2012, 12:36:46 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2234 r2332 22 22  2: #Hneq' normalize // ] qed. 23 23 24 lemma eq_block_identity : ∀b. eq_block b b = true. // qed. 24 (* useful facts on various boolean operations *) 25 lemma andb_lsimpl_true : ∀x. andb true x = x. // qed. 26 lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed. 27 lemma andb_comm : ∀x,y. andb x y = andb y x. // qed. 28 lemma notb_true : notb true = false. // qed. 29 lemma notb_false : notb false = true. % #H destruct qed. 30 lemma notb_fold : ∀x. if x then false else true = (¬x). // qed. 31 32 (* useful facts on block *) 33 lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false. 34 #b1 #b2 #Hneq 35 @(eq_block_elim … b1 b2) 36 [ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??))) 37  2: #_ @refl ] qed. 38 39 lemma not_eq_block_rev : ∀b1,b2. b2 ≠ b1 → eq_block b1 b2 = false. 40 #b1 #b2 #Hneq 41 @(eq_block_elim … b1 b2) 42 [ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??))) 43  2: #_ @refl ] qed. 44 45 (* useful facts on Z *) 46 lemma Zltb_to_Zleb_true : ∀a,b. Zltb a b = true → Zleb a b = true. 47 #a #b #Hltb lapply (Zltb_true_to_Zlt … Hltb) #Hlt @Zle_to_Zleb_true 48 /3 by Zlt_to_Zle, transitive_Zle/ qed. 49 50 lemma Zle_to_Zle_to_eq : ∀a,b. Zle a b → Zle b a → a = b. 51 #a #b elim b 52 [ 1: elim a // #a' normalize [ 1: @False_ind  2: #_ @False_ind ] ] 53 #b' elim a normalize 54 [ 1: #_ @False_ind 55  2: #a' #H1 #H2 >(le_to_le_to_eq … H1 H2) @refl 56  3: #a' #_ @False_ind 57  4: @False_ind 58  5: #a' @False_ind 59  6: #a' #H2 #H1 >(le_to_le_to_eq … H1 H2) @refl 60 ] qed. 61 62 lemma Zleb_true_to_Zleb_true_to_eq : ∀a,b. (Zleb a b = true) → (Zleb b a = true) → a = b. 63 #a #b #H1 #H2 64 /3 by Zle_to_Zle_to_eq, Zleb_true_to_Zle/ 65 qed. 66 67 lemma Zltb_dec : ∀a,b. (Zltb a b = true) ∨ (Zltb a b = false ∧ Zleb b a = true). 68 #a #b 69 lapply (Z_compare_to_Prop … a b) 70 cases a 71 [ 1:  2,3: #a' ] 72 cases b 73 whd in match (Z_compare OZ OZ); normalize nodelta 74 [ 2,3,5,6,8,9: #b' ] 75 whd in match (Zleb ? ?); 76 try /3 by or_introl, or_intror, conj, I, refl/ 77 whd in match (Zltb ??); 78 whd in match (Zleb ??); #_ 79 [ 1: cases (decidable_le (succ a') b') 80 [ 1: #H lapply (le_to_leb_true … H) #H %1 assumption 81  2: #Hnotle lapply (not_le_to_lt … Hnotle) #Hlt %2 @conj try @le_to_leb_true 82 /2 by monotonic_pred/ @(not_le_to_leb_false … Hnotle) ] 83  2: cases (decidable_le (succ b') a') 84 [ 1: #H lapply (le_to_leb_true … H) #H %1 assumption 85  2: #Hnotle lapply (not_le_to_lt … Hnotle) #Hlt %2 @conj try @le_to_leb_true 86 /2 by monotonic_pred/ @(not_le_to_leb_false … Hnotle) ] 87 ] qed. 88 89 lemma Zleb_unsigned_OZ : ∀bv. Zleb OZ (Z_of_unsigned_bitvector 16 bv) = true. 90 #bv elim bv try // #n' * #tl normalize /2/ qed. 91 92 lemma Zltb_unsigned_OZ : ∀bv. Zltb (Z_of_unsigned_bitvector 16 bv) OZ = false. 93 #bv elim bv try // #n' * #tl normalize /2/ qed. 94 95 lemma Z_of_unsigned_not_neg : ∀bv. 96 (Z_of_unsigned_bitvector 16 bv = OZ) ∨ (∃p. Z_of_unsigned_bitvector 16 bv = pos p). 97 #bv elim bv 98 [ 1: normalize %1 @refl 99  2: #n #hd #tl #Hind cases hd 100 [ 1: normalize %2 /2 by ex_intro/ 101  2: cases Hind normalize [ 1: #H %1 @H  2: * #p #H >H %2 %{p} @refl ] 102 ] 103 ] qed. 104 105 lemma free_not_in_bounds : ∀x. if Zleb (pos one) x 106 then Zltb x OZ 107 else false = false. 108 #x lapply (Zltb_to_Zleb_true x OZ) 109 elim (Zltb_dec … x OZ) 110 [ 1: #Hlt >Hlt #H lapply (H (refl ??)) elim x 111 [ 2,3: #x' ] normalize in ⊢ (% → ?); 112 [ 1: #Habsurd destruct (Habsurd) 113  2,3: #_ @refl ] 114  2: * #Hlt #Hle #_ >Hlt cases (Zleb (pos one) x) @refl ] 115 qed. 116 117 lemma free_not_valid : ∀x. if Zleb (pos one) x 118 then Zleb x OZ 119 else false = false. 120 #x 121 cut (Zle (pos one) x ∧ Zle x OZ → False) 122 [ * #H1 #H2 lapply (transitive_Zle … H1 H2) #H @H ] #Hguard 123 cut (Zleb (pos one) x = true ∧ Zleb x OZ = true → False) 124 [ * #H1 #H2 @Hguard @conj /2 by Zleb_true_to_Zle/ ] 125 cases (Zleb (pos one) x) cases (Zleb x OZ) 126 /2 by refl/ #H @(False_ind … (H (conj … (refl ??) (refl ??)))) 127 qed.
Note: See TracChangeset
for help on using the changeset viewer.