title: How to prove the mutual equivalence of peirce, classic, excluded_middle, de_morgan_not_and_not and implies_to_or without using intuition in coq
body: <p>I simplified the proof procedure of the mutual equivalence of peirce, classic, excluded_middle, de_morgan_not_and_not and implies_to_or primarily written in <code>git@github.com:B-Rich/sf.git</code> as following.</p>
  
  <pre><code>Theorem excluded_middle_irrefutable:  forall (P:Prop), ~ ~ (P \/ ~ P).
  Proof.
    intros. unfold not. intros.
    apply H. right. intros. apply H. left. apply H0.
  Qed.
  
  Definition peirce                := forall P Q: Prop, ((P-&gt;Q)-&gt;P)-&gt;P.
  Definition classic               := forall P :  Prop, ~~P -&gt; P.
  Definition excluded_middle       := forall P :  Prop, P \/ ~P.
  Definition de_morgan_not_and_not := forall P Q: Prop, ~(~P /\ ~Q) -&gt; P\/Q.
  Definition implies_to_or         := forall P Q: Prop, (P-&gt;Q) -&gt; (~P\/Q).
  
  Theorem peirce_classic : peirce -&gt; classic.
  Proof.
    compute. intros.
    specialize (H P False).
    apply H. intros.
    apply H. contradiction H0.
  Qed.
  
  Theorem classic_excluded_middle : classic -&gt; excluded_middle.
  Proof.
    compute. intros.
    apply H. intros.
    apply H0.
    right.
    intros.
    assert (P \/ (P-&gt;False)) as H2.
      apply (or_introl H1).
    apply (H0 H2).
  Qed.
  
  Theorem false_dist_1 : forall {P Q : Prop}, (P \/ Q -&gt; False) -&gt; (P -&gt; False) /\ (Q -&gt; False).
  Proof.
    intros.
    split.
    intros.
    apply (H (or_introl H0)).
    intros.
    apply (H (or_intror H0)).
  Qed.
  
  Theorem false_dist_2 : forall {P Q : Prop}, (P -&gt; False) /\ (Q -&gt; False) -&gt; (P \/ Q -&gt; False).
  Proof.
    intros.
    inversion H.
    inversion H0.
    apply (H1 H3).
    apply (H2 H3).
  Qed.
  
  Theorem em_de_morgan : excluded_middle -&gt; de_morgan_not_and_not.
  Proof.
    compute. intros.
    specialize (H (P \/ Q)).
    inversion H.
    apply H1.
    apply (False_ind (P \/ Q) (H0 (false_dist_1 H1))).
  Qed.
  
  Theorem double_neg : forall P : Prop,
    P -&gt; ((P-&gt;False)-&gt;False).
  Proof.
    (* WORKED IN CLASS *)
    intros P H. intros G. apply G. apply H.  Qed.
  
  Theorem de_morgan_to_or : de_morgan_not_and_not -&gt; implies_to_or.
  Proof.
    compute. intros.
    specialize (H (P -&gt; False) Q).
    intuition.
  Qed.
  
  Theorem to_or_peirce: implies_to_or -&gt; peirce.
  Proof.
    compute. intros.
    specialize (H P P).
    intuition.
  Qed.
  </code></pre>
  
  <p>I remove some <code>intuition</code> tactics successfully, except the last two.</p>
  
  <p>My question is:</p>
  
  <ul>
  <li>How to prove to_or_peirce and de_morgan_to_or without using the <code>intuition</code> tactic?</li>
  <li>What does the <code>intuition</code> tactic do?</li>
  <li>Is there a way to extract the concrete procedures which might be generated by the <code>intuition</code> tactic?</li>
  </ul>