Changeset 261


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.

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

Legend:

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

    r260 r261  
    207207nqed.
    208208
     209naxiom less_than_or_equal_injective:
     210  ∀m, n: Nat.
     211    S m ≤ S n → m ≤ n.
     212
    209213(*
    210 nlemma less_than_or_equal_injective:
    211   ∀m, n: Nat.
    212     S m ≤ S n → m ≤ n.
    213   #m n.
    214   nelim m.
    215   #H.
    216   napplyS less_than_or_equal_zero.
    217   #N H H2.
    218   ndestruct.
    219 
    220214nlemma less_than_or_equal_zero_equal_zero:
    221215  ∀m: Nat.
     
    249243  napplyS less_than_or_equal_zero.
    250244  #N H H2.
    251   //.
    252   napplyS H.
    253 
     245  nrewrite > H.
     246  nnormalize.
    254247
    255248nlemma less_than_or_equal_transitive:
     
    262255  #N H H2.
    263256  nnormalize.
    264   #;
    265257*)
    266258
  • 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)
  • Deliverables/D4.1/Matita/depends

    r260 r261  
     1Exponential.ma Connectives.ma Equality.ma Nat.ma
    12Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    2 Exponential.ma Connectives.ma Equality.ma Nat.ma
    33BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    44Cartesian.ma Universes.ma
     5Universes.ma
    56Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    67Either.ma Bool.ma Maybe.ma Universes.ma
    7 Universes.ma
    88ASM.ma BitVector.ma BitVectorTrie.ma Either.ma Plogic/equality.ma Universes.ma
     9Char.ma Universes.ma
    910Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
    10 Char.ma Universes.ma
    1111Connectives.ma Plogic/equality.ma
    1212Bool.ma Universes.ma
     
    1414Util.ma Nat.ma
    1515Interpret.ma Arithmetic.ma BitVectorTrie.ma
     16String.ma Char.ma List.ma
    1617BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    1718Compare.ma Universes.ma
    18 String.ma Char.ma List.ma
    1919Plogic/equality.ma Universes.ma
    2020Nat.ma Bool.ma Cartesian.ma Connectives.ma
Note: See TracChangeset for help on using the changeset viewer.