Changeset 697 for src/ASM/Vector.ma


Ignore:
Timestamp:
Mar 18, 2011, 1:28:33 PM (9 years ago)
Author:
campbell
Message:

Merge Clight branch of vectors and friends.
Start making stuff build.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM

  • src/ASM/Vector.ma

    r690 r697  
    66include "basics/list.ma".
    77include "basics/bool.ma".
    8 include "basics/sums.ma".
     8include "basics/types.ma".
    99
    1010include "cerco/Util.ma".
     
    1212include "arithmetics/nat.ma".
    1313
     14include "oldlib/eq.ma".
    1415
    1516(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    159160      | VCons o he tl ⇒ λK.
    160161        match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with
    161         [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉
     162        [ pair v1 v2 ⇒ 〈he:::v1, v2〉
    162163        ]
    163164      ] (?: (S (m' + n)) = S (m' + n))].
     
    200201    ].
    201202
     203let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
     204                     (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
     205  match v with
     206    [ VEmpty ⇒ x
     207    | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
     208    ].
     209
    202210let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
    203211                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
     
    228236  match v with
    229237    [ VEmpty ⇒ x
    230     | VCons n hd tl ⇒ f (fold_left A B n f x tl) hd
     238    | VCons n hd tl ⇒ fold_left A B n f (f x hd) tl
    231239    ].
    232240   
     
    269277  λv: Vector A n.
    270278  λq: Vector B n.
    271     zip_with A B (A × B) n (mk_pair A B) v q.
     279    zip_with A B (A × B) n (pair A B) v q.
    272280
    273281(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    319327(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    320328
    321 let rec reverse (A: Type[0]) (n: nat)
    322                  (v: Vector A n) on v ≝
    323   match v return (λm.λv. Vector A m) with
    324     [ VEmpty ⇒ [[ ]]
    325     | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]])
    326     ].
    327     //
    328 qed.
     329(* At some points matita will attempt to reduce reverse with a known vector,
     330   which reduces the equality proof for the cast.  Normalising this proof needs
     331   to be fast enough to keep matita usable. *)
     332let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
     333match n return λn'.∀m.S(n'+m) = n'+S m with
     334[ O ⇒ λm.refl ??
     335| S n' ⇒ λm. ?
     336]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
     337
     338let rec revapp (A: Type[0]) (n: nat) (m:nat)
     339                (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
     340  match v return λn'.λ_. Vector A (n' + m) with
     341    [ VEmpty ⇒ acc
     342    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
     343    ].
     344> plus_n_Sm_fast @refl qed.
     345
     346let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
     347  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
     348< plus_n_O @refl qed.
    329349
    330350(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    436456qed.
    437457
     458lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n.
     459  match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with
     460  [ O ⇒ λP.λv.P [[ ]] → P v
     461  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
     462  ] P v.
     463@(λA,n. λP:Vector A n → Prop. λv. match v return
     464?
     465with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P)
     466[ // | // ] qed.
     467(* XXX Proof below fails at qed.
     468#A #n #P * [ #H @H | #m #h #t #H @H ] qed.
     469*)
     470
     471lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
     472  (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
     473  ∀n,x,y.
     474  (x = y → P true) →
     475  (x ≠ y → P false) →
     476  P (eq_v A n f x y).
     477#P #A #f #f_elim #n #x elim x
     478[ #y @(vector_inv_n … y)
     479  normalize /2/
     480| #m #h #t #IH #y @(vector_inv_n … y)
     481  #h' #t' #Ht #Hf whd in ⊢ (?%)
     482  @(f_elim ? h h') #Eh
     483  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
     484  | @Hf % #E' destruct (E') elim Eh /2/
     485  ]
     486] qed.
     487
    438488(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    439489(* Subvectors.                                                                *)
Note: See TracChangeset for help on using the changeset viewer.