[coq] Proof of de morgan laws

demorgan.v

(*[Proof of de Morgan laws with coq]*)
(*{NOTE: coq tactics for Propositional Logic]
  |- A -> B       =intro A1=> A1: A |- B
  |- A -> B -> C  =intros A1 B1=> A1: A, B1: B |- C
  |- A\/B         =left=> |- A
  |- A\/B         =right=> |- B
  |- A/\B         =split=> |- A ; |- B
  |- False        =absurd (A)=> |- ~A ; |- A

  AB: A->B |- B   =apply AB=> AB: A->B |- A
  AB: A/\B |- C   =destruct AB as [A1 B1]=> A1: A, B1: B |- C
  AB: A\/B |- C   =destruct AB as [A1 | B1]=> A1: A |- C ; B1: B |- C
  NA: ~A |- False =apply NA=> |- A
*)

Theorem deMorgan1 (A B: Prop): ~(A\/B) -> ~A/\~B.
Proof.
  intro NAB.
  split.

  (* NAB: ~(A\/B) |- ~A *)
  - intro A1.
    apply NAB.
    left.
    exact A1.

  (* NAB ~(A\/B) |- ~B *)
  - intro B1.
    apply NAB.
    right.
    exact B1.
Qed.

Print deMorgan1.

(* embed body code for the type with `refine` tactic*)
Theorem deMorgan1b (A B: Prop): ~(A\/B) -> ~A/\~B.
Proof.
  intro NAB.
  refine (conj (fun A1: A => NAB (or_introl A1))
               (fun B1: B => NAB (or_intror B1))).
Qed.

Print deMorgan1b.


Theorem deMorgan2 (A B: Prop): ~A/\~B -> ~(A\/B).
Proof.
  intros NANB AB.
  destruct NANB as [NA NB].
  destruct AB as [A1 | B1].

  (* NA:~A, NB:~B A1:A |- False *)
  - apply NA.
    exact A1.

  (* NA:~A, NB:~B B1:B |- False *)
  - apply NB.
    exact B1.
Qed.

Print deMorgan2.


(* with `case` tactic instread of both `destruct`*)
Theorem deMorgan2b (A B: Prop): ~A/\~B -> ~(A\/B).
Proof.
  intros NANB AB.
  case AB.

  (* NANB:~A/\~B |- A->False *)
  - intro A1.
    case NANB.
    (* A1: A |- ~A->~B->False *)
    intros NA NB.
    apply NA.
    exact A1.

  (* NANB:~A/\~B |- B->False *)
  - intro B1.
    case NANB.
    (* B1: B |- ~A->~B->False *)
    intros NA NB.
    apply NB.
    exact B1.
Qed.

Print deMorgan2b.


Theorem deMorgan3 (A B: Prop): ~A\/~B -> ~(A/\B).
Proof.
  intros NANB AB.
  destruct AB as [A1 B1].
  destruct NANB as [NA | NB].

  (* A1: A, B1: B, NA:~A |- False *)
  - apply NA.
    exact A1.

  (* A1: A, B1: B, NB:~B |- False *)
  - apply NB.
    exact B1.
Qed.

Print deMorgan3.


(*
   This case of demorgan requires the axiom NNPP: ~~A -> A
   - same as: (~A->False)->A , or as: ((A->False)->False)->A
   |- A =apply NNPP=> |- ~A->False
*)
Require Import Classical.
Theorem deMorgan4 (A B: Prop): ~(A/\B) -> ~A\/~B.
Proof.
  intro NAB.
  apply NNPP.
  intro NNANB.
  apply NAB.
  split.

  (* NNANB: ~(~A\/~B) |- A *)
  - apply NNPP.
    intro NA.
    apply NNANB.
    left.
    exact NA.

  (* NNANB: ~(~A\/~B) |- B *)
  - apply NNPP.
    intro NB.
    apply NNANB.
    right.
    exact NB.
Qed.

Print deMorgan4.


(*[NOTE: Prop types on coq]
  Type hierarchy
  - Type: Type
  - Set Prop: Type
  - nat bool: Set    (builtin value types)
  - True False: Prop
  - A B C ... : Prop (user defined propositions)

  I: True
   : False (no functions of False type existed)
  
  and A B := conj: A->B->A/\B
  or A B := or_introl A->A\/B
          | or_introl B->A\/B

  ~A == A -> False  
*)

