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/BitVectorTrie.ma

    r464 r465  
    11include "BitVector.ma".
    2 include "Bool.ma".
    3 include "Maybe.ma".
    42
    5 ninductive BitVectorTrie (A: Type[0]): Nat → Type[0] ≝
    6   Leaf: A → BitVectorTrie A Z
    7 | Node: ∀n: Nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
    8 | Stub: ∀n: Nat. BitVectorTrie A n.
     3include "basics/bool.ma".
     4include "datatypes/sums.ma".
    95
    10 nlet rec lookup (A: Type[0]) (n: Nat)
     6ninductive BitVectorTrie (A: Type[0]): nat → Type[0] ≝
     7  Leaf: A → BitVectorTrie A O
     8| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
     9| Stub: ∀n: nat. BitVectorTrie A n.
     10
     11nlet rec lookup (A: Type[0]) (n: nat)
    1112                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
    1213       : A ≝
    1314  (match b return λx.λ_. x = n → A with
    1415    [ VEmpty ⇒
    15       (match t return λx.λ_. Z = x → A with
     16      (match t return λx.λ_. O = x → A with
    1617        [ Leaf l ⇒ λ_.l
    1718        | Node h l r ⇒ λK.⊥
     
    2829        | Stub s ⇒ λ_. a]
    2930    ]) (refl ? n).
    30  ##[##1,2: ndestruct |##*: napply S_inj; //]
     31 ##[##1,2: ndestruct |##*: napply injective_S; //]
    3132nqed.
    3233
    33 nlet rec prepare_trie_for_insertion (A: Type[0]) (n: Nat)
     34nlet rec prepare_trie_for_insertion (A: Type[0]) (n: nat)
    3435                                    (b: BitVector n) (a:A) on b
    3536       : BitVectorTrie A n ≝
     
    4344    ].
    4445
    45 nlet rec insert (A: Type[0]) (n: Nat)
     46nlet rec insert (A: Type[0]) (n: nat)
    4647                (b: BitVector n) (a: A) on b:
    4748                 BitVectorTrie A n → BitVectorTrie A n ≝
     
    6061    ]).
    6162    ##[ ndestruct;
    62     ##|##*: napply S_inj; // ]
     63    ##|##*: napply injective_S; // ]
    6364nqed.
    6465
     
    6667nlemma insert_lookup_stub:
    6768  ∀A: Type[0].
    68   ∀n: Nat.
     69  ∀n: nat.
    6970  ∀b: BitVector n.
    7071  ∀t: BitVectorTrie A n.
     
    8182(*
    8283nlemma test:
    83   ∀n: Nat.
     84  ∀n: nat.
    8485  ∀b: BitVector n.
    8586    length n b = n.
     
    9293nlemma insert_lookup_leaf:
    9394  ∀A: Type[0].
    94   ∀n: Nat.
     95  ∀n: nat.
    9596  ∀b: BitVector n.
    9697  ∀a, c: A.
Note: See TracChangeset for help on using the changeset viewer.