Changeset 726 for src/ASM/Vector.ma


Ignore:
Timestamp:
Mar 30, 2011, 6:47:35 PM (10 years ago)
Author:
campbell
Message:

Change identifiers to Words in Clight and RTLabs semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r700 r726  
    429429(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    430430
     431definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
     432λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
     433[ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
     434
     435definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
     436λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
     437[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
     438
    431439let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
    432   (match b return λx.λ_. n = x → bool with
    433     [ VEmpty ⇒
    434       match c return λx.λ_. x = O → bool with
    435         [ VEmpty ⇒ λ_. true
    436         | VCons p hd tl ⇒ λabsd.⊥
    437         ]
    438     | VCons o hd tl ⇒
    439         match c return λx.λ_. x = S o → bool with
    440           [ VEmpty ⇒ λabsd.⊥
    441           | VCons p hd' tl' ⇒
    442             λprf.
    443               if (f hd hd') then
    444                 (eq_v A o f tl (tl'⌈Vector A p ↦ Vector A o⌉))
    445               else
    446                 false
    447           ]
    448     ]) (refl ? n).
    449     [1,2:
    450       destruct
    451     | lapply (injective_S … prf);
    452       # X
    453       < X
    454       %
    455     ]
    456 qed.
    457 
    458 lemma 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
     440  (match b return λx.λ_. Vector A x → bool with
     441   [ VEmpty ⇒ λc.
     442       match c return λx.λ_. match x return λ_.Type[0] with [ O ⇒ bool | _ ⇒ True ] with
     443       [ VEmpty ⇒ true
     444       | VCons p hd tl ⇒ I
     445       ]
     446   | VCons m hd tl ⇒ λc. andb (f hd (head' A m c)) (eq_v A m f tl (tail A m c))
     447   ]
     448  ) c.
     449
     450lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Type[0]. ∀v:Vector A n.
     451  match n return λn'. (Vector A n' → Type[0]) → Vector A n' → Type[0] with
    460452  [ O ⇒ λP.λv.P [[ ]] → P v
    461453  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
    462454  ] P v.
    463 @(λA,n. λP:Vector A n → Prop. λv. match v return
     455@(λA,n. λP:Vector A n → Type[0]. λv. match v return
    464456?
    465457with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P)
     
    469461*)
    470462
    471 (* dpm: commented out to get out stuff to typecheck *)
    472 lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
    473   (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
     463lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f.
     464  (∀Q:bool → Type[0]. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
    474465  ∀n,x,y.
    475466  (x = y → P true) →
Note: See TracChangeset for help on using the changeset viewer.