Ignore:
Timestamp:
Dec 5, 2010, 11:54:59 PM (9 years ago)
Author:
sacerdot
Message:

1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons => VCons
3) DoTest? modified to pretty-print the execution trace.

This should make debugging easier.

File:
1 edited

Legend:

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

    r373 r374  
    1212
    1313ninductive Vector (A: Type[0]): Nat → Type[0] ≝
    14   Empty: Vector A Z
    15 | Cons: ∀n: Nat. A → Vector A n → Vector A (S n).
     14  VEmpty: Vector A Z
     15| VCons: ∀n: Nat. A → Vector A n → Vector A (S n).
    1616
    1717(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    2727  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
    2828
    29 interpretation "Vector vnil" 'vnil = (Empty ?).
    30 interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl).
     29interpretation "Vector vnil" 'vnil = (VEmpty ?).
     30interpretation "Vector vcons" 'vcons hd tl = (VCons ? ? hd tl).
    3131
    3232notation "hvbox(l break !!! break n)"
     
    4343    [ Z ⇒
    4444      match v return λx.λ_. Z < x → A with
    45         [ Empty ⇒ λabsd1: Z < Z. ?
    46         | Cons p hd tl ⇒ λprf1: Z < S p. hd
     45        [ VEmpty ⇒ λabsd1: Z < Z. ?
     46        | VCons p hd tl ⇒ λprf1: Z < S p. hd
    4747        ]
    4848    | S o ⇒
    4949      (match v return λx.λ_. S o < x → A with
    50         [ Empty ⇒ λprf: S o < Z. ?
    51         | Cons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
     50        [ VEmpty ⇒ λprf: S o < Z. ?
     51        | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
    5252        ])
    5353    ]) lt.
     
    7373    [ Z ⇒
    7474      match v with
    75         [ Empty ⇒ Nothing A
    76         | Cons p hd tl ⇒ Just A hd
     75        [ VEmpty ⇒ Nothing A
     76        | VCons p hd tl ⇒ Just A hd
    7777        ]
    7878    | S o ⇒
    7979      match v with
    80         [ Empty ⇒ Nothing A
    81         | Cons p hd tl ⇒ get_index_weak_v A p tl o
     80        [ VEmpty ⇒ Nothing A
     81        | VCons p hd tl ⇒ get_index_weak_v A p tl o
    8282        ]
    8383    ].
     
    8989    [ Z ⇒
    9090      match v return λx.λ_. Z < x → Vector A x with
    91         [ Empty ⇒ λabsd1: Z < Z. Empty A
    92         | Cons p hd tl ⇒ λprf1: Z < S p. (a ::: tl)
     91        [ VEmpty ⇒ λabsd1: Z < Z. [[ ]]
     92        | VCons p hd tl ⇒ λprf1: Z < S p. (a ::: tl)
    9393        ]
    9494    | S o ⇒
    9595      (match v return λx.λ_. S o < x → Vector A x with
    96         [ Empty ⇒ λprf: S o < Z. Empty A
    97         | Cons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
     96        [ VEmpty ⇒ λprf: S o < Z. [[ ]]
     97        | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
    9898        ])
    9999    ]) lt.
     
    107107    [ Z ⇒
    108108      match v with
    109         [ Empty ⇒ Nothing (Vector A n)
    110         | Cons o hd tl ⇒ Just (Vector A n) (? (Cons A o a tl))
     109        [ VEmpty ⇒ Nothing (Vector A n)
     110        | VCons o hd tl ⇒ Just (Vector A n) (? (VCons A o a tl))
    111111        ]
    112112    | S o ⇒
    113113      match v with
    114         [ Empty ⇒ Nothing (Vector A n)
    115         | Cons p hd tl ⇒
     114        [ VEmpty ⇒ Nothing (Vector A n)
     115        | VCons p hd tl ⇒
    116116            let settail ≝ set_index_weak A p tl o a in
    117117              match settail with
    118118                [ Nothing ⇒ Nothing (Vector A n)
    119                 | Just j ⇒ Just (Vector A n) (? (Cons A p hd j))
     119                | Just j ⇒ Just (Vector A n) (? (VCons A p hd j))
    120120                ]
    121121        ]
     
    130130    | S o ⇒
    131131      match v with
    132         [ Empty ⇒ Nothing (Vector A n)
    133         | Cons p hd tl ⇒ ? (drop A p tl o)
     132        [ VEmpty ⇒ Nothing (Vector A n)
     133        | VCons p hd tl ⇒ ? (drop A p tl o)
    134134        ]
    135135    ].
     
    144144  | S m' ⇒ λv.
    145145     match v return λl.λ_:Vector A l.l = S (m' + n) → (Vector A (S m')) × (Vector A n) with
    146       [ Empty ⇒ λK.⊥
    147       | Cons o he tl ⇒ λK.
    148          match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with
     146      [ VEmpty ⇒ λK.⊥
     147      | VCons o he tl ⇒ λK.
     148         match split A m' n (tl⌈Vector A o↦Vector A (m'+n)⌉) with
    149149          [ mk_Cartesian v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
    150150// [ ndestruct | nlapply (S_inj … K); //]
     
    154154≝ λA,n,v.
    155155 match v return λl.λ_:Vector A l.l = S n → A × (Vector A n) with
    156   [ Empty ⇒ λK.⊥
    157   | Cons o he tl ⇒ λK. 〈he,(tl⌈Vector A n ↦ Vector A o⌉)〉
     156  [ VEmpty ⇒ λK.⊥
     157  | VCons o he tl ⇒ λK. 〈he,(tl⌈Vector A o ↦ Vector A n⌉)〉
    158158  ] (? : S ? = S ?).
    159159// [ ndestruct | nlapply (S_inj … K); //]
     
    170170                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
    171171  match v with
    172     [ Empty ⇒ x
    173     | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
     172    [ VEmpty ⇒ x
     173    | VCons n hd tl ⇒ f hd (fold_right A B n f x tl)
    174174    ].
    175175
     
    178178                      (v: Vector A n) (q: Vector B n) on v : C n ≝
    179179  (match v return λx.λ_. x = n → C n with
    180     [ Empty ⇒
     180    [ VEmpty ⇒
    181181      match q return λx.λ_. Z = x → C x with
    182         [ Empty ⇒ λprf: Z = Z. c
    183         | Cons o hd tl ⇒ λabsd. ⊥
    184         ]
    185     | Cons o hd tl ⇒
     182        [ VEmpty ⇒ λprf: Z = Z. c
     183        | VCons o hd tl ⇒ λabsd. ⊥
     184        ]
     185    | VCons o hd tl ⇒
    186186      match q return λx.λ_. S o = x → C x with
    187         [ Empty ⇒ λabsd: S o = Z. ⊥
    188         | Cons p hd' tl' ⇒ λprf: S o = S p.
    189            (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B o ↦ Vector B p⌉)))⌈C (S p) ↦ C (S o)⌉
     187        [ VEmpty ⇒ λabsd: S o = Z. ⊥
     188        | VCons p hd' tl' ⇒ λprf: S o = S p.
     189           (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B p ↦ Vector B o⌉)))⌈C (S o) ↦ C (S p)⌉
    190190        ]
    191191    ]) (refl ? n).
     
    196196                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
    197197  match v with
    198     [ Empty ⇒ x
    199     | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
     198    [ VEmpty ⇒ x
     199    | VCons n hd tl ⇒ f (fold_left A B n f x tl) hd
    200200    ].
    201201   
     
    207207             (f: A → B) (v: Vector A n) on v ≝
    208208  match v with
    209     [ Empty ⇒ Empty B
    210     | Cons n hd tl ⇒ (f hd) ::: (map A B n f tl)
     209    [ VEmpty ⇒ [[ ]]
     210    | VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
    211211    ].
    212212
     
    214214             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
    215215  (match v return (λx.λr. x = n → Vector C x) with
    216     [ Empty ⇒ λ_. Empty C
    217     | Cons n hd tl ⇒
     216    [ VEmpty ⇒ λ_. [[ ]]
     217    | VCons n hd tl ⇒
    218218      match q return (λy.λr. S n = y → Vector C (S n)) with
    219         [ Empty ⇒ ?
    220         | Cons m hd' tl' ⇒
     219        [ VEmpty ⇒ ?
     220        | VCons m hd' tl' ⇒
    221221            λe: S n = S m.
    222222              (f hd hd') ::: (zip_with A B C n f tl ?)
     
    247247nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
    248248  match n return λn. Vector A n with
    249     [ Z ⇒ Empty A
     249    [ Z ⇒ [[ ]]
    250250    | S m ⇒ h ::: (replicate A m h)
    251251    ].
     
    254254                (v: Vector A n) (q: Vector A m) on v ≝
    255255  match v return (λn.λv. Vector A (n + m)) with
    256     [ Empty ⇒ q
    257     | Cons o hd tl ⇒ hd ::: (append A o m tl q)
     256    [ VEmpty ⇒ q
     257    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
    258258    ].
    259259   
     
    268268  a :::
    269269    (match v with
    270        [ Empty ⇒ Empty A
    271        | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl
     270       [ VEmpty ⇒ VEmpty A
     271       | VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
    272272       ]).
    273273
     
    275275                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
    276276  match v with
    277     [ Empty ⇒ ?
    278     | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
     277    [ VEmpty ⇒ ?
     278    | VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
    279279    ].
    280280    //.
     
    284284(* Other manipulations.                                                       *)
    285285(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    286    
    287 nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
    288   match v with
    289     [ Empty ⇒ Z
    290     | Cons n hd tl ⇒ S $ length A n tl
    291     ].
    292286
    293287nlet rec reverse (A: Type[0]) (n: Nat)
    294288                 (v: Vector A n) on v ≝
    295289  match v return (λm.λv. Vector A m) with
    296     [ Empty ⇒ Empty A
    297     | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
     290    [ VEmpty ⇒ [[ ]]
     291    | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]])
    298292    ].
    299293    nrewrite < (succ_plus ? ?).
     
    309303                        (v: Vector A n) on v ≝
    310304  match v return λn.λv. List A with
    311     [ Empty ⇒ ? (cic:/matita/ng/List/List.con(0,1,1) A)
    312     | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
    313     ].
    314     //.
    315 nqed.
     305    [ VEmpty ⇒ []
     306    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
     307    ].
    316308
    317309nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
    318310  match l return λl. Vector A (length A l) with
    319     [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A)
    320     | Cons hd tl ⇒ ? (hd ::: (vector_of_list A tl))
    321     ].
    322     nnormalize.
    323     //.
    324     //.
    325 nqed.
     311    [ Empty ⇒ [[ ]]
     312    | Cons hd tl ⇒ hd ::: (vector_of_list A tl)
     313    ].
    326314
    327315(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     
    335323    | S o ⇒
    336324        match v with
    337           [ Empty ⇒ Empty A
    338           | Cons p hd tl ⇒
    339              rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
     325          [ VEmpty ⇒ [[ ]]
     326          | VCons p hd tl ⇒
     327             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S Z) ↦ Vector A (S p)⌉)
    340328          ]
    341329    ].
    342     nrewrite < (succ_plus ? ?).
    343     nrewrite > (plus_zero ?).
    344     //.
     330 //.
    345331nqed.
    346332
     
    350336  λv: Vector A n.
    351337    reverse A n (rotate_left A n m (reverse A n v)).
    352    
     338
    353339ndefinition shift_left_1 ≝
    354340  λA: Type[0].
    355341  λn: Nat.
    356   λv: Vector A n.
     342  λv: Vector A (S n).
    357343  λa: A.
    358     match v with
    359       [ Empty ⇒ ?
    360       | Cons o hd tl ⇒ reverse A n (? (Cons A o a (reverse A o tl)))
    361       ].
    362       //.
     344   match v return λy.λ_. y = S n → Vector A y with
     345     [ VEmpty ⇒ λH.⊥
     346     | VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
     347     ] (refl ? (S n)).
     348 ndestruct.
    363349nqed.
    364350
     
    366352  λA: Type[0].
    367353  λn: Nat.
    368   λv: Vector A n.
     354  λv: Vector A (S n).
    369355  λa: A.
    370     reverse A n (shift_left_1 A n (reverse A n v) a).
     356    reverse … (shift_left_1 … (reverse … v) a).
    371357   
    372358ndefinition shift_left ≝
    373359  λA: Type[0].
    374360  λn, m: Nat.
    375   λv: Vector A n.
     361  λv: Vector A (S n).
    376362  λa: A.
    377     iterate (Vector A n) (λx. shift_left_1 A n x a) v m.
     363    iterate … (λx. shift_left_1 … x a) v m.
    378364   
    379365ndefinition shift_right ≝
    380366  λA: Type[0].
    381367  λn, m: Nat.
    382   λv: Vector A n.
     368  λv: Vector A (S n).
    383369  λa: A.
    384     iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
     370    iterate … (λx. shift_right_1 … x a) v m.
    385371
    386372(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    388374(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    389375
    390 nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b
     376nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b : Bool
    391377  (match b return λx.λ_. n = x → Bool with
    392     [ Empty ⇒
     378    [ VEmpty ⇒
    393379      match c return λx.λ_. x = Z → Bool with
    394         [ Empty ⇒ λ_. true
    395         | Cons p hd tl ⇒ λabsd.?
    396         ]
    397     | Cons o hd tl ⇒
     380        [ VEmpty ⇒ λ_. true
     381        | VCons p hd tl ⇒ λabsd.⊥
     382        ]
     383    | VCons o hd tl ⇒
    398384        match c return λx.λ_. x = S o → Bool with
    399           [ Empty ⇒ λabsd. ?
    400           | Cons p hd' tl' ⇒
     385          [ VEmpty ⇒ λabsd.⊥
     386          | VCons p hd' tl' ⇒
    401387            λprf.
    402388              if (f hd hd') then
    403                 (eq_v A o f tl ?)
     389                (eq_v A o f tl (tl'⌈Vector A p ↦ Vector A o⌉))
    404390              else
    405391                false
     
    407393    ]) (refl ? n).
    408394    ##[##1,2: ndestruct
    409       | nlapply (S_inj … prf); #X; nrewrite < X;
    410         napply tl' ]
     395      | nlapply (S_inj … prf); #X; nrewrite < X; @]
    411396nqed.
    412397
     
    452437  @.
    453438nqed.
    454 
    455 nlemma length_correct:
    456   ∀A: Type[0].
    457   ∀n: Nat.
    458   ∀v: Vector A n.
    459     length A n v = n.
    460   #A n v.
    461   nelim v.
    462   nnormalize.
    463   @.
    464   #N H V H2.
    465   nnormalize.
    466   nrewrite > H2.
    467   @.
    468 nqed.
    469 
    470 nlemma map_length:
    471   ∀A, B: Type[0].
    472   ∀n: Nat.
    473   ∀v: Vector A n.
    474   ∀f: A → B.
    475     length A n v = length B n (map A B n f v).
    476   #A B n v f.
    477   nelim v.
    478   nnormalize.
    479   @.
    480   #N H V H2.
    481   nnormalize.
    482   nrewrite > H2.
    483   @.
    484 nqed.
Note: See TracChangeset for help on using the changeset viewer.