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
|
From Coq Require Import Setoid.
(** NOTE: These should fit into a larger picture, e.g. lattices or monoids **)
(** And/Conjunction **)
Lemma and_True_iff : forall P, (P /\ True) <-> P.
Proof. intuition. Qed.
Lemma and_and_iff : forall P, (P /\ P) <-> P.
Proof. intuition. Qed.
Lemma and_assoc : forall P Q R, (P /\ Q /\ R) <-> ((P /\ Q) /\ R).
Proof. intuition. Qed.
Lemma and_comm : forall P Q, (P /\ Q) <-> (Q /\ P).
Proof. intuition. Qed.
Lemma and_False_iff : forall P, (P /\ False) <-> False.
Proof. intuition. Qed.
Lemma and_cancel
: forall P Q R : Prop, (P -> (Q <-> R)) -> ((P /\ Q) <-> (P /\ R)).
Proof. intuition. Qed.
Lemma and_iff
: forall P Q R S : Prop,
(P <-> R) ->
(P -> (Q <-> S)) ->
((P /\ Q) <-> (R /\ S)).
Proof. clear; intuition. Qed.
(** Or/Disjunction **)
Lemma or_False_iff : forall P, (P \/ False) <-> P.
Proof. intuition. Qed.
Lemma or_or_iff : forall P, (P \/ P) <-> P.
Proof. intuition. Qed.
Lemma or_assoc : forall P Q R, (P \/ Q \/ R) <-> ((P \/ Q) \/ R).
Proof. intuition. Qed.
Lemma or_comm : forall P Q, (P \/ Q) <-> (Q \/ P).
Proof. intuition. Qed.
Lemma or_True_iff : forall P, (P \/ True) <-> True.
Proof. intuition. Qed.
(** Implication **)
Lemma impl_True_iff : forall (P : Prop), (True -> P) <-> P.
Proof.
clear; intros; tauto.
Qed.
Lemma impl_iff
: forall P Q R S : Prop,
(P <-> R) ->
(P -> (Q <-> S)) ->
((P -> Q) <-> (R -> S)).
Proof. clear. intuition. Qed.
Lemma impl_eq : forall (P Q : Prop), P = Q -> (P -> Q).
Proof. clear. intros; subst; auto. Qed.
Lemma uncurry : forall (P Q R : Prop),
(P /\ Q -> R) <-> (P -> Q -> R).
Proof. clear. tauto. Qed.
(** Forall **)
Lemma forall_iff : forall T P Q,
(forall x,
P x <-> Q x) ->
((forall x : T, P x) <-> (forall x : T, Q x)).
Proof.
intros. setoid_rewrite H. reflexivity.
Qed.
Lemma forall_impl : forall {T} (P Q : T -> Prop),
(forall x, P x -> Q x) ->
(forall x, P x) -> (forall x, Q x).
Proof.
clear. intuition.
Qed.
(** Exists **)
Lemma exists_iff : forall T P Q,
(forall x,
P x <-> Q x) ->
((exists x : T, P x) <-> (exists x : T, Q x)).
Proof.
intros. setoid_rewrite H. reflexivity.
Qed.
Lemma exists_impl : forall {T} (P Q : T -> Prop),
(forall x, P x -> Q x) ->
(exists x, P x) -> (exists x, Q x).
Proof.
clear. intuition.
destruct H0; eauto.
Qed.
Lemma iff_eq : forall (P Q : Prop), P = Q -> (P <-> Q).
Proof. clear. intros; subst; reflexivity. Qed.
|
