Line | |
---|

1 | include "ASM/BitVectorTrie.ma". |
---|

2 | include "ASM/Util.ma". |
---|

3 | |
---|

4 | definition BitVectorTrieSet ≝ BitVectorTrie unit. |
---|

5 | |
---|

6 | let 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 | ] |
---|

31 | qed. |
---|

32 | |
---|

33 | let 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 | ] |
---|

51 | qed. |
---|

52 | |
---|

53 | let 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 | ] |
---|

77 | qed. |
---|

78 | |
---|

79 | definition set_insert ≝ |
---|

80 | λn: nat. |
---|

81 | λb: BitVector n. |
---|

82 | λs: BitVectorTrieSet n. |
---|

83 | insert unit n b it s. |
---|

84 | |
---|

85 | definition set_empty ≝ λn. Stub unit n. |
---|

86 | |
---|

87 | definition set_singleton ≝ |
---|

88 | λn: nat. |
---|

89 | λb: BitVector n. |
---|

90 | insert unit n b it (set_empty ?). |
---|

**Note:** See

TracBrowser
for help on using the repository browser.