-
Notifications
You must be signed in to change notification settings - Fork 9
/
Copy pathAddrs.v
76 lines (65 loc) · 2.18 KB
/
Addrs.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
(** Copyright (c) 2015 Bill White **)
(** Distributed under the MIT/X11 software license **)
(** See http://www.opensource.org/licenses/mit-license.php **)
(** Addrs : Representation of addresses as 160 bit sequences. **)
Require Export Prelude.
Fixpoint bitseq (n:nat) : Type :=
match n with
| 0 => unit
| S n' => (bool * bitseq n')%type
end.
Definition bitseq_eq_dec {n} (bs1 bs2:bitseq n) : { bs1 = bs2 } + { bs1 <> bs2 }.
induction n as [|n IHn].
- destruct bs1, bs2. decide equality.
- destruct bs1 as [b1 bs1], bs2 as [b2 bs2]. repeat decide equality.
Defined.
Definition addr := bitseq 160.
Definition addr_eq_dec (a1 a2: addr) : { a1 = a2 } + { a1 <> a2 }.
apply bitseq_eq_dec.
Defined.
Fixpoint strip_bitseq_false {n:nat} {X:Type} (l:list (bitseq (S n) * X)%type) : list (bitseq n * X)%type :=
match l with
| nil => nil
| cons ((false,bs),x) l' => cons (bs,x) (strip_bitseq_false l')
| cons ((true,bs),x) l' => strip_bitseq_false l'
end.
Fixpoint strip_bitseq_true {n:nat} {X:Type} (l:list (bitseq (S n) * X)%type) : list (bitseq n * X)%type :=
match l with
| nil => nil
| cons ((true,bs),x) l' => cons (bs,x) (strip_bitseq_true l')
| cons ((false,bs),x) l' => strip_bitseq_true l'
end.
Lemma strip_bitseq_false_iff {n} {X} (alpha:bitseq n) (x:X) (l:list (bitseq (S n) * X)%type) :
In (alpha,x) (strip_bitseq_false l) <-> In ((false,alpha),x) l.
induction l as [|[[[|] beta] y] l IH].
- simpl. tauto.
- simpl. split.
+ intros H1. right. now apply IH.
+ intros [H1|H1].
* inversion H1.
* now apply IH.
- simpl. split.
+ intros [H1|H1].
* left. inversion H1. reflexivity.
* right. now apply IH.
+ intros [H1|H1].
* inversion H1. now left.
* right. now apply IH.
Qed.
Lemma strip_bitseq_true_iff {n} {X} (alpha:bitseq n) (x:X) (l:list (bitseq (S n) * X)%type) :
In (alpha,x) (strip_bitseq_true l) <-> In ((true,alpha),x) l.
induction l as [|[[[|] beta] y] l IH].
- simpl. tauto.
- simpl. split.
+ intros [H1|H1].
* left. inversion H1. reflexivity.
* right. now apply IH.
+ intros [H1|H1].
* inversion H1. now left.
* right. now apply IH.
- simpl. split.
+ intros H1. right. now apply IH.
+ intros [H1|H1].
* inversion H1.
* now apply IH.
Qed.