Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (9 years ago)
Author:
mulligan
Message:

Moved over to standard library.

File:
1 edited

Legend:

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

    r374 r465  
    44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    55
    6 include "Nat.ma".
    7 include "List.ma".
     6include "datatypes/list.ma".
     7include "basics/bool.ma".
     8include "datatypes/sums.ma".
     9
     10include "Util.ma".
     11
     12include "arithmetics/nat.ma".
     13
    814
    915(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    1117(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    1218
    13 ninductive Vector (A: Type[0]): Nat → Type[0] ≝
    14   VEmpty: Vector A Z
    15 | VCons: ∀n: Nat. A → Vector A n → Vector A (S n).
     19ninductive Vector (A: Type[0]): nat → Type[0] ≝
     20  VEmpty: Vector A O
     21| VCons: ∀n: nat. A → Vector A n → Vector A (S n).
    1622
    1723(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    3844(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3945
    40 nlet rec get_index_v (A: Type[0]) (n: Nat)
    41                    (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝
     46nlet rec get_index_v (A: Type[0]) (n: nat)
     47                   (v: Vector A n) (m: nat) (lt: m < n) on m: A ≝
    4248  (match m with
    43     [ Z
    44       match v return λx.λ_. Z < x → A with
    45         [ VEmpty ⇒ λabsd1: Z < Z. ?
    46         | VCons p hd tl ⇒ λprf1: Z < S p. hd
     49    [ O
     50      match v return λx.λ_. O < x → A with
     51        [ VEmpty ⇒ λabsd1: O < O. ?
     52        | VCons p hd tl ⇒ λprf1: O < S p. hd
    4753        ]
    4854    | S o ⇒
    4955      (match v return λx.λ_. S o < x → A with
    50         [ VEmpty ⇒ λprf: S o < Z. ?
     56        [ VEmpty ⇒ λprf: S o < O. ?
    5157        | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
    5258        ])
    5359    ]) lt.
    54     ##[ ncases (nothing_less_than_Z Z); #K; ncases (K absd1)
    55     ##| ncases (nothing_less_than_Z (S o)); #K; ncases (K prf)
    56     ##| napply succ_less_than_injective; nassumption
     60    ##[ ncases (not_le_Sn_O O); nnormalize in absd1; #H; ncases (H absd1);
     61    ##| ncases (not_le_Sn_O (S o)); nnormalize in prf; #H; ncases (H prf);
     62    ##| nnormalize; nnormalize in prf; napply le_S_S_to_le; nassumption;
    5763    ##]
    5864nqed.
     
    6066ndefinition get_index' ≝
    6167  λA: Type[0].
    62   λn, m: Nat.
     68  λn, m: nat.
    6369  λb: Vector A (S (n + m)).
    6470    get_index_v A (S (n + m)) b n ?.
    6571  nnormalize;
    66   napply less_than_or_equal_monotone;
    67   napply less_than_or_equal_plus;
    68 nqed.
    69 
    70 nlet rec get_index_weak_v (A: Type[0]) (n: Nat)
    71                           (v: Vector A n) (m: Nat) on m ≝
     72  //;
     73nqed.
     74
     75nlet rec get_index_weak_v (A: Type[0]) (n: nat)
     76                          (v: Vector A n) (m: nat) on m ≝
    7277  match m with
    73     [ Z
     78    [ O
    7479      match v with
    75         [ VEmpty ⇒ Nothing A
    76         | VCons p hd tl ⇒ Just A hd
     80        [ VEmpty ⇒ None A
     81        | VCons p hd tl ⇒ Some A hd
    7782        ]
    7883    | S o ⇒
    7984      match v with
    80         [ VEmpty ⇒ Nothing A
     85        [ VEmpty ⇒ None A
    8186        | VCons p hd tl ⇒ get_index_weak_v A p tl o
    8287        ]
     
    8590interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
    8691
    87 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
     92nlet rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝
    8893  (match m with
    89     [ Z
    90       match v return λx.λ_. Z < x → Vector A x with
    91         [ VEmpty ⇒ λabsd1: Z < Z. [[ ]]
    92         | VCons p hd tl ⇒ λprf1: Z < S p. (a ::: tl)
     94    [ O
     95      match v return λx.λ_. O < x → Vector A x with
     96        [ VEmpty ⇒ λabsd1: O < O. [[ ]]
     97        | VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl)
    9398        ]
    9499    | S o ⇒
    95100      (match v return λx.λ_. S o < x → Vector A x with
    96         [ VEmpty ⇒ λprf: S o < Z. [[ ]]
     101        [ VEmpty ⇒ λprf: S o < O. [[ ]]
    97102        | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
    98103        ])
    99104    ]) lt.
    100     napply succ_less_than_injective.
    101     nassumption.
    102 nqed.
    103    
    104 nlet rec set_index_weak (A: Type[0]) (n: Nat)
    105                         (v: Vector A n) (m: Nat) (a: A) on m ≝
     105    nnormalize in prf ⊢ %;
     106    /2/;
     107nqed.
     108   
     109nlet rec set_index_weak (A: Type[0]) (n: nat)
     110                        (v: Vector A n) (m: nat) (a: A) on m ≝
    106111  match m with
    107     [ Z
     112    [ O
    108113      match v with
    109         [ VEmpty ⇒ Nothing (Vector A n)
    110         | VCons o hd tl ⇒ Just (Vector A n) (? (VCons A o a tl))
     114        [ VEmpty ⇒ None (Vector A n)
     115        | VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl))
    111116        ]
    112117    | S o ⇒
    113118      match v with
    114         [ VEmpty ⇒ Nothing (Vector A n)
     119        [ VEmpty ⇒ None (Vector A n)
    115120        | VCons p hd tl ⇒
    116121            let settail ≝ set_index_weak A p tl o a in
    117122              match settail with
    118                 [ Nothing ⇒ Nothing (Vector A n)
    119                 | Just j ⇒ Just (Vector A n) (? (VCons A p hd j))
     123                [ None ⇒ None (Vector A n)
     124                | Some j ⇒ Some (Vector A n) (? (VCons A p hd j))
    120125                ]
    121126        ]
     
    124129nqed.
    125130
    126 nlet rec drop (A: Type[0]) (n: Nat)
    127               (v: Vector A n) (m: Nat) on m ≝
     131nlet rec drop (A: Type[0]) (n: nat)
     132              (v: Vector A n) (m: nat) on m ≝
    128133  match m with
    129     [ Z ⇒ Just (Vector A n) v
     134    [ O ⇒ Some (Vector A n) v
    130135    | S o ⇒
    131136      match v with
    132         [ VEmpty ⇒ Nothing (Vector A n)
     137        [ VEmpty ⇒ None (Vector A n)
    133138        | VCons p hd tl ⇒ ? (drop A p tl o)
    134139        ]
     
    137142nqed.
    138143
    139 nlet rec split (A: Type[0]) (m,n: Nat) on m
    140              : Vector A (m+n) → (Vector A m) × (Vector A n)
     144nlet rec split (A: Type[0]) (m,n: nat) on m
     145             : Vector A (plus m n) → (Vector A m) × (Vector A n)
    141146
    142  match m return λm. Vector A (m+n) → (Vector A m) × (Vector A n) with
    143   [ Z ⇒ λv.〈[[ ]], v〉
     147 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
     148  [ O ⇒ λv.〈[[ ]], v〉
    144149  | S m' ⇒ λv.
    145      match v return λl.λ_:Vector A l.l = S (m' + n) → (Vector A (S m')) × (Vector A n) with
     150     match v return λl.λ_:Vector A l.l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with
    146151      [ VEmpty ⇒ λK.⊥
    147152      | VCons o he tl ⇒ λK.
    148153         match split A m' n (tl⌈Vector A o↦Vector A (m'+n)⌉) with
    149           [ mk_Cartesian v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
    150 // [ ndestruct | nlapply (S_inj … K); //]
     154          [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
     155// [ ndestruct | nlapply (injective_S … K); //]
    151156nqed.
    152157
     
    157162  | VCons o he tl ⇒ λK. 〈he,(tl⌈Vector A o ↦ Vector A n⌉)〉
    158163  ] (? : S ? = S ?).
    159 // [ ndestruct | nlapply (S_inj … K); //]
    160 nqed.
    161 
    162 ndefinition from_singl: ∀A:Type[0]. Vector A (S Z) → A ≝
    163  λA,v. first … (head … v).
     164// [ ndestruct | nlapply (injective_S … K); //]
     165nqed.
     166
     167ndefinition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝
     168 λA,v. fst … (head … v).
    164169   
    165170(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    167172(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    168173   
    169 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
     174nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
    170175                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
    171176  match v with
     
    174179    ].
    175180
    176 nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: Nat → Type[0])
    177                       (f: ∀N. A → B → C N → C (S N)) (c: C Z) (n: Nat)
     181nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
     182                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
    178183                      (v: Vector A n) (q: Vector B n) on v : C n ≝
    179184  (match v return λx.λ_. x = n → C n with
    180185    [ VEmpty ⇒
    181       match q return λx.λ_. Z = x → C x with
    182         [ VEmpty ⇒ λprf: Z = Z. c
     186      match q return λx.λ_. O = x → C x with
     187        [ VEmpty ⇒ λprf: O = O. c
    183188        | VCons o hd tl ⇒ λabsd. ⊥
    184189        ]
    185190    | VCons o hd tl ⇒
    186191      match q return λx.λ_. S o = x → C x with
    187         [ VEmpty ⇒ λabsd: S o = Z. ⊥
     192        [ VEmpty ⇒ λabsd: S o = O. ⊥
    188193        | VCons p hd' tl' ⇒ λprf: S o = S p.
    189194           (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)⌉
    190195        ]
    191196    ]) (refl ? n).
    192 ##[##1,2: ndestruct | ##3,4: nlapply (S_inj … prf); // ]
     197##[##1,2: ndestruct | ##3,4: nlapply (injective_S … prf); // ]
    193198nqed.
    194199 
    195 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
     200nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
    196201                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
    197202  match v with
     
    204209(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    205210
    206 nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
     211nlet rec map (A: Type[0]) (B: Type[0]) (n: nat)
    207212             (f: A → B) (v: Vector A n) on v ≝
    208213  match v with
     
    211216    ].
    212217
    213 nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
     218nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
    214219             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
    215220  (match v return (λx.λr. x = n → Vector C x) with
     
    228233          ndestruct(e);
    229234          ##
    230         | nlapply (S_inj … e); #H; nrewrite > H;
     235        | nlapply (injective_S … e); #H; nrewrite > H;
    231236          napply tl'
    232237          ##
     
    236241ndefinition zip ≝
    237242  λA, B: Type[0].
    238   λn: Nat.
     243  λn: nat.
    239244  λv: Vector A n.
    240245  λq: Vector B n.
    241     zip_with A B (Cartesian A B) n (mk_Cartesian A B) v q.
     246    zip_with A B (A × B) n (mk_pair A B) v q.
    242247
    243248(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    245250(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    246251
    247 nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
     252nlet rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
    248253  match n return λn. Vector A n with
    249     [ Z ⇒ [[ ]]
     254    [ O ⇒ [[ ]]
    250255    | S m ⇒ h ::: (replicate A m h)
    251256    ].
    252257
    253 nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
     258(* DPM: fixme.  Weird matita bug in base case. *)
     259nlet rec append (A: Type[0]) (n: nat) (m: nat)
    254260                (v: Vector A n) (q: Vector A m) on v ≝
    255261  match v return (λn.λv. Vector A (n + m)) with
    256     [ VEmpty ⇒ q
     262    [ VEmpty ⇒ (? q)
    257263    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
    258264    ].
     265    #H; nassumption;
     266nqed.
    259267   
    260268notation "hvbox(l break @@ r)"
     
    264272interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
    265273   
    266 nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
     274nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
    267275                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
    268276  a :::
     
    272280       ]).
    273281
    274 nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)
     282nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
    275283                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
    276284  match v with
     
    285293(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    286294
    287 nlet rec reverse (A: Type[0]) (n: Nat)
     295nlet rec reverse (A: Type[0]) (n: nat)
    288296                 (v: Vector A n) on v ≝
    289297  match v return (λm.λv. Vector A m) with
     
    291299    | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]])
    292300    ].
    293     nrewrite < (succ_plus ? ?).
    294     nrewrite > (plus_zero ?).
    295     //.
     301    //;
    296302nqed.
    297303
     
    300306(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    301307
    302 nlet rec list_of_vector (A: Type[0]) (n: Nat)
     308nlet rec list_of_vector (A: Type[0]) (n: nat)
    303309                        (v: Vector A n) on v ≝
    304   match v return λn.λv. List A with
     310  match v return λn.λv. list A with
    305311    [ VEmpty ⇒ []
    306312    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
    307313    ].
    308314
    309 nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
     315nlet rec vector_of_list (A: Type[0]) (l: list A) on l ≝
    310316  match l return λl. Vector A (length A l) with
    311     [ Empty ⇒ [[ ]]
    312     | Cons hd tl ⇒ hd ::: (vector_of_list A tl)
     317    [ nil ⇒ [[ ]]
     318    | cons hd tl ⇒ hd ::: (vector_of_list A tl)
    313319    ].
    314320
     
    317323(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    318324   
    319 nlet rec rotate_left (A: Type[0]) (n: Nat)
    320                      (m: Nat) (v: Vector A n) on m: Vector A n ≝
     325nlet rec rotate_left (A: Type[0]) (n: nat)
     326                     (m: nat) (v: Vector A n) on m: Vector A n ≝
    321327  match m with
    322     [ Z ⇒ v
     328    [ O ⇒ v
    323329    | S o ⇒
    324330        match v with
    325331          [ VEmpty ⇒ [[ ]]
    326332          | 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)⌉)
     333             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
    328334          ]
    329335    ].
     
    333339ndefinition rotate_right ≝
    334340  λA: Type[0].
    335   λn, m: Nat.
     341  λn, m: nat.
    336342  λv: Vector A n.
    337343    reverse A n (rotate_left A n m (reverse A n v)).
     
    339345ndefinition shift_left_1 ≝
    340346  λA: Type[0].
    341   λn: Nat.
     347  λn: nat.
    342348  λv: Vector A (S n).
    343349  λa: A.
     
    351357ndefinition shift_right_1 ≝
    352358  λA: Type[0].
    353   λn: Nat.
     359  λn: nat.
    354360  λv: Vector A (S n).
    355361  λa: A.
     
    358364ndefinition shift_left ≝
    359365  λA: Type[0].
    360   λn, m: Nat.
     366  λn, m: nat.
    361367  λv: Vector A (S n).
    362368  λa: A.
     
    365371ndefinition shift_right ≝
    366372  λA: Type[0].
    367   λn, m: Nat.
     373  λn, m: nat.
    368374  λv: Vector A (S n).
    369375  λa: A.
     
    374380(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    375381
    376 nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b : Bool ≝
    377   (match b return λx.λ_. n = x → Bool with
     382nlet rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
     383  (match b return λx.λ_. n = x → bool with
    378384    [ VEmpty ⇒
    379       match c return λx.λ_. x = Z → Bool with
     385      match c return λx.λ_. x = O → bool with
    380386        [ VEmpty ⇒ λ_. true
    381387        | VCons p hd tl ⇒ λabsd.⊥
    382388        ]
    383389    | VCons o hd tl ⇒
    384         match c return λx.λ_. x = S o → Bool with
     390        match c return λx.λ_. x = S o → bool with
    385391          [ VEmpty ⇒ λabsd.⊥
    386392          | VCons p hd' tl' ⇒
     
    393399    ]) (refl ? n).
    394400    ##[##1,2: ndestruct
    395       | nlapply (S_inj … prf); #X; nrewrite < X; @]
     401      | nlapply (injective_S … prf); #X; nrewrite < X; @]
    396402nqed.
    397403
     
    402408ndefinition mem ≝
    403409 λA: Type[0].
    404  λeq_a : A → A → Bool.
    405  λn: Nat.
     410 λeq_a : A → A → bool.
     411 λn: nat.
    406412 λl: Vector A n.
    407413 λx: A.
    408   fold_right … (λy,v. inclusive_disjunction (eq_a x y) v) false l.
     414  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
    409415
    410416ndefinition subvector_with ≝
    411417  λA: Type[0].
    412   λn: Nat.
    413   λm: Nat.
    414   λf: A → A → Bool.
     418  λn: nat.
     419  λm: nat.
     420  λf: A → A → bool.
    415421  λv: Vector A n.
    416422  λq: Vector A m.
    417     fold_right ? ? ? (λx, v. conjunction (mem ? f ? q x) v) true v.
     423    fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v.
    418424   
    419425(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    423429nlemma map_fusion:
    424430  ∀A, B, C: Type[0].
    425   ∀n: Nat.
     431  ∀n: nat.
    426432  ∀v: Vector A n.
    427433  ∀f: A → B.
Note: See TracChangeset for help on using the changeset viewer.