Changeset 697 for src/ASM/Vector.ma

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:

• . (modified) (1 prop)
• Vector.ma (modified) (8 diffs)

src/ASM/Vector.ma

@@ -6 +6 @@
 include "basics/list.ma".
 include "basics/bool.ma".
-include "basics/sums.ma".
+include "basics/types.ma".
 
 include "cerco/Util.ma".
@@ -12 +12 @@
 include "arithmetics/nat.ma".
 
+include "oldlib/eq.ma".
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
@@ -159 +160 @@
       | VCons o he tl ⇒ λK.
         match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with
-        [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉
+        [ pair v1 v2 ⇒ 〈he:::v1, v2〉
         ]
       ] (?: (S (m' + n)) = S (m' + n))].
@@ -200 +201 @@
     ].
 
+let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
+                     (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
+  match v with
+    [ VEmpty ⇒ x
+    | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
+    ].
+
 let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
                       (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
@@ -228 +236 @@
   match v with
     [ VEmpty ⇒ x
-    | VCons n hd tl ⇒ f (fold_left A B n f x tl) hd
+    | VCons n hd tl ⇒ fold_left A B n f (f x hd) tl
     ].
     
@@ -269 +277 @@
   λv: Vector A n.
   λq: Vector B n.
-    zip_with A B (A × B) n (mk_pair A B) v q.
+    zip_with A B (A × B) n (pair A B) v q.
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
@@ -319 +327 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 
-let rec reverse (A: Type[0]) (n: nat)
-                 (v: Vector A n) on v ≝
-  match v return (λm.λv. Vector A m) with
-    [ VEmpty ⇒ [[ ]]
-    | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]])
-    ].
-    //
-qed.
+(* At some points matita will attempt to reduce reverse with a known vector,
+   which reduces the equality proof for the cast.  Normalising this proof needs
+   to be fast enough to keep matita usable. *)
+let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
+match n return λn'.∀m.S(n'+m) = n'+S m with
+[ O ⇒ λm.refl ??
+| S n' ⇒ λm. ?
+]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
+
+let rec revapp (A: Type[0]) (n: nat) (m:nat)
+                (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
+  match v return λn'.λ_. Vector A (n' + m) with
+    [ VEmpty ⇒ acc
+    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
+    ].
+> plus_n_Sm_fast @refl qed.
+
+let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
+  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
+< plus_n_O @refl qed.
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
@@ -436 +456 @@
 qed.
 
+lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n.
+  match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with
+  [ O ⇒ λP.λv.P [[ ]] → P v
+  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
+  ] P v.
+@(λA,n. λP:Vector A n → Prop. λv. match v return
+?
+with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P)
+[ // | // ] qed.
+(* XXX Proof below fails at qed.
+#A #n #P * [ #H @H | #m #h #t #H @H ] qed.
+*)
+
+lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
+  (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
+  ∀n,x,y.
+  (x = y → P true) →
+  (x ≠ y → P false) →
+  P (eq_v A n f x y).
+#P #A #f #f_elim #n #x elim x
+[ #y @(vector_inv_n … y)
+  normalize /2/
+| #m #h #t #IH #y @(vector_inv_n … y)
+  #h' #t' #Ht #Hf whd in ⊢ (?%)
+  @(f_elim ? h h') #Eh
+  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
+  | @Hf % #E' destruct (E') elim Eh /2/
+  ]
+] qed.
+
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 (* Subvectors.                                                                *)