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

Last change on this file since 357 was 357, checked in by sacerdot, 9 years ago
  • stupid bug fixed in BitVectorTrie?
  • dependencies minimized, dead code removed
File size: 2.7 KB
Line 
1include "BitVector.ma".
2include "Bool.ma".
3include "Maybe.ma".
4
5ninductive 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.
9
10nlet rec lookup (A: Type[0]) (n: Nat)
11                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
12       : A ≝
13  (match b return λx.λ_. x = n → A with
14    [ Empty ⇒
15      (match t return λx.λ_. Z = x → A with
16        [ Leaf l ⇒ λ_.l
17        | Node h l r ⇒ λK.⊥
18        | Stub s ⇒ λ_.a
19        ])
20    | Cons o hd tl ⇒
21      match t return λx.λ_. (S o) = x → A with
22        [ Leaf l ⇒ λK.⊥
23        | Node h l r ⇒
24           match hd with
25             [ true ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
26             | false ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
27             ]
28        | Stub s ⇒ λ_. a
29        ]
30    ]) (refl ? n).
31 ##[##1,2: ndestruct |##*: napply S_inj; //]
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    [ Empty ⇒ Leaf A a
39    | Cons 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    [ Empty ⇒ λ_. Leaf A a
51    | Cons 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⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉))
57                | false ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉)
58                ]
59            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (Cons ? o hd tl) a)
60            ] (refl ? (S o))
61    ]).
62    ##[ ndestruct;
63    ##|##*: napply S_inj; // ]
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.