Changeset 2121


Ignore:
Timestamp:
Jun 27, 2012, 3:30:58 PM (5 years ago)
Author:
sacerdot
Message:

More functions moved to the places they belong to

Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2119 r2121  
    33include "ASM/StatusProofs.ma".
    44include alias "arithmetics/nat.ma".
    5 
    6 lemma mem_monotonic_wrt_append:
    7   ∀A: Type[0].
    8   ∀m, o: nat.
    9   ∀eq: A → A → bool.
    10   ∀reflex: ∀a. eq a a = true.
    11   ∀p: Vector A m.
    12   ∀a: A.
    13   ∀r: Vector A o.
    14     mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
    15   #A #m #o #eq #reflex #p #a
    16   elim p try (#r #assm assumption)
    17   #m' #hd #tl #inductive_hypothesis #r #assm
    18   normalize
    19   cases (eq ??) try %
    20   @inductive_hypothesis assumption
    21 qed.
    22 
    23 lemma subvector_multiple_append:
    24   ∀A: Type[0].
    25   ∀o, n: nat.
    26   ∀eq: A → A → bool.
    27   ∀refl: ∀a. eq a a = true.
    28   ∀h: Vector A o.
    29   ∀v: Vector A n.
    30   ∀m: nat.
    31   ∀q: Vector A m.
    32     bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
    33   #A #o #n #eq #reflex #h #v
    34   elim v try (normalize #m #irrelevant @I)
    35   #m' #hd #tl #inductive_hypothesis #m #q
    36   change with (bool_to_Prop (andb ??))
    37   cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
    38   [1:
    39     @mem_monotonic_wrt_append try assumption
    40     @mem_monotonic_wrt_append try assumption
    41     normalize >reflex %
    42   |2:
    43     #assm >assm
    44     >vector_cons_append
    45     change with (bool_to_Prop (subvector_with ??????))
    46     @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))
    47     try @associative_plus
    48     @inductive_hypothesis
    49   ]
    50 qed.
    51 
    52 lemma vector_cons_empty:
    53   ∀A: Type[0].
    54   ∀n: nat.
    55   ∀v: Vector A n.
    56     [[ ]] @@ v = v.
    57   #A #n #v
    58   cases v try %
    59   #n' #hd #tl %
    60 qed.
    615
    626lemma is_in_monotonic_wrt_append:
     
    9337qed.
    9438
     39(*CSC: move elsewhere *)
    9540definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
    9641  λa, b: addressing_mode.
     
    161106  ].
    162107
    163 lemma eq_bv_refl:
    164   ∀n, b.
    165     eq_bv n b b = true.
    166   #n #b cases b //
    167 qed.
    168 
    169 lemma eq_b_refl:
    170   ∀b.
    171     eq_b b b = true.
    172   #b cases b //
    173 qed.
    174 
     108(*CSC: move elsewhere *)
    175109lemma eq_addressing_mode_refl:
    176110  ∀a. eq_addressing_mode a a = true.
     
    181115qed.
    182116 
     117(*CSC: move elsewhere *)
    183118definition eq_sum:
    184119    ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
     
    197132    ].
    198133
     134(*CSC: move elsewhere *)
    199135definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
    200136  λlt, rt, leq, req, left, right.
     
    203139      leq l l' ∧ req r r'.
    204140
     141(*CSC: move elsewhere *)
    205142definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
    206143  λi, j.
     
    417354  ].
    418355
     356(*CSC: move elsewhere *)
    419357lemma eq_sum_refl:
    420358  ∀A, B: Type[0].
     
    428366qed.
    429367
     368(*CSC: move elsewhere *)
    430369lemma eq_prod_refl:
    431370  ∀A, B: Type[0].
     
    442381qed.
    443382
     383(*CSC: move elsewhere *)
    444384lemma eq_preinstruction_refl:
    445385  ∀i.
     
    546486qed.
    547487
     488(*CSC: move elsewhere *)
    548489definition eq_instruction: instruction → instruction → bool ≝
    549490  λi, j.
     
    591532  ].
    592533 
     534(*CSC: move elsewhere *)
    593535lemma eq_instruction_refl:
    594536  ∀i. eq_instruction i i = true.
     
    604546 λA,n,eq,v,a. mem A eq (S n) v a.
    605547
    606 definition tech_if_vect_member ≝
    607  λn,l,am,H.
    608   bool_inv_rect_Type0 (vect_member … n … eq_a l am) ? H (λ_.True).
    609 
     548(*CSC: move elsewhere*)
    610549definition is_in_cons_elim:
    611550 ∀len.∀hd,tl.∀m:addressing_mode
     
    616555qed.
    617556
    618 lemma vsplit_zero:
    619   ∀A,m.
    620   ∀v: Vector A m.
    621     〈[[]], v〉 = vsplit A 0 m v.
    622   #A #m #v
    623   cases v try %
    624   #n #hd #tl %
    625 qed.
    626 
    627 lemma Vector_O:
    628   ∀A: Type[0].
    629   ∀v: Vector A 0.
    630     v ≃ VEmpty A.
    631  #A #v
    632  generalize in match (refl … 0);
    633  cases v in ⊢ (??%? → ?%%??); //
    634  #n #hd #tl #absurd
    635  destruct(absurd)
    636 qed.
    637 
    638 lemma Vector_Sn:
    639   ∀A: Type[0].
    640   ∀n: nat.
    641   ∀v: Vector A (S n).
    642     ∃hd: A. ∃tl: Vector A n.
    643       v ≃ VCons A n hd tl.
    644   #A #n #v
    645   generalize in match (refl … (S n));
    646   cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
    647   [1:
    648     #absurd destruct(absurd)
    649   |2:
    650     #m #hd #tl #eq
    651     <(injective_S … eq)
    652     %{hd} %{tl} %
    653   ]
    654 qed.
    655 
    656 lemma vector_append_zero:
    657   ∀A,m.
    658   ∀v: Vector A m.
    659   ∀q: Vector A 0.
    660     v = q@@v.
    661   #A #m #v #q
    662   >(Vector_O A q) %
    663 qed.
    664 
     557(*CSC: move elsewhere*)
    665558lemma prod_eq_left:
    666559  ∀A: Type[0].
     
    671564qed.
    672565
     566(*CSC: move elsewhere*)
    673567lemma prod_eq_right:
    674568  ∀A: Type[0].
     
    677571  #A #p #q #r #hyp
    678572  destruct %
    679 qed.
    680 
    681 corollary prod_vector_zero_eq_left:
    682   ∀A, n.
    683   ∀q: Vector A O.
    684   ∀r: Vector A n.
    685     〈q, r〉 = 〈[[ ]], r〉.
    686   #A #n #q #r
    687   generalize in match (Vector_O A q …);
    688   #hyp destruct %
    689 qed.
    690 
    691 lemma tail_head:
    692   ∀a: Type[0].
    693   ∀m, n: nat.
    694   ∀hd: a.
    695   ∀l: Vector a m.
    696   ∀r: Vector a n.
    697     tail a ? (hd:::(l@@r)) = l@@r.
    698   #a #m #n #hd #l #r
    699   cases l try %
    700   #m' #hd' #tl' %
    701 qed.
    702 
    703 lemma head_head':
    704   ∀a: Type[0].
    705   ∀m: nat.
    706   ∀hd: a.
    707   ∀l: Vector a m.
    708     hd = head' … (hd:::l).
    709   #a #m #hd #l cases l try %
    710   #m' #hd' #tl %
    711 qed.
    712 
    713 lemma vsplit_succ:
    714   ∀A: Type[0].
    715   ∀m, n: nat.
    716   ∀l: Vector A m.
    717   ∀r: Vector A n.
    718   ∀v: Vector A (m + n).
    719   ∀hd: A.
    720     v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
    721   #A #m
    722   elim m
    723   [1:
    724     #n #l #r #v #hd #eq #hyp
    725     destruct >(Vector_O … l) %
    726   |2:
    727     #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
    728     destruct
    729     cases (Vector_Sn … l) #hd' #tl'
    730     whd in ⊢ (???%);
    731     >tail_head
    732     <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
    733     try (<hyp <head_head' %)
    734     elim l normalize //
    735   ]
    736 qed.
    737 
    738 lemma vsplit_prod:
    739   ∀A: Type[0].
    740   ∀m, n: nat.
    741   ∀p: Vector A (m + n).
    742   ∀v: Vector A m.
    743   ∀q: Vector A n.
    744     p = v@@q → 〈v, q〉 = vsplit A m n p.
    745   #A #m elim m
    746   [1:
    747     #n #p #v #q #hyp
    748     >hyp <(vector_append_zero A n q v)
    749     >(prod_vector_zero_eq_left A …)
    750     @vsplit_zero
    751   |2:
    752     #r #ih #n #p #v #q #hyp
    753     >hyp
    754     cases (Vector_Sn A r v) #hd #exists
    755     cases exists #tl #jmeq
    756     >jmeq @vsplit_succ try %
    757     @ih %
    758   ]
    759 qed.
    760 
    761 definition vsplit_elim:
    762   ∀A: Type[0].
    763   ∀l, m: nat.
    764   ∀v: Vector A (l + m).
    765   ∀P: (Vector A l) × (Vector A m) → Prop.
    766     (∀vl: Vector A l.
    767      ∀vm: Vector A m.
    768       v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
    769   λa: Type[0].
    770   λl, m: nat.
    771   λv: Vector a (l + m).
    772   λP. ?.
    773   cases daemon
    774573qed.
    775574
     
    785584  ].
    786585
     586(*CSC: move elsewhere *)
    787587lemma add_bitvector_of_nat_Sm:
    788588  ∀n, m: nat.
     
    824624qed.
    825625
     626(*CSC: move elsewhere*)
    826627lemma destruct_bug_fix_1:
    827628  ∀n: nat.
     
    830631qed.
    831632
     633(*CSC: move elsewhere*)
    832634lemma destruct_bug_fix_2:
    833635  ∀m, n: nat.
     
    836638qed.
    837639
     640(*CSC: move elsewhere*)
    838641definition bitvector_3_cases:
    839642  ∀b: BitVector 3.
     
    884687qed.
    885688
     689(*CSC: move elsewhere*)
    886690lemma bitvector_3_elim_prop:
    887691  ∀P: BitVector 3 → Prop.
     
    947751  ].
    948752
     753(*CSC: move elsewhere*)
    949754lemma option_destruct_Some:
    950755  ∀A: Type[0].
     
    955760qed.
    956761
     762(*CSC: move elsewhere*)
    957763lemma eq_instruction_to_eq:
    958764  ∀i1, i2: instruction.
     
    16231429     ticks_of0 program sigma policy ppc fetched.
    16241430
     1431(*CSC: move elsewhere*)
    16251432lemma eq_rect_Type1_r:
    16261433  ∀A: Type[1].
     
    16331440qed.
    16341441
    1635 axiom vsplit_append:
    1636   ∀A: Type[0].
    1637   ∀m, n: nat.
    1638   ∀v, v': Vector A m.
    1639   ∀q, q': Vector A n.
    1640     let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
    1641       v = v' ∧ q = q'.
    1642 
    1643 lemma vsplit_vector_singleton:
    1644   ∀A: Type[0].
    1645   ∀n: nat.
    1646   ∀v: Vector A (S n).
    1647   ∀rest: Vector A n.
    1648   ∀s: Vector A 1.
    1649     v = s @@ rest →
    1650     ((get_index_v A ? v 0 ?) ::: rest) = v.
    1651   [1:
    1652     #A #n #v cases daemon (* XXX: !!! *)
    1653   |2:
    1654     @le_S_S @le_O_n
    1655   ]
    1656 qed.
    1657 
     1442(*CSC: move elsewhere*)
    16581443example sub_minus_one_seven_eight:
    16591444  ∀v: BitVector 7.
     
    17921577*)
    17931578
     1579(*CSC: move elsewhere*)
    17941580lemma Some_Some_elim:
    17951581 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
     
    17971583qed.
    17981584
     1585(*CSC: move elsewhere*)
    17991586lemma pair_destruct_right:
    18001587  ∀A: Type[0].
     
    18561643qed.
    18571644
     1645(*CSC: move elsewhere*)
    18581646lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
    18591647  /2/
  • src/ASM/AssemblyProofSplit.ma

    r2114 r2121  
    170170qed.
    171171
     172(*CSC: move elsewhere*)
    172173lemma pair_replace:
    173174 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →
     
    326327qed.
    327328
     329(*CSC: move elsewhere*)
    328330lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
    329331 #P #A #a #abs destruct
     
    359361include alias "ASM/BitVectorTrie.ma".
    360362
     363(*CSC: move elsewhere*)
    361364lemma jmpair_as_replace:
    362365 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c.
     
    375378qed.
    376379
     380(*CSC: move elsewhere*)
    377381lemma if_then_else_replace:
    378382  ∀T: Type[0].
     
    396400qed.
    397401
     402(*CSC: move elsewhere*)
    398403lemma refl_to_jmrefl:
    399404  ∀a: Type[0].
  • src/ASM/BitVector.ma

    r2006 r2121  
    129129    else
    130130      notb c.
     131
     132lemma eq_b_refl:
     133  ∀b.
     134    eq_b b b = true.
     135  #b cases b //
     136qed.
    131137
    132138lemma eq_b_eq:
  • src/ASM/Vector.ma

    r2032 r2121  
    2121  VEmpty: Vector A O
    2222| VCons: ∀n: nat. A → Vector A n → Vector A (S n).
     23
     24lemma Vector_O:
     25  ∀A: Type[0].
     26  ∀v: Vector A 0.
     27    v ≃ VEmpty A.
     28 #A #v
     29 generalize in match (refl … 0);
     30 cases v in ⊢ (??%? → ?%%??); //
     31 #n #hd #tl #absurd
     32 destruct(absurd)
     33qed.
     34
     35lemma Vector_Sn:
     36  ∀A: Type[0].
     37  ∀n: nat.
     38  ∀v: Vector A (S n).
     39    ∃hd: A. ∃tl: Vector A n.
     40      v ≃ VCons A n hd tl.
     41  #A #n #v
     42  generalize in match (refl … (S n));
     43  cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
     44  [1:
     45    #absurd destruct(absurd)
     46  |2:
     47    #m #hd #tl #eq
     48    <(injective_S … eq)
     49    %{hd} %{tl} %
     50  ]
     51qed.
    2352
    2453(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    194223 vsplit' A m n v.
    195224
     225lemma vsplit_zero:
     226  ∀A,m.
     227  ∀v: Vector A m.
     228    〈[[]], v〉 = vsplit A 0 m v.
     229  #A #m #v
     230  cases v try %
     231  #n #hd #tl %
     232qed.
     233
    196234definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
    197235  λA: Type[0].
     
    326364   
    327365interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
     366
     367lemma vector_append_zero:
     368  ∀A,m.
     369  ∀v: Vector A m.
     370  ∀q: Vector A 0.
     371    v = q@@v.
     372  #A #m #v #q
     373  >(Vector_O A q) %
     374qed.
     375
     376lemma vector_cons_empty:
     377  ∀A: Type[0].
     378  ∀n: nat.
     379  ∀v: Vector A n.
     380    [[ ]] @@ v = v.
     381  #A #n #v
     382  cases v try %
     383  #n' #hd #tl %
     384qed.
    328385
    329386lemma vector_cons_append:
     
    367424qed.
    368425
     426lemma tail_head:
     427  ∀a: Type[0].
     428  ∀m, n: nat.
     429  ∀hd: a.
     430  ∀l: Vector a m.
     431  ∀r: Vector a n.
     432    tail a ? (hd:::(l@@r)) = l@@r.
     433  #a #m #n #hd #l #r
     434  cases l try %
     435  #m' #hd' #tl' %
     436qed.
     437
     438lemma head_head':
     439  ∀a: Type[0].
     440  ∀m: nat.
     441  ∀hd: a.
     442  ∀l: Vector a m.
     443    hd = head' … (hd:::l).
     444  #a #m #hd #l cases l try %
     445  #m' #hd' #tl %
     446qed.
     447
    369448axiom vsplit_elim':
    370449  ∀A: Type[0].
     
    386465      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt)
    387466        (let 〈lft, rgt〉 ≝ vsplit A l m v in T' lft rgt).
    388    
     467
     468lemma vsplit_succ:
     469  ∀A: Type[0].
     470  ∀m, n: nat.
     471  ∀l: Vector A m.
     472  ∀r: Vector A n.
     473  ∀v: Vector A (m + n).
     474  ∀hd: A.
     475    v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
     476  #A #m
     477  elim m
     478  [1:
     479    #n #l #r #v #hd #eq #hyp
     480    destruct >(Vector_O … l) %
     481  |2:
     482    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
     483    destruct
     484    cases (Vector_Sn … l) #hd' #tl'
     485    whd in ⊢ (???%);
     486    >tail_head
     487    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
     488    try (<hyp <head_head' %)
     489    elim l normalize //
     490  ]
     491qed.
     492
     493corollary prod_vector_zero_eq_left:
     494  ∀A, n.
     495  ∀q: Vector A O.
     496  ∀r: Vector A n.
     497    〈q, r〉 = 〈[[ ]], r〉.
     498  #A #n #q #r
     499  generalize in match (Vector_O A q …);
     500  #hyp destruct %
     501qed.
     502
     503lemma vsplit_prod:
     504  ∀A: Type[0].
     505  ∀m, n: nat.
     506  ∀p: Vector A (m + n).
     507  ∀v: Vector A m.
     508  ∀q: Vector A n.
     509    p = v@@q → 〈v, q〉 = vsplit A m n p.
     510  #A #m elim m
     511  [1:
     512    #n #p #v #q #hyp
     513    >hyp <(vector_append_zero A n q v)
     514    >(prod_vector_zero_eq_left A …)
     515    @vsplit_zero
     516  |2:
     517    #r #ih #n #p #v #q #hyp
     518    >hyp
     519    cases (Vector_Sn A r v) #hd #exists
     520    cases exists #tl #jmeq
     521    >jmeq @vsplit_succ try %
     522    @ih %
     523  ]
     524qed.
     525
     526definition vsplit_elim:
     527  ∀A: Type[0].
     528  ∀l, m: nat.
     529  ∀v: Vector A (l + m).
     530  ∀P: (Vector A l) × (Vector A m) → Prop.
     531    (∀vl: Vector A l.
     532     ∀vm: Vector A m.
     533      v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
     534  λa: Type[0].
     535  λl, m: nat.
     536  λv: Vector a (l + m).
     537  λP. ?.
     538  cases daemon
     539qed.
     540
     541axiom vsplit_append:
     542  ∀A: Type[0].
     543  ∀m, n: nat.
     544  ∀v, v': Vector A m.
     545  ∀q, q': Vector A n.
     546    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
     547      v = v' ∧ q = q'.
     548
     549lemma vsplit_vector_singleton:
     550  ∀A: Type[0].
     551  ∀n: nat.
     552  ∀v: Vector A (S n).
     553  ∀rest: Vector A n.
     554  ∀s: Vector A 1.
     555    v = s @@ rest →
     556    ((get_index_v A ? v 0 ?) ::: rest) = v.
     557  [1:
     558    #A #n #v cases daemon (* XXX: !!! *)
     559  |2:
     560    @le_S_S @le_O_n
     561  ]
     562qed.
     563
    389564let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
    390565                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
     
    593768qed.
    594769
     770lemma mem_monotonic_wrt_append:
     771  ∀A: Type[0].
     772  ∀m, o: nat.
     773  ∀eq: A → A → bool.
     774  ∀reflex: ∀a. eq a a = true.
     775  ∀p: Vector A m.
     776  ∀a: A.
     777  ∀r: Vector A o.
     778    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
     779  #A #m #o #eq #reflex #p #a
     780  elim p try (#r #assm assumption)
     781  #m' #hd #tl #inductive_hypothesis #r #assm
     782  normalize
     783  cases (eq ??) try %
     784  @inductive_hypothesis assumption
     785qed.
     786
     787
    595788let rec subvector_with
    596789  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
     
    622815 #A #n #eq #refl #v @(subvector_with_refl0 … v … [[]]) //
    623816qed.
     817
     818lemma subvector_multiple_append:
     819  ∀A: Type[0].
     820  ∀o, n: nat.
     821  ∀eq: A → A → bool.
     822  ∀refl: ∀a. eq a a = true.
     823  ∀h: Vector A o.
     824  ∀v: Vector A n.
     825  ∀m: nat.
     826  ∀q: Vector A m.
     827    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
     828  #A #o #n #eq #reflex #h #v
     829  elim v try (normalize #m #irrelevant @I)
     830  #m' #hd #tl #inductive_hypothesis #m #q
     831  change with (bool_to_Prop (andb ??))
     832  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
     833  [1:
     834    @mem_monotonic_wrt_append try assumption
     835    @mem_monotonic_wrt_append try assumption
     836    normalize >reflex %
     837  |2:
     838    #assm >assm
     839    >vector_cons_append
     840    change with (bool_to_Prop (subvector_with ??????))
     841    @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))
     842    try @associative_plus
     843    @inductive_hypothesis
     844  ]
     845qed.
     846
     847
    624848
    625849(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.