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

Last change on this file since 352 was 352, checked in by mulligan, 9 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.