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

Last change on this file since 352 was 352, checked in by mulligan, 10 years ago

Do not use ndestruct for injectivity since it introduces StreickerK that
blocks reductions.

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