-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathaula4.v
89 lines (76 loc) · 1.66 KB
/
aula4.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
Require Import aula3.
Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
intros pareira. simpl. reflexivity. Qed.
Theorem plus_1_l : forall n:nat, 1 + n = S n.
Proof.
intros n. reflexivity. Qed.
Theorem mult_0_l : forall n:nat, 0 * n = 0.
Proof.
intros n. reflexivity. Qed.
Theorem plus_id_example : forall n m:nat,
n = m ->
n + n = m + m.
Proof.
intros n m.
intros H.
rewrite -> H.
reflexivity.
Qed.
Theorem mult_0_plus : forall n m : nat,
(0 + n) * m = n * m.
Proof.
intros n m.
rewrite plus_O_n.
reflexivity.
Qed.
Theorem mult_S_1 : forall n m : nat,
m = S n ->
m * (1 + n) = m * m.
Proof.
intros n m H.
rewrite -> H.
rewrite <- plus_1_l.
reflexivity.
Qed.
Theorem plus_1_neq_0_firsttry : forall n : nat,
beq_nat (n + 1) 0 = false.
Proof.
intros n.
simpl. (* does nothing! *)
Abort.
Theorem plus_1_neq_0 : forall n : nat,
beq_nat (n + 1) 0 = false.
Proof.
intros n. destruct n as [| n'].
- reflexivity.
- reflexivity.
Qed.
Theorem negb_involutive : forall b : bool,
negb (negb b) = b.
Proof.
intros b. destruct b.
- reflexivity.
- reflexivity.
Qed.
Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
intros b c. destruct b.
- destruct c.
+ reflexivity.
+ reflexivity.
- destruct c.
+ reflexivity.
+ reflexivity.
Qed.
Theorem andb3_exchange :
forall b c d, andb (andb b c) d = andb (andb b d) c.
Proof.
intros b c d. destruct b.
- destruct c.
{ destruct d. - reflexivity. - reflexivity. }
{ destruct d. - reflexivity. - reflexivity. }
- destruct c.
{ destruct d. - reflexivity. - reflexivity. }
{ destruct d. - reflexivity. - reflexivity. }
Qed.