Changeset 328

Timestamp:

Nov 29, 2010, 11:17:58 AM (9 years ago)

Author:

mulligan

Message:

Got fold_right_i to type check. Moved eq_rect_Type0 into Plogic/equality.ma. Added new file for main processor execution loop.

Location:

Deliverables/D4.1/Matita

Files:

• Interpret.ma (added)
• Plogic/equality.ma (modified) (1 diff)
• Vector.ma (modified) (3 diffs)
• depends (modified) (2 diffs)

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

@@ -32 +32 @@
  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption.
+nqed.
+
+nlemma eq_rect_Type0_r :
+  ∀A: Type[0].
+  ∀a:A.
+  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
+  #A a P H x p.
+  ngeneralize in match H.
+  ngeneralize in match P.
+  ncases p.
+  //.
 nqed.
 

Deliverables/D4.1/Matita/Vector.ma

@@ -170 +170 @@
     ].
 
-(* 
 nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0])
-                      (n: Nat) (m: Nat)
-                      (f: A → B → C → C) (c: C)
-                      (v: Vector A n) (q: Vector B m) on v ≝
-  (match v return λx.λ_. x = m → C with
+                      (n: Nat) (f: A → B → C → C) (c: C)
+                      (v: Vector A n) (q: Vector B n) on v ≝
+  (match v return λx.λ_. x = n → C with
     [ Empty ⇒
       match q return λx.λ_. Z = x → C with
-        [ Empty ⇒ λ_.c
+        [ Empty ⇒ λprf: Z = Z. c
         | Cons o hd tl ⇒ λabsd. ?
         ]
     | Cons o hd tl ⇒ 
       match q return λx.λ_. S o = x → C with
-        [ Empty ⇒ λabsd. ?
+        [ Empty ⇒ λabsd: S o = Z. ?
         | Cons p hd' tl' ⇒ λprf: S o = S p.
-            fold_right_i A B C o p f (f hd hd') tl tl'
-        ]
-    ]) ?.
-*)
+            fold_right_i A B C o f (f hd hd' c) tl ?
+        ]
+    ]) (refl ? n).
+    ##[##1,2:
+        ndestruct;
+    ##| ndestruct (prf);
+        napply tl';
+    ##]
+nqed.
   
 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
@@ -207 +210 @@
     | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
     ].
-
-(* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
-   currently in there.
-*)
-nlemma eq_rect_Type0_r :
-  ∀A: Type[0].
-  ∀a:A.
-  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
-  #A a P H x p.
-  ngeneralize in match H.
-  ngeneralize in match P.
-  ncases p.
-  //.
-nqed.
 
 nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
@@ -477 +466 @@
   @.
 nqed.
-
-naxiom eqv: ∀A,n. Vector A n → Vector A n → Bool.

Deliverables/D4.1/Matita/depends

@@ +1 @@
+Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
+Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
-Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
-Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
 BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
 Cartesian.ma Universes.ma
+Universes.ma 
 Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
 Either.ma Bool.ma Maybe.ma Universes.ma
-Universes.ma 
 ASM.ma BitVectorTrie.ma Either.ma String.ma
-Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
 Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
 Char.ma Universes.ma
+Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
 Connectives.ma Plogic/equality.ma
 Bool.ma Universes.ma
@@ -16 +16 @@
 List.ma Bool.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
 Util.ma Nat.ma
+Compare.ma Universes.ma
 BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
-Compare.ma Universes.ma
 String.ma Char.ma List.ma
 Plogic/equality.ma Universes.ma