blob: 7300937e05089b93f1ed9ccb5da1a096349c4e6b (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Setoid_Prop.v 10739 2008-04-01 14:45:20Z herbelin $: i*)
Require Import Setoid_tac.
(** * A few examples on [iff] *)
(** [iff] as a relation *)
Add Relation Prop iff
reflexivity proved by iff_refl
symmetry proved by iff_sym
transitivity proved by iff_trans
as iff_relation.
(** [impl] as a relation *)
Theorem impl_trans: transitive _ impl.
Proof.
hnf; unfold impl; tauto.
Qed.
Add Relation Prop impl
reflexivity proved by impl_refl
transitivity proved by impl_trans
as impl_relation.
(** [impl] is a morphism *)
Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
Proof.
unfold impl; tauto.
Qed.
(** [and] is a morphism *)
Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
tauto.
Qed.
(** [or] is a morphism *)
Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
Proof.
tauto.
Qed.
(** [not] is a morphism *)
Add Morphism not with signature iff ==> iff as Not_Morphism.
Proof.
tauto.
Qed.
(** The same examples on [impl] *)
Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
Proof.
unfold impl; tauto.
Qed.
Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
Proof.
unfold impl; tauto.
Qed.
Add Morphism not with signature impl --> impl as Not_Morphism2.
Proof.
unfold impl; tauto.
Qed.
|
