Ignore:
Timestamp:
Dec 1, 2010, 11:18:05 AM (9 years ago)
Author:
mulligan
Message:

Added fold_right_i (with dependent type) to List file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/List.ma

    r342 r349  
    216216    ].
    217217   
     218nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0])
     219                      (f: A → B → C → C) (c: C)
     220                      (l: List A) (r: List B) (p: length ? l = length ? r) on l: C ≝
     221  (match l return λx. (length ? x) = (length ? r) → C with
     222    [ Empty ⇒
     223      match r return λx. Z = length ? x → C with
     224        [ Empty ⇒ λprf: Z = Z. c
     225        | Cons hd tl ⇒ λabsd. ?
     226        ]
     227    | Cons hd tl ⇒
     228      match r return λx. S (length ? tl) = length ? x → C with
     229        [ Empty ⇒ λabsd: S(length ? tl) = Z. ?
     230        | Cons hd' tl' ⇒ λprf: S(length ? tl) = length ? (hd'::tl').
     231            fold_right_i A B C f (f hd hd' c) tl tl' ?
     232        ]
     233    ]) p.
     234    ##[##1,2:
     235        nnormalize in absd;
     236        ndestruct (absd);
     237    ##|##3:
     238        nnormalize in prf;
     239        ndestruct (prf);
     240        nassumption;
     241    ##]
     242nqed.
     243   
    218244nlet rec fold_left (A: Type[0]) (B: Type[0])
    219245                   (f: A → B → A) (x: A) (l: List B) on l ≝
     
    223249    ].
    224250
    225 nlet rec fold_lefti_aux (A: Type[0]) (B: Type[0])
     251nlet rec fold_left_i_aux (A: Type[0]) (B: Type[0])
    226252                   (f: Nat → A → B → A) (x: A) (i: Nat) (l: List B) on l ≝
    227253  match l with
    228254    [ Empty ⇒ x
    229     | Cons hd tl ⇒ f i (fold_lefti_aux A B f x (S i) tl) hd
    230     ].
    231 
    232 ndefinition fold_lefti ≝ λA,B,f,x. fold_lefti_aux A B f x Z.
     255    | Cons hd tl ⇒ f i (fold_left_i_aux A B f x (S i) tl) hd
     256    ].
     257
     258ndefinition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x Z.
    233259   
    234260(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.