Changeset 349


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.

Location:
Deliverables/D4.1/Matita
Files:
4 edited

Legend:

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

    r313 r349  
    146146  nassumption;
    147147nqed.
     148
     149ndefinition full_add:
     150  ∀n: Nat.
     151  ∀b, c: BitVector n.
     152  ∀d: Bit.
     153    fold_left_i ? ? (
     154      λb1, b2: Bool.
     155      λd.
     156        let 〈c1,r〉 ≝ d in
     157          〈inclusive_disjunction (conjunction b1 b2)
     158                                 (conjunction c1 (inclusive_disjunction b1 b2)),
     159           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) :: r〉)
     160             b c 〈c, [ ]〉.
     161   
     162    (fun b1 b2 (c,r) -> b1 & b2 || c & (b1 || b2),xor (xor b1 b2) c::r) l r (c,[])
     163   
     164ndefinition half_add ≝
     165  λn: Nat.
     166  λb, c: BitVector n.
     167    full_add n b c false.
     168
  • Deliverables/D4.1/Matita/BitVector.ma

    r343 r349  
    217217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    218218    ].
    219    
    220 naxiom full_add:
    221   ∀n: Nat.
    222   ∀b, c: BitVector n.
    223   ∀d: Bit.
    224     Bool × (BitVector n).
    225    
    226 ndefinition half_add ≝
    227   λn: Nat.
    228   λb, c: BitVector n.
    229     full_add n b c false.
  • 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(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/Nat.ma

    r343 r349  
    190190interpretation "Nat exponential" 'exponential n m = (exponential n m).
    191191
    192 nlet rec decidable_equality (m: Nat) (n: Nat) on m: Bool ≝
     192nlet rec eq_n (m: Nat) (n: Nat) on m: Bool ≝
    193193  match m with
    194194    [ Z ⇒
     
    199199    | S o ⇒
    200200      match n with
    201         [ S p ⇒ decidable_equality o p
     201        [ S p ⇒ eq_n o p
    202202        | _ ⇒ false
    203203        ]
Note: See TracChangeset for help on using the changeset viewer.