Changeset 2438 for src/Clight/frontend_misc.ma
 Timestamp:
 Nov 7, 2012, 11:18:56 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2386 r2438 2 2 3 3 include "Clight/TypeComparison.ma". 4 include "Clight/Csem.ma". 4 5 include "common/Pointers.ma". 5 6 include "basics/jmeq.ma". 6 7 include "basics/star.ma". (* wellfounded relations *) 8 include "common/IOMonad.ma". 9 include "common/IO.ma". 7 10 include "basics/lists/listb.ma". 8 11 include "basics/lists/list.ma". 9 10 12 11 13 (*  *) … … 32 34 33 35 lemma le_S_O_absurd : ∀x:nat. S x ≤ 0 → False. /2 by absurd/ qed. 36 37 lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed. 38 39 lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c. 40 #A #B #a #b * #a' #b' #H destruct @refl 41 qed. 42 43 lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c. 44 #A #B #a #b * #a' #b' #H destruct @refl 45 qed. 46 47 lemma bindIO_Error : ∀err,f. bindIO io_out io_in (val×trace) (trace×state) (Error … err) f = Wrong io_out io_in (trace×state) err. 48 // qed. 49 50 lemma bindIO_Value : ∀v,f. bindIO io_out io_in (val×trace) (trace×state) (Value … v) f = (f v). 51 // qed. 52 53 lemma bindIO_elim : 54 ∀A. 55 ∀P : (IO io_out io_in A) → Prop. 56 ∀e : res A. (*IO io_out io_in A.*) 57 ∀f. 58 (∀v. (e:IO io_out io_in A) = OK … v → P (f v)) → 59 (∀err. (e:IO io_out io_in A) = Error … err → P (Wrong ??? err)) → 60 P (bindIO io_out io_in ? A (e:IO io_out io_in A) f). 61 #A #P * try /2/ qed. 62 63 lemma opt_to_io_Value : 64 ∀A,B,C,err,x,res. opt_to_io A B C err x = return res → x = Some ? res. 65 #A #B #C #err #x cases x normalize 66 [ 1: #res #Habsurd destruct 67  2: #c #res #Heq destruct @refl ] 68 qed. 69 70 lemma some_inversion : 71 ∀A,B:Type[0]. 72 ∀e:option A. 73 ∀res:B. 74 ∀f:A → option B. 75 match e with 76 [ None ⇒ None ? 77  Some x ⇒ f x ] = Some ? res → 78 ∃x. e = Some ? x ∧ f x = Some ? res. 79 #A #B #e #res #f cases e normalize nodelta 80 [ 1: #Habsurd destruct (Habsurd) 81  2: #a #Heq %{a} @conj >Heq @refl ] 82 qed. 83 84 lemma cons_inversion : 85 ∀A,B:Type[0]. 86 ∀e:list A. 87 ∀res:B. 88 ∀f:A → list A → option B. 89 match e with 90 [ nil ⇒ None ? 91  cons hd tl ⇒ f hd tl ] = Some ? res → 92 ∃hd,tl. e = hd::tl ∧ f hd tl = Some ? res. 93 #A #B #e #res #f cases e normalize nodelta 94 [ 1: #Habsurd destruct (Habsurd) 95  2: #hd #tl #Heq %{hd} %{tl} @conj >Heq @refl ] 96 qed. 97 98 lemma if_opt_inversion : 99 ∀A:Type[0]. 100 ∀x. 101 ∀y:A. 102 ∀e:bool. 103 (if e then 104 x 105 else 106 None ?) = Some ? y → 107 e = true ∧ x = Some ? y. 108 #A #x #y * normalize 109 #H destruct @conj @refl 110 qed. 111 112 lemma andb_inversion : 113 ∀a,b : bool. andb a b = true → a = true ∧ b = true. 114 * * normalize /2 by conj, refl/ qed. 115 116 lemma identifier_eq_i_i : ∀tag,i. ∃pf. identifier_eq tag i i = inl … pf. 117 #tag #i cases (identifier_eq ? i i) 118 [ 1: #H %{H} @refl 119  2: * #Habsurd @(False_ind … (Habsurd … (refl ? i))) ] 120 qed. 34 121 35 122 (*  *) … … 120 207 121 208 lemma free_not_valid : ∀x. if Zleb (pos one) x 122 then Zl eb x OZ209 then Zltb x OZ 123 210 else false = false. 124 211 #x 125 cut (Zle (pos one) x ∧ Zl ex OZ → False)126 [ * #H1 #H2 lapply (transitive_Zle … H1 H2) #H @H ] #Hguard127 cut (Zleb (pos one) x = true ∧ Zl eb x OZ = true → False)128 [ * #H1 #H2 @Hguard @conj /2 by Zleb_true_to_Zle/ ]129 cases (Zleb (pos one) x) cases (Zl eb x OZ)212 cut (Zle (pos one) x ∧ Zlt x OZ → False) 213 [ * #H1 #H2 lapply (transitive_Zle … (monotonic_Zle_Zsucc … H1) (Zlt_to_Zle … H2)) #H @H ] #Hguard 214 cut (Zleb (pos one) x = true ∧ Zltb x OZ = true → False) 215 [ * #H1 #H2 @Hguard @conj /2 by Zleb_true_to_Zle/ @Zltb_true_to_Zlt assumption ] 216 cases (Zleb (pos one) x) cases (Zltb x OZ) 130 217 /2 by refl/ #H @(False_ind … (H (conj … (refl ??) (refl ??)))) 131 218 qed. … … 219 306 lemma nil_append : ∀A. ∀(l : list A). [ ] @ l = l. // qed. 220 307 308 alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)". 309 221 310 lemma mem_append : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) ↔ (mem … elt l1) ∨ (mem … elt l2). 222 311 #A #elt #l1 elim l1 223 312 [ 1: #l2 normalize @conj [ 1: #H %2 @H  2: * [ 1: @False_ind  2: #H @H ] ] 224 313  2: #hd #tl #Hind #l2 @conj 225 [ 1: whd in match (mem ???); *314 [ 1: whd in match (meml ???); * 226 315 [ 1: #Heq >Heq %1 normalize %1 @refl 227 316  2: #H1 lapply (Hind l2) * #HA #HB normalize
Note: See TracChangeset
for help on using the changeset viewer.