source: src/common/BitVectorTrieMap.ma @ 2755

Last change on this file since 2755 was 2604, checked in by piccolo, 7 years ago

ERTLtoERTLptr in place.

File size: 2.4 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "ASM/BitVectorTrie.ma".
16
17let rec map (A : Type[0]) (B : Type[0]) (f : A → B) (n : nat)
18(t : BitVectorTrie A n) on t : BitVectorTrie B n ≝
19match t with
20[Leaf a ⇒ Leaf ? (f a)
21|Node n1 t1 t2 ⇒ Node … n1 (map A B f n1 t1) (map A B f n1 t2)
22|Stub n1 ⇒ Stub … n1
23].
24
25lemma map_ext : ∀A,B : Type[0]. ∀n : nat. ∀t: BitVectorTrie A n.
26∀f,g : A→B. (∀a.f a =g a) → map A B f n t = map A B g n t.
27#A #B #n #t elim t
28[#x #f #g #H normalize >(H x) %
29|#n1 #l #r #Hl #Hr #f #g #H normalize >(Hl f g H) >(Hr f g H) %
30|#n1 #f #g #H %
31]
32qed.
33
34
35lemma insert_map: ∀ A,B : Type[0].∀ n: nat.∀t : BitVectorTrie A n.
36∀f : A → B.∀a,b.
37map A B f n (insert A n b a t) = insert B n b (f a) (map A B f n t).
38#A #B #n #t elim t -n
39[  #x #f #a #b >(BitVector_O b) -b %
40| #n #l #r #IHl #IHr #f #a #b
41  cases (BitVector_Sn … b) * * #tl #EQ >EQ -b normalize
42  [ >IHr | >IHl ] %
43| #n #f #a * -n [ % ]
44  #n #hd #tl change with (map ???? (prepare_trie_for_insertion ????) = prepare_trie_for_insertion ????)
45  elim (hd:::tl) [%] #n' * #tl' #Htl' normalize @eq_f2 try @Htl' %
46]
47qed.
48
49lemma lookup_map :  ∀ A,B : Type[0].∀ n: nat.∀t : BitVectorTrie A n.
50∀f : A → B.∀a,b. lookup B n b (map A B f n t) (f a) = f (lookup A n b t a).
51#A #B #n #t elim t
52[ #a #f #a1 #b >(BitVector_O b) %
53| #n1 #l #r #Hl #Hr #f #a #b cases (BitVector_Sn … b) * * #tl #EQ >EQ
54  normalize [@Hr|@Hl]
55| #n1 #f #a * [%] #n2 #hd #tl %
56]
57qed.
Note: See TracBrowser for help on using the repository browser.