Changeset 268 for Deliverables/D4.1/Matita

Timestamp:

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

Author:

sacerdot

Message:

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

Location:

Deliverables/D4.1/Matita

Files:

• ASM.ma (modified) (1 diff)
• BitVectorTrie.ma (modified) (1 diff)
• Bool.ma (modified) (1 diff)
• Cartesian.ma (modified) (1 diff)
• Connectives.ma (modified) (1 diff)
• Either.ma (modified) (1 diff)
• Equality.ma (deleted)
• Exponential.ma (modified) (1 diff)
• Plogic/equality.ma (modified) (1 diff)
• Vector.ma (modified) (2 diffs)
• depends (modified) (3 diffs)

Deliverables/D4.1/Matita/ASM.ma

@@ -2 +2 @@
 include "BitVectorTrie.ma".
 include "String.ma".
-
-interpretation "Cartesian" 'product A B = (Cartesian A B).
-notation "hvbox(a break ⊎ b)"
- left associative with precedence 50
-for @{ 'disjoint_union $a $b }.
-interpretation "Either" 'disjoint_union A B = (Either A B).
-interpretation "Bool" 'or a b = (inclusive_disjunction a b).
 
 ninductive addressing_mode: Type[0] ≝

Deliverables/D4.1/Matita/BitVectorTrie.ma

@@ -8 +8 @@
 | Node: ∀n: Nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
 | Stub: ∀n: Nat. BitVectorTrie A n.
-
-notation "hvbox(t⌈h ↦ o⌉)"
-  with precedence 45
-  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
-
-notation "⊥" with precedence 90
-  for @{ match ? in False with [ ] }.
 
 nlet rec lookup (A: Type[0]) (n: Nat)

Deliverables/D4.1/Matita/Bool.ma

@@ -44 +44 @@
     ].
 
+interpretation "Bool" 'or a b = (inclusive_disjunction a b).
+
 nlet rec negation (b: Bool) on b ≝
   match b with

Deliverables/D4.1/Matita/Cartesian.ma

@@ -2 +2 @@
 
 nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝
-{
-  first: A;
+{ first: A;
   second: B
 }.
 
-notation "(l,r)"
-  non associative with precedence 90
-  for @{ 'cartesian $l $r }.
-  
-interpretation "Cartesian product" 'cartesian l r = (mk_Cartesian ? ? l r).
+interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r).
+interpretation "Cartesian" 'product A B = (Cartesian A B).

Deliverables/D4.1/Matita/Connectives.ma

@@ -30 +30 @@
 ninductive Not (A:Prop): Prop ≝
 nmk: (A → False) → Not A.
+
+notation "⊥" with precedence 90
+  for @{ match ? in False with [ ] }.
 
 interpretation "logical not" 'not x = (Not x).

Deliverables/D4.1/Matita/Either.ma

@@ -7 +7 @@
   Left: A → Either A B
 | Right: B → Either A B.
+
+notation "hvbox(a break ⊎ b)"
+ left associative with precedence 50
+for @{ 'disjoint_union $a $b }.
+interpretation "Either" 'disjoint_union A B = (Either A B).
 
 ndefinition is_left ≝

Deliverables/D4.1/Matita/Exponential.ma

@@ -5 +5 @@
 include "Nat.ma".
 
-include "Equality.ma".
+include "Plogic/equality.ma".
 include "Connectives.ma".
 

Deliverables/D4.1/Matita/Plogic/equality.ma

@@ -17 +17 @@
 ninductive eq (A:Type[2]) (x:A) : A → Prop ≝
     refl: eq A x x.
-    
+
+notation "hvbox(t⌈h ↦ o⌉)"
+  with precedence 45
+  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
+ 
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 

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.
     

Deliverables/D4.1/Matita/depends

@@ -1 +1 @@
 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
-Exponential.ma Connectives.ma Equality.ma Nat.ma
+Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
 BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
 Cartesian.ma Universes.ma
@@ -7 +7 @@
 Universes.ma 
 ASM.ma BitVectorTrie.ma Either.ma String.ma
-Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
+Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
 Char.ma Universes.ma
 Connectives.ma Plogic/equality.ma
@@ -20 +20 @@
 Plogic/equality.ma Universes.ma
 Nat.ma Bool.ma Cartesian.ma Connectives.ma
-Equality.ma Universes.ma