Changeset 328


Ignore:
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:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Plogic/equality.ma

    r268 r328  
    3232 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
    3333 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption.
     34nqed.
     35
     36nlemma eq_rect_Type0_r :
     37  ∀A: Type[0].
     38  ∀a:A.
     39  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
     40  #A a P H x p.
     41  ngeneralize in match H.
     42  ngeneralize in match P.
     43  ncases p.
     44  //.
    3445nqed.
    3546
  • Deliverables/D4.1/Matita/Vector.ma

    r322 r328  
    170170    ].
    171171
    172 (*
    173172nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0])
    174                       (n: Nat) (m: Nat)
    175                       (f: A → B → C → C) (c: C)
    176                       (v: Vector A n) (q: Vector B m) on v ≝
    177   (match v return λx.λ_. x = m → C with
     173                      (n: Nat) (f: A → B → C → C) (c: C)
     174                      (v: Vector A n) (q: Vector B n) on v ≝
     175  (match v return λx.λ_. x = n → C with
    178176    [ Empty ⇒
    179177      match q return λx.λ_. Z = x → C with
    180         [ Empty ⇒ λ_.c
     178        [ Empty ⇒ λprf: Z = Z. c
    181179        | Cons o hd tl ⇒ λabsd. ?
    182180        ]
    183181    | Cons o hd tl ⇒
    184182      match q return λx.λ_. S o = x → C with
    185         [ Empty ⇒ λabsd. ?
     183        [ Empty ⇒ λabsd: S o = Z. ?
    186184        | Cons p hd' tl' ⇒ λprf: S o = S p.
    187             fold_right_i A B C o p f (f hd hd') tl tl'
    188         ]
    189     ]) ?.
    190 *)
     185            fold_right_i A B C o f (f hd hd' c) tl ?
     186        ]
     187    ]) (refl ? n).
     188    ##[##1,2:
     189        ndestruct;
     190    ##| ndestruct (prf);
     191        napply tl';
     192    ##]
     193nqed.
    191194 
    192195nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
     
    207210    | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
    208211    ].
    209 
    210 (* Should be moved into Plogic/equality.ma at some point.  Only Type[2] version
    211    currently in there.
    212 *)
    213 nlemma eq_rect_Type0_r :
    214   ∀A: Type[0].
    215   ∀a:A.
    216   ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    217   #A a P H x p.
    218   ngeneralize in match H.
    219   ngeneralize in match P.
    220   ncases p.
    221   //.
    222 nqed.
    223212
    224213nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
     
    477466  @.
    478467nqed.
    479 
    480 naxiom eqv: ∀A,n. Vector A n → Vector A n → Bool.
  • Deliverables/D4.1/Matita/depends

    r316 r328  
     1Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
     2Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    13Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    3 Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
    44BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    55Cartesian.ma Universes.ma
     6Universes.ma
    67Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    78Either.ma Bool.ma Maybe.ma Universes.ma
    8 Universes.ma
    99ASM.ma BitVectorTrie.ma Either.ma String.ma
    10 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1110Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1211Char.ma Universes.ma
     12Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1313Connectives.ma Plogic/equality.ma
    1414Bool.ma Universes.ma
     
    1616List.ma Bool.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
    1717Util.ma Nat.ma
     18Compare.ma Universes.ma
    1819BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    19 Compare.ma Universes.ma
    2020String.ma Char.ma List.ma
    2121Plogic/equality.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.