(*[Appendix: traditional proof tree rules of /\-elim \/-elim with coq]
  and_ind: (A->B->P) -> (A/\B) -> P
  or_ind: (A->P) -> (B->P) -> (A\/B) -> P

  |- P =apply and_ind with A B=> |- A->B->P ; |- A/\B->P
  |- P =apply or_ind with A B=> |- A->P ; |- B->P ; |- A\/B->P

  
  |- A ==> |- A/\B                 (and-l-elim)
  |- B ==> |- A/\B                 (and-r-elim)
  |- C ==> |- A\/B ; A |- C; B |- C  (or-elim)
 *)
(* make custom tactic for and-l-elim / and-r-elim *)
Theorem and_elim_l (A B: Prop): A/\B->A.
Proof.
  intro AB.
  apply and_ind with A B.
  (* AB: A/\B |- A->B->A *)
  - intros A1 B1.
    exact A1.
  (* AB: A/\B |- A/\B *)
  - exact AB.
Qed.
Theorem and_elim_r (A B: Prop): A/\B->B.
Proof.
  intro AB.
  apply and_ind with A B.
  (* AB: A/\B |- A->B->B *)
  - intros A1 B1.
    exact B1.
  (* AB: A/\B |- A/\B *)
  - exact AB.
Qed.
Ltac and_l_elim B := apply and_elim_l with B.
Ltac and_r_elim A := apply and_elim_r with A.

(* with traditional axiom style: and_elim_l and_elim_r *)
Theorem and_refl0 (A B: Prop): A/\B -> B/\A.
Proof.
  intro AB.
  split.
  
  (* AB: A/\B |- B *)
  - and_r_elim A.
    (* AB: A/\B |- A/\B *)
    exact AB.
      
  (* AB: A/\B |- A *)
  - and_l_elim B.
    (* AB: A/\B |- A/\B *)
    exact AB.
Qed.

(* with applying and_ind directly *)
Theorem and_refl (A B: Prop): A/\B -> B/\A.
Proof.
  intro AB.
  split.
  
  (* AB: A/\B |- B *)
  - apply and_ind with A B.
    (* AB: A/\B |- A->B->B *)
    + intros A1 B1.
      exact B1.
    (* AB: A/\B |- A/\B *)
    + exact AB.
      
  (* AB: A/\B |- A *)
  - apply and_ind with A B.
    (* AB: A/\B |- A->B->A *)
    + intros A1 B1.
      exact A1.
    (* AB: A/\B |- A/\B *)
    + exact AB.
Qed.

(* or_ind is same as traditional axiom:  or_elim *)
Theorem or_refl (A B: Prop): A\/B -> B\/A.
Proof.
  intro AB.
  apply or_ind with A B.

  (* AB: A\/B |- A->B\/A *)
  - intro A1.
    right.
    exact A1.
    
  (* AB: A\/B |- B->B\/A *)
  - intro B1.
    left.
    exact B1.
    
  (* AB: A/\B |- A/\B *)
  - exact AB.
Qed.

(*
  [How to use this on coqtop]
  $ coqc demorgan.v
  $ ledit coqtop
  Coq < Require Import demorgan.
  Coq < Print deMorgan0.
  deMorgan0 =
  fun (A B : Prop) (NAB : ~ (A \/ B)) =>
  conj (fun A1 : A => NAB (or_introl A1)) (fun B1 : B => NAB (or_intror B1))
       : forall A B : Prop, ~ (A \/ B) -> ~ A /\ ~ B
  
  Argument scopes are [type_scope type_scope _]
  
  Coq <
*)

demorgan_pred.v

(* de Morgan laws  for Predicate Logic *)

Theorem deMorgan1 (A: Type) (P: A->Prop):
  ~(exists x: A, P x) -> (forall x: A, ~(P x)).
Proof.
  intros NxPx x0 Px0.
  apply NxPx.
  (* NxPx: ~(exists x: A, P x), x0: A, Px0: (P x0) |- exists x: A, P x *)
  exists x0.
  exact Px0.
Qed.

Print deMorgan1.

Theorem deMorgan2 (A: Type) (P: A->Prop):
  (forall x: A, ~(P x)) -> ~(exists x: A, P x).
