Ignore:
Timestamp:
Nov 7, 2012, 11:18:56 AM (8 years ago)
Author:
garnier
Message:

Sync of the w.i.p. for switch removal.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2386 r2438  
    22
    33include "Clight/TypeComparison.ma".
     4include "Clight/Csem.ma".
    45include "common/Pointers.ma".
    56include "basics/jmeq.ma".
    67include "basics/star.ma". (* well-founded relations *)
     8include "common/IOMonad.ma".
     9include "common/IO.ma".
    710include "basics/lists/listb.ma".
    811include "basics/lists/list.ma".
    9 
    1012
    1113(* --------------------------------------------------------------------------- *)
     
    3234
    3335lemma le_S_O_absurd : ∀x:nat. S x ≤ 0 → False. /2 by absurd/ qed.
     36
     37lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed.
     38
     39lemma 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
     41qed.
     42
     43lemma 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
     45qed.
     46
     47lemma 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
     50lemma bindIO_Value : ∀v,f. bindIO io_out io_in (val×trace) (trace×state) (Value … v) f = (f v).
     51// qed.
     52
     53lemma 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
     63lemma 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 ]
     68qed. 
     69
     70lemma 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 ]
     82qed.
     83
     84lemma 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 ]
     96qed.
     97
     98lemma 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
     110qed.
     111
     112lemma andb_inversion :
     113  ∀a,b : bool. andb a b = true → a = true ∧ b = true.
     114* * normalize /2 by conj, refl/ qed. 
     115
     116lemma 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))) ]
     120qed.
    34121
    35122(* --------------------------------------------------------------------------- *)
     
    120207
    121208lemma free_not_valid : ∀x. if Zleb (pos one) x
    122                             then Zleb x OZ 
     209                            then Zltb x OZ 
    123210                            else false = false.
    124211#x
    125 cut (Zle (pos one) x ∧ Zle x OZ → False)
    126 [ * #H1 #H2 lapply (transitive_Zle … H1 H2) #H @H ] #Hguard
    127 cut (Zleb (pos one) x = true ∧ Zleb x OZ = true → False)
    128 [ * #H1 #H2 @Hguard @conj /2 by Zleb_true_to_Zle/ ]
    129 cases (Zleb (pos one) x) cases (Zleb x OZ)
     212cut (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
     214cut (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 ]
     216cases (Zleb (pos one) x) cases (Zltb x OZ)
    130217/2 by refl/ #H @(False_ind … (H (conj … (refl ??) (refl ??))))
    131218qed.
     
    219306lemma nil_append : ∀A. ∀(l : list A). [ ] @ l = l. // qed.
    220307
     308alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
     309
    221310lemma mem_append : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) ↔ (mem … elt l1) ∨ (mem … elt l2).
    222311#A #elt #l1 elim l1
    223312[ 1: #l2 normalize @conj [ 1: #H %2 @H | 2: * [ 1: @False_ind | 2: #H @H ] ]
    224313| 2: #hd #tl #Hind #l2 @conj
    225      [ 1: whd in match (mem ???); *
     314     [ 1: whd in match (meml ???); *
    226315          [ 1: #Heq >Heq %1 normalize %1 @refl
    227316          | 2: #H1 lapply (Hind l2) * #HA #HB normalize
Note: See TracChangeset for help on using the changeset viewer.