source: src/utilities/BitVectorTrieSet.ma @ 746

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

Changes to bitvectortrieset: equality on sets. Added new file for translation of variable set functor. other small changes.

File size: 2.4 KB
Line 
1include "ASM/BitVectorTrie.ma".
2include "ASM/Util.ma".
3
4definition BitVectorTrieSet ≝ BitVectorTrie unit.
5
6let rec set_member (n: nat) (p: Vector bool n) (b: BitVectorTrieSet n) on p: bool ≝
7  (match p return λx. λ_. n = x → bool with
8  [ VEmpty ⇒
9   ( match b return λx. λ_. x = 0 → bool with
10    [ Leaf _ ⇒ λprf. true
11    | Stub _ ⇒ λprf. false
12    | _ ⇒ λabsd. ?
13    ])
14  | VCons o hd tl ⇒
15    (match b return λx. λ_. x = S o → bool with
16    [ Leaf _ ⇒ λabsd. ?
17    | Stub _ ⇒ λprf. false
18    | Node p l r ⇒
19      match hd with
20      [ true ⇒ λprf: S p = S o. set_member o tl (r⌈p ↦ o⌉)
21      | false ⇒ λprf: S p = S o. set_member o tl (l⌈p ↦ o⌉)
22      ]
23    ])
24  ]) (refl ? n).
25  [3,4:
26     @ injective_S
27       assumption
28  |1,2:
29       destruct
30  ]
31qed.
32
33let rec set_union (n: nat) (b: BitVectorTrieSet n) on b: BitVectorTrieSet n → BitVectorTrieSet n ≝
34  match b return λx. λ_. BitVectorTrieSet x → BitVectorTrieSet x with
35  [ Stub _ ⇒ λc. c
36  | Leaf l ⇒ λc. Leaf ? l
37  | Node p l r ⇒
38    λc.
39    (match c return λx. λ_. x = (S p) → BitVectorTrieSet (S p) with
40    [ Node p' l' r' ⇒ λprf. Node ? ? (set_union ? l (l'⌈p' ↦ p⌉)) (set_union ? r (r'⌈p' ↦ p⌉))
41    | Stub _ ⇒ λprf. Node ? p l r
42    | Leaf _ ⇒ λabsd. ?
43    ] (refl ? (S p)))
44  ].
45  [1:
46      destruct(absd)
47  |2,3:
48      @ injective_S
49        assumption
50  ]
51qed.
52
53let rec set_eq (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: bool ≝
54  match b return λh. λ_. n = h → bool with
55  [ Stub s ⇒
56    match c with
57    [ Stub s' ⇒ λ_. eq_nat s s'
58    | _ ⇒ λ_. false
59    ]
60  | Leaf l ⇒
61    match c with
62    [ Leaf l' ⇒ λ_. true (* dpm: l and l' both unit *)
63    | _ ⇒ λ_. false
64    ]
65  | Node h l r ⇒
66    match c with
67    [ Node h' l' r' ⇒ λprf. andb (set_eq h l ?) (set_eq h r ?)
68    | _ ⇒ λ_. false
69    ]
70  ] (refl ? n).
71  [ 1: @ r
72  | 2: lapply (injective_S … prf)
73       # H
74       < H
75       @ r'
76  ]
77qed.
78
79(*
80let rec set_diff (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: BitVectorTrieSet n ≝
81  match b with
82  [ Stub ⇒
83*)
84
85definition set_insert ≝
86  λn: nat.
87  λb: BitVector n.
88  λs: BitVectorTrieSet n.
89    insert unit n b it s.
90
91definition set_empty ≝ λn. Stub unit n.
92
93definition set_singleton ≝
94  λn: nat.
95  λb: BitVector n.
96    insert unit n b it (set_empty ?).
Note: See TracBrowser for help on using the repository browser.