Ignore:
Timestamp:
Nov 23, 2010, 3:50:28 PM (9 years ago)
Author:
mulligan
Message:

Strengthened typings of get_ and set_index in Vector file.

File:
1 edited

Legend:

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

    r260 r261  
    3737(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3838
     39naxiom succ_less_than_injective:
     40  ∀m, n: Nat.
     41    S m < S n → m < n.
     42   
     43naxiom nothing_less_than_Z:
     44  ∀m: Nat.
     45    ¬(m < Z).
     46
    3947nlet rec get_index (A: Type[0]) (n: Nat)
     48                   (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝
     49  (match m with
     50    [ Z ⇒
     51      match v return λx.λ_. Z < x → A with
     52        [ Empty ⇒ λabsd1: Z < Z. ?
     53        | Cons p hd tl ⇒ λprf1: Z < S p. hd
     54        ]
     55    | S o ⇒
     56      (match v return λx.λ_. S o < x → A with
     57        [ Empty ⇒ λprf: S o < Z. ?
     58        | Cons p hd tl ⇒ λprf: S o < S p. get_index A p tl o ?
     59        ])
     60    ]) lt.
     61    ##[ ncases (nothing_less_than_Z Z); #K; ncases (K absd1)
     62    ##| ncases (nothing_less_than_Z (S o)); #K; ncases (K prf)
     63    ##| napply succ_less_than_injective; nassumption
     64    ##]
     65nqed.
     66
     67nlet rec get_index_weak (A: Type[0]) (n: Nat)
    4068                   (v: Vector A n) (m: Nat) on m ≝
    4169  match m with
     
    4876      match v with
    4977        [ Empty ⇒ Nothing A
    50         | Cons p hd tl ⇒ get_index A p tl o
     78        | Cons p hd tl ⇒ get_index_weak A p tl o
    5179        ]
    5280    ].
     
    5482interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
    5583   
    56 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) on m
    57   match m return (λx. x < n → A) with
     84nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n
     85  (match m with
    5886    [ Z ⇒
    59       match v with
    60         [ Empty ⇒ λ_.?
    61         | Cons p hd tl ⇒ λ_.hd
    62         ]
    63     | S o ⇒
    64       match v with
    65         [ Empty ⇒ λ_.?
    66         | Cons p hd tl ⇒ λprf: m < p. set_index A p tl o a
    67         ]
    68     ].
     87      match v return λx.λ_. Z < x → Vector A x with
     88        [ Empty ⇒ λabsd1: Z < Z. Empty A
     89        | Cons p hd tl ⇒ λprf1: Z < S p. (a :: tl)
     90        ]
     91    | S o ⇒
     92      (match v return λx.λ_. S o < x → Vector A x with
     93        [ Empty ⇒ λprf: S o < Z. Empty A
     94        | Cons p hd tl ⇒ λprf: S o < S p. hd :: (set_index A p tl o a ?)
     95        ])
     96    ]) lt.
     97    napply succ_less_than_injective.
     98    nassumption.
     99nqed.
    69100   
    70101nlet rec set_index_weak (A: Type[0]) (n: Nat)
Note: See TracChangeset for help on using the changeset viewer.