Coq 練習問題

coq1.v

Require Import ssreflect.
Section Coq1.
  Variable P Q R : Prop.
  Theorem imp_trans : (P -> Q) -> (Q -> R) -> P -> R.
  Proof.
    intros p q r.
    apply q.
    apply p.
    assumption.
  Qed.
    
  Theorem not_false : not False.
  Proof.
    (* ⊥ -> ⊥*)
    unfold not.
    intro p.
    contradiction.
  Qed.

  Theorem double_neg : P -> ~~P.
  Proof.
    unfold not.
    intros p pf.
    apply pf.
    assumption.
  Qed.

  Theorem contraposition : (P -> Q) -> ~Q-> ~P.
  Proof.
    unfold not.
    intros p q r.
    apply q.
    apply p.
    assumption.
  Qed.

  Theorem and_assoc : P /\ (Q /\ R) -> (P /\ Q) /\ R.
  Proof.
    move => [a b].
    move: b.
    move => [c d].
    split.
    split.
    done.
    done.
    done.
  Qed.
  Theorem and_distr : P /\ (Q \/ R) -> (P /\ Q) \/ (P /\ R).
  Proof.
    move => [].
    intro.
    move => [|].
    left.
    split.
    done.
    done.
    right.
    split.
    done.
    done.
  Qed.
  
  Theorem absurd : P -> ~P -> Q.
  Proof.
    rewrite /not. 
    move=>h.
    move=>i.
    exfalso.
    apply i.
    assumption.
  Qed.


  Definition DM_rev := forall P Q, ~ ((~P) /\ (~Q)) -> P \/ Q.
  Definition EM := forall P : Prop, P \/ (~P).
  Theorem DM_rev_is_EM : DM_rev <-> EM.
  Proof.
    rewrite /EM.
    rewrite /DM_rev.



    split.
    +  intro demo_rev.
      intro p0.
      specialize (demo_rev p0).
      specialize (demo_rev (~p0)).    
      rewrite /not in demo_rev.
      apply demo_rev.
       rewrite /not. 
      move => [pf pff].
      apply pff.
      assumption.


    +  intro em.
      intro p.
      intro q.
      rewrite /not.
      intro conj.
      specialize (em (p \/ q)).
      move: em.
      move => [|].
      intro a.
      assumption.
      intro b.
      exfalso.



      cut (~(p \/ q) -> ((p -> False) /\ (q -> False))).
      - intro hyp.
        apply hyp .
        assumption.
        exfalso.
        apply conj.
        apply hyp.
        assumption.
      - intro H.
        split.
        * intro HO.
          apply H.
          left.
          assumption.

        * intro HO.
          apply H.
          right.
          assumption.
  Qed.

End Coq1.