Changeset 268 for Deliverables/D4.1/Matita/Vector.ma

Timestamp:

Nov 23, 2010, 5:44:42 PM (9 years ago)

Author:

sacerdot

Message:

• notation moved to proper places
• new function split on Vectors

File:

• Deliverables/D4.1/Matita/Vector.ma (modified) (2 diffs)

Deliverables/D4.1/Matita/Vector.ma

@@ -5 +5 @@
 
 include "Util.ma".
-
-include "Universes.ma".
 
 include "Nat.ma".
@@ -133 +131 @@
     ].
     //.
+nqed.
+
+nlet rec split (A: Type[0]) (n,m: Nat) on m
+             : Vector A (m+n) → (Vector A m) × (Vector A n)
+≝
+ match m return λm. Vector A (m+n) → (Vector A m) × (Vector A n) with
+  [ Z ⇒ λv.〈[[ ]], v〉
+  | S m' ⇒ λv.
+     match v return λl.λ_:Vector A l.l = S (m' + n) → (Vector A (S m')) × (Vector A n) with
+      [ Empty ⇒ λK.⊥
+      | Cons o he tl ⇒ λK.
+         match split A n m' (tl⌈Vector A (m'+n)↦Vector A o⌉) with
+          [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
+//; ndestruct; //.
 nqed.