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
| Require Import Classical.
Variable T : Set.
Variable A : T -> Prop.
Variable B : Prop.
Variable T_nonempty : T.
Definition lhs
:= (forall x, A x) -> B.
Definition rhs
:= exists x, (A x -> B).
Theorem dir_b
: rhs -> lhs.
Proof.
unfold lhs. unfold rhs. intros.
inversion H. apply H1. apply H0.
Qed.
Theorem dir_a
: lhs -> rhs.
Proof.
unfold lhs. unfold rhs. intro H.
assert ((forall x : T, A x) \/ (~(forall x : T, A x))) as Hem.
apply classic. inversion Hem as [HT | HF].
(* forall x : T, A x
We already have B, so the witness of T nonempty is enough. *)
exists T_nonempty. intros AT. apply H. apply HT.
(* ~(forall x : T, A x)
Rewrite to exists x, A x -> False, use ex falso to get B. *)
apply not_all_ex_not in HF. inversion HF as [x NAx].
exists x. intros Ax. unfold not in NAx.
apply NAx in Ax. inversion Ax.
Qed.
Theorem both
: lhs <-> rhs.
Proof.
unfold iff. split. apply dir_a. apply dir_b.
Qed.
|