Changeset 2032 for src/ASM/Vector.ma


Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (8 years ago)
Author:
sacerdot
Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r1908 r2032  
    4040  non associative with precedence 90
    4141  for @{ 'get_index_v $l $n }.
     42
     43lemma dependent_rewrite_vectors:
     44  ∀A:Type[0].
     45  ∀n, m: nat.
     46  ∀v1: Vector A n.
     47  ∀v2: Vector A m.
     48  ∀P: ∀m. Vector A m → Prop.
     49    n = m → v1 ≃ v2 → P n v1 → P m v2.
     50  #A #n #m #v1 #v2 #P #eq #jmeq
     51  destruct #assm assumption
     52qed.
     53
     54lemma jmeq_cons_vector_monotone:
     55  ∀A: Type[0].
     56  ∀m, n: nat.
     57  ∀v: Vector A m.
     58  ∀q: Vector A n.
     59  ∀prf: m = n.
     60  ∀hd: A.
     61    v ≃ q → hd:::v ≃ hd:::q.
     62  #A #m #n #v #q #prf #hd #E
     63  @(dependent_rewrite_vectors A … E)
     64  try assumption %
     65qed.
    4266
    4367(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    161185[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
    162186
    163 let rec split' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
     187let rec vsplit' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
    164188 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
    165189  [ O ⇒ λv. 〈[[ ]], v〉
    166   | S m' ⇒ λv. let 〈l,r〉 ≝ split' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
     190  | S m' ⇒ λv. let 〈l,r〉 ≝ vsplit' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
    167191  ].
    168192(* Prevent undesirable unfolding. *)
    169 let rec split (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
    170  split' A m n v.
     193let rec vsplit (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
     194 vsplit' A m n v.
    171195
    172196definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
     
    303327interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
    304328
    305 axiom split_elim':
     329lemma vector_cons_append:
     330  ∀A: Type[0].
     331  ∀n: nat.
     332  ∀e: A.
     333  ∀v: Vector A n.
     334    e ::: v = [[ e ]] @@ v.
     335  #A #n #e #v
     336  cases v try %
     337  #n' #hd #tl %
     338qed.
     339
     340lemma vector_cons_append2:
     341  ∀A: Type[0].
     342  ∀n, m: nat.
     343  ∀v: Vector A n.
     344  ∀q: Vector A m.
     345  ∀hd: A.
     346    hd:::(v@@q) = (hd:::v)@@q.
     347  #A #n #m #v #q
     348  elim v try (#hd %)
     349  #n' #hd' #tl' #ih #hd'
     350  <ih %
     351qed.
     352
     353lemma vector_associative_append:
     354  ∀A: Type[0].
     355  ∀n, m, o:  nat.
     356  ∀v: Vector A n.
     357  ∀q: Vector A m.
     358  ∀r: Vector A o.
     359    (v @@ q) @@ r ≃ v @@ (q @@ r).
     360  #A #n #m #o #v #q #r
     361  elim v try %
     362  #n' #hd #tl #ih
     363  <(vector_cons_append2 A … hd)
     364  @jmeq_cons_vector_monotone
     365  try assumption
     366  @associative_plus
     367qed.
     368
     369axiom vsplit_elim':
    306370  ∀A: Type[0].
    307371  ∀B: Type[1].
     
    310374  ∀P: B → Prop.
    311375    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
    312       P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
    313 
    314 axiom split_elim'':
     376      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt).
     377
     378axiom vsplit_elim'':
    315379  ∀A: Type[0].
    316380  ∀B,B': Type[1].
     
    320384  ∀P: B → B' → Prop.
    321385    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
    322       P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
    323         (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
     386      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt)
     387        (let 〈lft, rgt〉 ≝ vsplit A l m v in T' lft rgt).
    324388   
    325389let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
     
    432496  λv: Vector A (S n).
    433497  λa: A.
    434     let 〈v',dropped〉 ≝ split ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
     498    let 〈v',dropped〉 ≝ vsplit ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
    435499(*    reverse … (shift_left_1 … (reverse … v) a).*)
    436500
     
    441505    [ nat_lt _ _ ⇒ λv,a. replicate … a
    442506    | nat_eq _   ⇒ λv,a. replicate … a
    443     | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ split … v in switch_bv_plus … (v' @@ (replicate … a))
     507    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ vsplit … v in switch_bv_plus … (v' @@ (replicate … a))
    444508    ].
    445509
     
    522586  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
    523587
     588lemma mem_append: ∀A,eq_a. (∀x. eq_a x x = true) → ∀n,m.∀v: Vector A n. ∀w: Vector A m. ∀x. mem A eq_a … (v@@x:::w) x.
     589 #A #eq_a #refl #n #m #v elim v
     590 [ #w #x whd whd in match (mem ?????); >refl //
     591 | /2/
     592 ]
     593qed.
     594
    524595let rec subvector_with
    525596  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
     
    533604      false
    534605  ].
    535    
     606
     607lemma subvector_with_refl0:
     608 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
     609  ∀m. ∀w: Vector A m. subvector_with A … eq v (w@@v).
     610 #A #n #eq #refl #v elim v
     611 [ //
     612 | #m #hd #tl #IH #m #w whd in match (subvector_with ??????); >mem_append //
     613   change with (bool_to_Prop (subvector_with ??????)) lapply (IH … (w@@[[hd]]))
     614  lapply (vector_associative_append ???? w [[hd]] tl) #EQ
     615  @(dependent_rewrite_vectors … EQ) //
     616 ]
     617qed.
     618
     619lemma subvector_with_refl:
     620 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
     621  subvector_with A … eq v v.
     622 #A #n #eq #refl #v @(subvector_with_refl0 … v … [[]]) //
     623qed.
     624
    536625(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    537626(* Lemmas.                                                                    *)
Note: See TracChangeset for help on using the changeset viewer.