source: Deliverables/D4.2-4.3/utilities/BitVectorTrieSet.ma @ 491

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

Initial commit of (part)-formalisation of LIN intermediate language.

File size: 1.5 KB
Line 
1include "cerco/BitVectorTrie.ma".
2
3definition BitVectorTrieSet ≝ BitVectorTrie unit.
4
5let rec set_member (n: nat) (p: Vector bool n) (b: BitVectorTrieSet n) on p: bool ≝
6  (match p return λx. λ_. n = x → bool with
7  [ VEmpty ⇒
8   ( match b return λx. λ_. x = 0 → bool with
9    [ Leaf _ ⇒ λprf. true
10    | Stub _ ⇒ λprf. false
11    | _ ⇒ λabsd. ?
12    ])
13  | VCons o hd tl ⇒
14    (match b return λx. λ_. x = S o → bool with
15    [ Leaf _ ⇒ λabsd. ?
16    | Stub _ ⇒ λprf. false
17    | Node p l r ⇒
18      match hd with
19      [ true ⇒ λprf: S p = S o. set_member o tl (r⌈p ↦ o⌉)
20      | false ⇒ λprf: S p = S o. set_member o tl (l⌈p ↦ o⌉)
21      ]
22    ])
23  ]) (refl ? n).
24  [3,4:
25     @ injective_S
26       assumption
27  |1,2:
28       destruct
29  ]
30qed.
31
32let rec set_union (n: nat) (b: BitVectorTrieSet n) on b: BitVectorTrieSet n → BitVectorTrieSet n ≝
33  match b return λx. λ_. BitVectorTrieSet x → BitVectorTrieSet x with
34  [ Stub _ ⇒ λc. c
35  | Leaf l ⇒ λc. Leaf ? l
36  | Node p l r ⇒
37    λc.
38    (match c return λx. λ_. x = (S p) → BitVectorTrieSet (S p) with
39    [ Node p' l' r' ⇒ λprf. Node ? ? (set_union ? l (l'⌈p' ↦ p⌉)) (set_union ? r (r'⌈p' ↦ p⌉))
40    | Stub _ ⇒ λprf. Node ? p l r
41    | Leaf _ ⇒ λabsd. ?
42    ] (refl ? (S p)))
43  ].
44  [1:
45      destruct(absd)
46  |2,3:
47      @ injective_S
48        assumption
49  ]
50qed.
51
52definition set_insert ≝
53  λn: nat.
54  λb: BitVector n.
55  λs: BitVectorTrieSet n.
56    insert unit n b it s.
57
58definition set_empty ≝ λn. Stub unit n.
Note: See TracBrowser for help on using the repository browser.