-
Notifications
You must be signed in to change notification settings - Fork 0
/
deMorgenBool.v
48 lines (44 loc) · 1.09 KB
/
deMorgenBool.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
Require Import Bool.
(* Please ignore:
negb is just another name for
the not function for booleans,
more on that later.
*)
Definition not := negb.
Theorem deMorgen: forall x y:bool,
not (x || y) = (not x) && (not y).
Proof.
Abort.
Theorem deMorgen_answer: forall x y:bool,
not (x || y) = (not x) && (not y).
Proof.
intros.
(* We can start by doing case analysis on x into its two cases.
Almost like a truth table for computer scientists or
A very lame induction for mathematicians.
*)
Print bool.
(*
We can see that a bool is either true of false
*)
case x.
(* Now we have two cases to prove,
lets focus on our first goal
*)
-
(* Seems like some of this equation is simply solvable.
simpl can partially apply functions,
for you have only supplied limited arguments. *)
simpl.
(* false = false is true by reflexivity *)
reflexivity.
(* Coq helps us remember all cases.
The proof cannot complete,
if we haven't proved it for all cases.
*)
- (* seems like this can also be simplified *)
simpl.
(* not y = not y, no matter what y is *)
reflexivity.
Qed.
(* Qed = Proven *)