102 lines
1.9 KiB
Coq
102 lines
1.9 KiB
Coq
Theorem dM1: forall A B:Prop,
|
|
~(or A B) -> and (~A) (~B).
|
|
Proof.
|
|
intros A B H.
|
|
split.
|
|
- intro a.
|
|
apply (H (or_introl a)).
|
|
- intro b.
|
|
exact (H (or_intror b)).
|
|
Qed.
|
|
|
|
Theorem dM1r: forall A B:Prop,
|
|
and (~A) (~B) -> ~(or A B).
|
|
Proof.
|
|
intros A B.
|
|
intro nA_and_nB.
|
|
intro AorB.
|
|
unfold not in nA_and_nB.
|
|
destruct AorB.
|
|
- destruct nA_and_nB.
|
|
exact (H0 H).
|
|
- destruct nA_and_nB.
|
|
exact (H1 H).
|
|
Qed.
|
|
|
|
Theorem dM2r: forall A B:Prop,
|
|
or (~A) (~B) -> ~(and A B).
|
|
Proof.
|
|
intros A B H.
|
|
unfold not.
|
|
intro A_and_B.
|
|
destruct H.
|
|
- unfold not in H.
|
|
destruct A_and_B.
|
|
exact (H H0).
|
|
- destruct A_and_B.
|
|
unfold not in H.
|
|
exact (H H1).
|
|
Qed.
|
|
|
|
(* The unprovable de-Morgan law is equivalent ot LEM *)
|
|
(* https://github.com/coq-community/coq-art/blob/master/ch5_everydays_logic/SRC/class.v#L53 *)
|
|
|
|
Definition lem := forall P:Prop, P\/~P.
|
|
Definition deM := forall P Q:Prop, ~(~P/\~Q)->P\/Q.
|
|
|
|
Lemma foo : deM -> lem.
|
|
Proof.
|
|
unfold lem.
|
|
intros H P.
|
|
apply H. (* P=P, Q=~P *) (* New goal: ~(~P /\ ~~P) *)
|
|
intros [HnP HnnP].
|
|
contradiction.
|
|
Qed.
|
|
Lemma foo_r : lem -> deM.
|
|
Proof.
|
|
unfold lem.
|
|
intro H.
|
|
unfold deM.
|
|
intros P Q.
|
|
intro H2.
|
|
(*
|
|
intros [HnP HnQ].
|
|
intros H P.
|
|
apply H. (* P=P, Q=~P *) (* New goal: ~(~P /\ ~~P) *)
|
|
intros [HnP HnnP].
|
|
contradiction.
|
|
*)
|
|
Abort.
|
|
|
|
Theorem foo23:
|
|
let deM := forall A B:Prop, ~(~A /\ ~B) -> (A \/ B) in
|
|
let lem := forall A:Prop, A \/ ~A in
|
|
deM -> lem.
|
|
Proof.
|
|
intros dem lem.
|
|
subst lem.
|
|
intro dm.
|
|
intro A.
|
|
apply dm.
|
|
intros [HnP HnnP].
|
|
contradiction.
|
|
Qed.
|
|
|
|
Theorem foo32:
|
|
let deM := forall A B:Prop, ~(~A /\ ~B) -> (A \/ B) in
|
|
let lem := forall A:Prop, A \/ ~A in
|
|
lem -> deM.
|
|
Proof.
|
|
intros lem dem.
|
|
subst dem.
|
|
intro dm.
|
|
Abort.
|
|
|
|
Goal forall a b:Prop,
|
|
~a \/ ~b -> ~(a /\ b).
|
|
Proof.
|
|
intros a b HaOrb Hab.
|
|
destruct Hab as [Ha Hb].
|
|
destruct HaOrb; apply H; assumption.
|
|
Qed.
|