Proof.
  intros xNPx xPx.
  destruct xPx as [x0 Px0].
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: (P x0)  |- False *)
  apply xNPx in Px0.
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: False  |- False *)
  exact Px0.
Qed.

Print deMorgan2.

Theorem deMorgan2a (A: Type) (P: A->Prop):
  (forall x: A, ~(P x)) -> ~(exists x: A, P x).
Proof.
  intros xNPx xPx.
  destruct xPx as [x0 Px0].
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: (P x0)  |- False *)
  specialize xNPx with x0 as NPx0.
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: (P x0), NPx0: ~(P x0)  |- False *)
  apply NPx0.
  exact Px0.
Qed.

Print deMorgan2a.

(* traditional style proof without `appky in` for hypo *)
Theorem deMorgan2b (A: Type) (P: A->Prop):
  (forall x: A, ~(P x)) -> ~(exists x: A, P x).
Proof.
  intros xNPx xPx.
  destruct xPx as [x0 Px0].
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: (P x0)  |- False *)
  absurd (P x0).
  
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: (P x0)  |- ~P x0 *)
  - apply xNPx.
  
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: (P x0)  |- P x0 *)
  - exact Px0.
Qed.

Print deMorgan2b.


Theorem deMorgan3 (A: Type) (P: A->Prop):
  (exists x: A, ~(P x)) -> ~(forall x: A, P x).
Proof.
  intros xNPx xPx.
  destruct xNPx as [x0 NPx0].
  (* xPx: (forall x: A, P x),  x0: A, NPx0: ~(P x0) |- False*)
  apply NPx0.
  (* xPx: (forall x: A, P x),  x0: A, NPx0: ~(P x0) |- P x0 *)
  apply xPx.
Qed.

Print deMorgan3.

Theorem deMorgan3a (A: Type) (P: A->Prop):
  (exists x: A, ~(P x)) -> ~(forall x: A, P x).
Proof.
  intros xNPx xPx.
  destruct xNPx as [x0 NPx0].
  (* xPx: (forall x: A, P x),  x0: A, NPx0: ~(P x0) |- False*)
  specialize xPx with x0 as Px0.
  (* xPx: (forall x: A, P x),  x0: A, NPx0: ~(P x0), Px0: (P x0)  |- False *)
  apply NPx0.
  exact Px0.
Qed.

Print deMorgan3a.


Theorem deMorgan4 (A: Type) (P: A->Prop):
  ~(forall x: A, P x) -> (exists x: A, ~(P x)).
Proof.
  Require Import Classical.
  
  intro NxPx.
  apply NNPP.
  intro NxNPx.
  (* NxPx: ~(forall x: A, P x), NxNPx: ~(exists x: A, ~P x) |- False *)
  apply NxPx.
  intro x0.
  apply NNPP.
  intro NPx0.
  (* NxPx: ~(forall x: A, P x), NxNPx: ~(exists x: A, ~P x),  
     x0: A, NPx0: ~(P x0) |- False *)
  apply NxNPx.
  exists x0.
  exact NPx0.
Qed.

Print deMorgan4.

(* Appendix A: reversed law ~P x <=> P x with double deMorgan4 *)
Theorem deMorgan4n (A: Type) (P: A->Prop):
  ~(forall x: A, ~P x) -> (exists x: A, P x).
Proof.
  intro NxNPx.
  apply deMorgan4 in NxNPx as xNNPx.
  (* NxNPx, xNNPx: (exists x: A, ~~P x) |- exists x: A, P x *)
  destruct xNNPx as [x0 NNPx0].
  (* NxNPx, x0: A, NNPx0: ~~(P x0) |- exists x: A, P x *)
  (*NOTE: ~~(P x0) => ~(P x0 -> False) => ~(forall _: P x0, False) *)
  apply deMorgan4 in NNPx0 as Px0NF.  
  (* NxNPx, x0, NNPx0, Px0NF: (exists _: (P x0), ~False) |- exists x: A, P x *)
  destruct Px0NF as [Px0 NF].
  exists x0.
  exact Px0.
Qed.

Print deMorgan4n.


(* Appendix B: NNPP proven with deMorgan4 *)
Theorem nnpp (P: Prop): ~~P -> P.
Proof.
  intro NNP.
  apply deMorgan4 in NNP as PNN.
  destruct PNN as [P0 NN].
  exact P0.
Qed.

Print nnpp.