source: Deliverables/D4.1/Matita/BitVectorTrie.ma @ 557

Last change on this file since 557 was 465, checked in by mulligan, 9 years ago

Moved over to standard library.

File size: 2.7 KB
Line 
1include "BitVector.ma".
2
3include "basics/bool.ma".
4include "datatypes/sums.ma".
5
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)
12                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
13       : A ≝
14  (match b return λx.λ_. x = n → A with
15    [ VEmpty ⇒
16      (match t return λx.λ_. O = x → A with
17        [ Leaf l ⇒ λ_.l
18        | Node h l r ⇒ λK.⊥
19        | Stub s ⇒ λ_.a
20        ])
21    | VCons o hd tl ⇒
22      match t return λx.λ_. (S o) = x → A with
23        [ Leaf l ⇒ λK.⊥
24        | Node h l r ⇒
25           match hd with
26             [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a
27             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
28             ]
29        | Stub s ⇒ λ_. a]
30    ]) (refl ? n).
31 ##[##1,2: ndestruct |##*: napply injective_S; //]
32nqed.
33
34nlet rec prepare_trie_for_insertion (A: Type[0]) (n: nat)
35                                    (b: BitVector n) (a:A) on b
36       : BitVectorTrie A n ≝
37   match b with
38    [ VEmpty ⇒ Leaf A a
39    | VCons o hd tl ⇒
40      match hd with
41        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
42        | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
43        ]
44    ].
45
46nlet rec insert (A: Type[0]) (n: nat)
47                (b: BitVector n) (a: A) on b:
48                 BitVectorTrie A n → BitVectorTrie A n ≝
49  (match b with
50    [ VEmpty ⇒ λ_. Leaf A a
51    | VCons o hd tl ⇒ λt.
52          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
53            [ Leaf l ⇒ λprf.⊥
54            | Node p l r ⇒ λprf.
55               match hd with
56                [ true ⇒  Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉))
57                | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉)
58                ]
59            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a)
60            ] (refl ? (S o))
61    ]).
62    ##[ ndestruct;
63    ##|##*: napply injective_S; // ]
64nqed.
65
66(*
67nlemma insert_lookup_stub:
68  ∀A: Type[0].
69  ∀n: nat.
70  ∀b: BitVector n.
71  ∀t: BitVectorTrie A n.
72  ∀a, c: A.
73    (lookup A n b (insert A n b a (Stub A n)) a) = a.
74  #A n b t a c.
75  nelim b.
76  //.
77  #N H V H2.
78  nnormalize.
79  @.
80nqed.
81*)
82(*
83nlemma test:
84  ∀n: nat.
85  ∀b: BitVector n.
86    length n b = n.
87  #n b.
88  nelim b.
89  //.
90  #N H V IH.
91  ncases H.
92
93nlemma insert_lookup_leaf:
94  ∀A: Type[0].
95  ∀n: nat.
96  ∀b: BitVector n.
97  ∀a, c: A.
98  ∀t: BitVectorTrie A n.
99    lookup A ? b (insert A ? b a t) c = a.
100  #A n b a c t.
101  nelim b.
102  nnormalize.
103  @.
104  #N H V IH.
105*)
Note: See TracBrowser for help on using the repository browser.