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

More functions moved to the places they belong to

File:
1 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/
Note: See TracChangeset for help on using the changeset viewer.