-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathTribool.v
130 lines (103 loc) · 2.91 KB
/
Tribool.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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
Inductive tribool : Set := ttrue : tribool | tfalse : tribool | unknown : tribool.
Delimit Scope tribool_scope with tribool.
Bind Scope tribool_scope with tribool.
(** probably to be declared as a coercion *)
Definition tribool_of_bool (b : bool) : tribool := if b then ttrue else tfalse.
(** Basic boolean operators *)
Definition andtb (b1 b2:tribool) : tribool :=
match b1, b2 with
| tfalse, _ => tfalse
| _, tfalse => tfalse
| unknown, _ => unknown
| _, unknown => unknown
| ttrue, ttrue => ttrue
end.
Definition ortb (b1 b2:tribool) : tribool :=
match b1, b2 with
| ttrue, _ => ttrue
| _, ttrue => ttrue
| unknown, _ => unknown
| _, unknown => unknown
| tfalse, tfalse => tfalse
end.
(*
Definition implb (b1 b2:bool) : bool := if b1 then b2 else true.
Definition xorb (b1 b2:bool) : bool :=
match b1, b2 with
| true, true => false
| true, false => true
| false, true => true
| false, false => false
end.
*)
Definition negtb (b:tribool) := match b with ttrue => tfalse | unknown => unknown | tfalse => ttrue end.
Infix "||" := ortb : tribool_scope.
Infix "&&" := andtb : tribool_scope.
Ltac destr_tribool :=
intros; destruct_all tribool; simpl in *; trivial; try discriminate.
(** We have several interpretations of tribools as propositions *)
Definition Is_ttrue (b:tribool) :=
match b with
| ttrue => True
| _ => False
end.
Definition Is_tfalse (b:tribool) :=
match b with
| tfalse => True
| _ => False
end.
Definition Is_unknown (b:tribool) :=
match b with
| unknown => True
| _ => False
end.
(** Decidability *)
Lemma tribool_dec : forall b1 b2 : tribool, {b1 = b2} + {b1 <> b2}.
Proof.
decide equality.
Defined.
(*************)
(** * Equality *)
(*************)
Definition eqb (b1 b2:tribool) : bool :=
match b1, b2 with
| ttrue, ttrue => true
| tfalse, tfalse => true
| unknown, unknown => true
| _, _ => false
end.
Lemma eqb_subst :
forall (P:tribool -> Prop) (b1 b2:tribool), eqb b1 b2 = true -> P b1 -> P b2.
Proof.
destr_tribool.
Qed.
Lemma eqb_reflx : forall b:tribool, eqb b b = true.
Proof.
destr_tribool.
Qed.
Lemma eqb_prop : forall a b:tribool, eqb a b = true -> a = b.
Proof.
destr_tribool.
Qed.
Lemma eqb_true_iff : forall a b:tribool, eqb a b = true <-> a = b.
Proof.
destr_tribool; intuition; discriminate.
Qed.
Lemma eqb_false_iff : forall a b:tribool, eqb a b = false <-> a <> b.
Proof.
destr_tribool; intuition; discriminate.
Qed.
Lemma negtb_negtb (b : tribool) : negtb (negtb b) = b.
Proof.
destr_tribool.
Qed.
Lemma negtb_andtb (b1 b2 : tribool) : negtb (andtb b1 b2) = ortb (negtb b1) (negtb b2).
Proof.
destr_tribool.
Qed.
Lemma negtb_ortb (b1 b2 : tribool) : negtb (ortb b1 b2) = andtb (negtb b1) (negtb b2).
Proof.
destr_tribool.
Qed.
Definition of_option_bool : option bool -> tribool :=
fun x => match x with Some b => tribool_of_bool b | _ => unknown end.