Changeset 859


Ignore:
Timestamp:
May 30, 2011, 6:38:58 PM (8 years ago)
Author:
mulligan
Message:

more added

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r856 r859  
    5959qed.
    6060
     61include "basics/jmeq.ma".
     62
     63notation > "hvbox(a break ≃ b)"
     64  non associative with precedence 45
     65for @{ 'jmeq ? $a ? $b }.
     66
     67notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
     68  non associative with precedence 45
     69for @{ 'jmeq $t $a $u $b }.
     70
     71interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
     72
     73lemma eq_to_jmeq:
     74  ∀A: Type[0].
     75  ∀x, y: A.
     76    x = y → x ≃ y.
     77  //
     78qed.
     79
     80axiom vector_associativity_of_append:
     81  ∀A: Type[0].
     82  ∀n, m, o:  nat.
     83  ∀v: Vector A n.
     84  ∀q: Vector A m.
     85  ∀r: Vector A o.
     86    ((v @@ q) @@ r)
     87    ≃
     88    (v @@ (q @@ r)).
     89       
     90axiom vector_cons_append:
     91  ∀A: Type[0].
     92  ∀n: nat.
     93  ∀a: A.
     94  ∀v: Vector A n.
     95    a ::: v = [[ a ]] @@ v.
     96
     97lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
     98 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
     99qed.
     100
     101coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
     102
     103lemma super_rewrite2:
     104 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
     105  ∀P: ∀m. Vector A m → Prop.
     106   n=m → v1 ≃ v2 → P n v1 → P m v2.
     107 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
     108qed.
     109
     110lemma mem_middle_vector:
     111  ∀A: Type[0].
     112  ∀m, o: nat.
     113  ∀eq: A → A → bool.
     114  ∀reflex: ∀a. eq a a = true.
     115  ∀p: Vector A m.
     116  ∀a: A.
     117  ∀r: Vector A o.
     118    mem A eq ? (p@@(a:::r)) a = true.
     119  # A # M # O # EQ # REFLEX # P # A
     120  elim P
     121  [ normalize
     122    > (REFLEX A)
     123    normalize
     124    # H
     125    %
     126  | # NN # AA # PP # IH
     127    normalize
     128    cases (EQ A AA) //
     129     @ IH
     130  ]
     131qed.
     132
     133lemma mem_monotonic_wrt_append:
     134  ∀A: Type[0].
     135  ∀m, o: nat.
     136  ∀eq: A → A → bool.
     137  ∀reflex: ∀a. eq a a = true.
     138  ∀p: Vector A m.
     139  ∀a: A.
     140  ∀r: Vector A o.
     141    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
     142  # A # M # O # EQ # REFLEX # P # A
     143  elim P
     144  [ #R #H @H
     145  | #NN #AA # PP # IH #R #H
     146    normalize
     147    cases (EQ A AA)
     148    [ normalize %
     149    | @ IH @ H
     150    ]
     151  ]
     152qed.
     153
     154lemma subvector_hd_tl:
     155  ∀A: Type[0].
     156  ∀o, n: nat.
     157  ∀eq: A → A → bool.
     158  ∀refl: ∀a. eq a a = true.
     159  ∀h: Vector A o.
     160  ∀v: Vector A n.
     161  ∀m: nat.
     162  ∀q: Vector A m.
     163    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
     164  # A # O # N # EQ # REFLEX # H # V
     165  elim V
     166  [ normalize
     167    # M # V %
     168  | # NN # AA # VV # IH # MM # QQ
     169    change with (bool_to_Prop (andb ??))
     170    cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
     171    [
     172    | # HH > HH
     173      > (vector_cons_append ? ? AA VV)
     174      change with (bool_to_Prop (subvector_with ??????))
     175      @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
     176        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
     177        ?
     178        (vector_associativity_of_append A ? ? ? QQ [[AA]] VV))
     179      [ >associative_plus //
     180      | @IH ]
     181    ]
     182    @(mem_monotonic_wrt_append)
     183    [ @ REFLEX
     184    | @(mem_monotonic_wrt_append)
     185      [ @ REFLEX
     186      | normalize
     187        > REFLEX
     188        normalize
     189        %
     190      ]
     191    ]
     192qed.
    61193(*
    62194lemma subvector_hd_tl:
     
    100232    whd in ⊢ (% → ?)
    101233  ]
     234  *)
    102235
    103236let rec list_addressing_mode_tags_elim
     
    140273      ]
    141274  ].
     275(*
    142276
    143277definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
    144278 λP.
    145279   P (ADD … ACC_A
    146    P (DA … ACC_A).
     280   P (DA … ACC_A).lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
     281 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
     282qed.
    147283 %
    148284qed.
     
    173309 
    174310(* RUSSEL **)
    175 
    176 include "basics/jmeq.ma".
    177 
    178 notation > "hvbox(a break ≃ b)"
    179   non associative with precedence 45
    180 for @{ 'jmeq ? $a ? $b }.
    181 
    182 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
    183   non associative with precedence 45
    184 for @{ 'jmeq $t $a $u $b }.
    185 
    186 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
    187311
    188312definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
Note: See TracChangeset for help on using the changeset viewer.