-
Notifications
You must be signed in to change notification settings - Fork 0
/
andbprops.v
186 lines (139 loc) · 4.82 KB
/
andbprops.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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
(************************************************************************)
(* Copyright (c) 2017, Ajay Kumar Eeralla <ae266@mail.missouri.edu> *)
(* University of Missouri-Columbia. *)
(* *)
(* *)
(* *)
(************************************************************************)
Load "ex5_4_IFMORPH".
(** * [andB] properties *)
(** This library defines some of the properties of [andB]. *)
(** [FAlse] if one of them is [FAlse]. *)
Lemma andB_FAlse_intro1 : forall b1 b2 : Bool, b1 ## FAlse -> b1 & b2 ## FAlse.
Proof.
intros.
unfold andB .
rewrite H.
apply IFFALSE_B.
Qed.
Lemma andB_FAlse_intro2 : forall b1 b2:Bool, b2 ## FAlse -> b1 & b2 ## FAlse.
Proof. intros. unfold andB. rewrite H. apply IFSAME_B. Qed.
Lemma andB_FAlse_r : forall b:Bool, b & FAlse ## FAlse.
Proof. intros. unfold andB. apply IFSAME_B. Qed.
Lemma andB_FAlse_l : forall b: Bool, FAlse & b ## FAlse.
Proof. intros. unfold andB. apply IFFALSE_B. Qed.
Lemma andB_diag : forall n, (Bvar n) & (Bvar n) ## (Bvar n).
Proof. intros. unfold andB. rewrite IFEVAL_B. simpl.
rewrite <- beq_nat_refl.
rewrite IFTF.
reflexivity.
Qed.
(** Invariant under [TRue]. *)
Lemma andB_TRue_r : forall b:Bool, b & TRue ## b.
Proof. intros. unfold andB.
pose proof (IFTF 1).
apply Forall_ELM_EVAL_B with (n :=1)(b:=b) in H.
simpl in H.
apply H. Qed.
Lemma andB_TRue_l : forall b:Bool, TRue & b ## b.
Proof. intros. unfold andB.
apply IFTRUE_B.
Qed.
Lemma andB_notb_r : forall n, (Bvar n) & (notb (Bvar n)) ## FAlse.
Proof. intros. unfold andB . unfold notb. rewrite IFEVAL_B. simpl. rewrite <- beq_nat_refl.
rewrite IFTRUE_B. rewrite IFSAME_B. reflexivity. Qed.
(** [andB] is commutative. *)
Lemma andB_comm1: forall n1 n2 , ( (Bvar n1) & (Bvar n2)) ## ( (Bvar n2) & (Bvar n1)).
Proof. intros. unfold andB. rewrite <- IFTF with (n:= n2) at 1 .
rewrite IFMORPH_B1 with (n1:= n2) (n2:=n1). rewrite IFTF with (n:= n1). rewrite IFSAME_B. reflexivity. Qed.
Axiom andB_comm: forall (b1 b2: Bool), (b1 & b2) ## (b2 & b1).
(** [andB] is associative *)
Lemma andB_assoc1 : forall n1 n2 n3, (Bvar n1) & ((Bvar n2) & (Bvar n3)) ##( ((Bvar n1) & (Bvar n2)) & (Bvar n3)).
Proof. intros. unfold andB.
pose proof(andB_comm1).
unfold andB in H.
pose proof (IFMORPH_B1).
rewrite IFMORPH_B1 with (n1:= n2) (n2:= n1).
rewrite H with (n1:=n1) (n2:= n2).
rewrite IFMORPH_B2.
rewrite IFSAME_B.
rewrite IFFALSE_B.
reflexivity.
Qed.
Axiom andB_assoc: forall (b1 b2 b3: Bool), (b1 & b2) & b3 ## b1 & (b2 & b3).
Axiom andB_prop : forall a b:Bool, (andB a b) ## TRue -> (a ## TRue) /\ (b ## TRue).
Lemma andB_TRue_intro : forall b1 b2:Bool, b1 ## TRue /\ b2 ## TRue -> (andB b1 b2) ## TRue.
Proof. intros.
inversion H.
unfold andB.
rewrite H0.
rewrite IFTRUE_B.
assumption.
Qed.
Lemma andB_TRue_iff : forall n1 n2, (Bvar n1) & (Bvar n2) ## TRue <-> (Bvar n1) ## TRue /\ (Bvar n2) ## TRue.
Proof. split.
apply andB_prop.
apply andB_TRue_intro.
Qed.
(** [notb] properties *)
Lemma notB_involutive : forall n, (notb (notb (Bvar n))) ## (Bvar n).
Proof. intros. unfold notb.
rewrite IFMORPH_B2. rewrite IFFALSE_B. rewrite IFTRUE_B.
rewrite IFTF. reflexivity. Qed.
Lemma notB_TRue_iff : forall n, ( notb (Bvar n)) ## TRue <-> (Bvar n) ## FAlse.
Proof.
intros. split.
intros.
rewrite <- notB_involutive.
rewrite H.
unfold notb .
rewrite IFTRUE_B.
reflexivity.
intros.
rewrite H.
unfold notb.
rewrite IFFALSE_B.
reflexivity.
Qed.
Lemma notb_FAlse_iff : forall n, (notb (Bvar n)) ## FAlse <-> (Bvar n) ## TRue.
Proof. intros. split.
intros. rewrite <- notB_involutive. rewrite H. unfold notb. rewrite IFFALSE_B. reflexivity.
intros. rewrite H. unfold notb.
rewrite IFTRUE_B. reflexivity. Qed.
(** [andB] complement *)
Lemma and_notB_r : forall n, (Bvar n) & (notb (Bvar n)) ## FAlse.
Proof. intros. unfold andB.
unfold notb. rewrite IFMORPH_B1.
rewrite IFIDEMP_B. rewrite IFSAME_B. reflexivity. Qed.
Lemma and_notB_l : forall n, (notb (Bvar n)) & (Bvar n) ## FAlse.
Proof. intros. unfold andB.
unfold notb. rewrite IFMORPH_B2.
rewrite IFFALSE_B, IFTRUE_B.
rewrite IFEVAL_B.
simpl.
rewrite <- beq_nat_refl.
rewrite IFSAME_B.
reflexivity. Qed.
Theorem b1_notb2 : forall (n1 : nat) , (Bvar n1) &(notb (Bvar (n1+1))) ##
(ifb (Bvar (n1+1)) FAlse (Bvar n1)) .
Proof.
intros.
unfold notb, andB.
rewrite <- IFSAME_B with (b:= (Bvar (n1+1))) (b1:= (ifb (Bvar n1) (ifb (Bvar (n1 + 1)) FAlse TRue) FAlse)).
rewrite IFEVAL_B with (n := (n1+1)).
simpl.
rewrite <- beq_nat_refl.
rewrite IFFALSE_B.
rewrite IFTRUE_B.
rewrite IFSAME_B.
(*************)
assert(H: beq_nat n1 (n1 + 1) = false).
induction n1.
reflexivity.
simpl.
assumption.
(************)
rewrite H.
rewrite IFTF.
reflexivity.
Qed.