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

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

Fixed strange bug/typo in BitVectorTrie?.ma

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