Ignore:
Timestamp:
Sep 12, 2012, 12:36:46 PM (7 years ago)
Author:
garnier
Message:

Some progress on switch removal. Small fix in the definition of free, in GenMem?.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2234 r2332  
    2222| 2: #Hneq' normalize // ] qed.
    2323
    24 lemma eq_block_identity : ∀b. eq_block b b = true. // qed.
     24(* useful facts on various boolean operations *)
     25lemma andb_lsimpl_true : ∀x. andb true x = x. // qed.
     26lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed.
     27lemma andb_comm : ∀x,y. andb x y = andb y x. // qed.
     28lemma notb_true : notb true = false. // qed.
     29lemma notb_false : notb false = true. % #H destruct qed.
     30lemma notb_fold : ∀x. if x then false else true = (¬x). // qed.
     31
     32(* useful facts on block *)
     33lemma 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
     39lemma 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 *)
     46lemma 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
     50lemma 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
     62lemma 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/
     65qed.
     66
     67lemma Zltb_dec : ∀a,b. (Zltb a b = true) ∨ (Zltb a b = false ∧ Zleb b a = true).
     68#a #b
     69lapply (Z_compare_to_Prop … a b)
     70cases a
     71[ 1: | 2,3: #a' ]
     72cases b
     73whd in match (Z_compare OZ OZ); normalize nodelta
     74[ 2,3,5,6,8,9: #b' ]
     75whd in match (Zleb ? ?);
     76try /3 by or_introl, or_intror, conj, I, refl/
     77whd in match (Zltb ??);
     78whd 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
     89lemma Zleb_unsigned_OZ : ∀bv. Zleb OZ (Z_of_unsigned_bitvector 16 bv) = true.
     90#bv elim bv try // #n' * #tl normalize /2/ qed.
     91
     92lemma Zltb_unsigned_OZ : ∀bv. Zltb (Z_of_unsigned_bitvector 16 bv) OZ = false.
     93#bv elim bv try // #n' * #tl normalize /2/ qed.
     94
     95lemma 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
     105lemma 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)
     109elim (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 ]
     115qed.
     116
     117lemma free_not_valid : ∀x. if Zleb (pos one) x
     118                            then Zleb x OZ 
     119                            else false = false.
     120#x
     121cut (Zle (pos one) x ∧ Zle x OZ → False)
     122[ * #H1 #H2 lapply (transitive_Zle … H1 H2) #H @H ] #Hguard
     123cut (Zleb (pos one) x = true ∧ Zleb x OZ = true → False)
     124[ * #H1 #H2 @Hguard @conj /2 by Zleb_true_to_Zle/ ]
     125cases (Zleb (pos one) x) cases (Zleb x OZ)
     126/2 by refl/ #H @(False_ind … (H (conj … (refl ??) (refl ??))))
     127qed.
Note: See TracChangeset for help on using the changeset viewer.