Doubts in Coq

coq_prop_logic.md

Dear Sir,
I was revising the exercises in propositional logic and I was having some doubts.

1. Working of destruct and case tactic on a Lemma.

   I understand destruct tactic works on hypothesis with /\, \/, and <-> operators in it.
   I have included a small code snippet that shows the basic usage of destruct in simple cases.

   Please click here to expand the code

   Section Propositonal_Logic.
   Variables P Q R: Prop.
   
   Section DestructAnd.
   Hypothesis H: P /\ Q.
   Lemma L1: P.
   Proof.
     destruct H as [PisTrue QisTrue].
     exact PisTrue.
   Qed.
   End DestructAnd.
   
   Section DestructOr.
   Hypothesis H: P \/ P.
   Lemma L2: P.
   Proof.
     destruct H. (* Introduce two subgoals for each case in H *)
     (* Gives error: Expects a disjunctive pattern with 2 branches. *)
     (* destruct H as [H1 H2]. *)
     exact H0.
     exact H0.
   Qed.
   End DestructOr.
   
   Section DestructEquiv.
   Hypothesis H: P <-> Q.
   Lemma L3: P -> Q.
   Proof.
     (* Similar to destruct on /\ operation *)
     destruct H as [PimpliesQ QimpliesP].
     exact PimpliesQ.
   Qed.
   End DestructEquiv.

   But on \/ operator, destruct H as .. doesn't seem to work, only destruct H seems to work.
   It gives an error: Expects a disjunctive pattern with 2 branches.
   However this only a minor problem of naming the new hypothesis, and I understand how it works.

   But I can't relate how destruct work there with how destruct Lemma works.
   Could you give a bit more insight on what is happening when we do destruct Lemma?
   Also could you explain a bit about how it is different from case Lemma?

   Example code for destruct Lemma

   Section Propositonal_Logic.
   Variables P Q R: Prop.
   
   Section Lemma.
   Hypothesis PisTrue: P.
   Lemma PorQ: P \/ Q.
   Proof.
   left.
   exact PisTrue.
   Qed.
   End Lemma.
   
   
   Lemma L: P -> (P \/ Q).
   Proof.
   
   (* Before:
   1 subgoal
   P, Q, R : Prop
   ______________________________________(1/1)
   P -> P \/ Q
   *)
   
   destruct PorQ.
   
   (* After:
   3 subgoals
   P, Q, R : Prop
   ______________________________________(1/3)
   P
   ______________________________________(2/3)
   P -> P \/ Q
   ______________________________________(3/3)
   P -> P \/ Q
   *)
   
   Qed.
   
   End Propositional_Logic.

2. Working of proof by absurdity method.
   From what I understand, in proof by absurdity method, we:

   • Assume the opposite of what we want to prove using a Variable conventionally named assume.
     (Is this in effect same as Hypothesis in Coq? Are we using Variable instead of Hypothesis for convention only?)
   • Prove a Lemma absurd: False using the above assumption.
   • Using the above Lemma, we prove what we originally wanted to prove.

   In the final step, I tried replacing the goal with propositions which are not true, but still I was able to complete the proof.
   Should this be possible?

   Example code

    Section Propositional_Logic.
    Variables P Q: Prop.
   
    Variable assume: ~(~P \/ P).
   
    Lemma demorgan: ~~P /\ ~P.
    Proof.
    unfold not.
    unfold not in assume.
    split.
    
    intro.
    apply assume.
    left.
    exact H.
   
    intro.
    apply assume.
    right.
    exact H.
    Qed.
   
    Lemma absurd: False.
    Proof.
    destruct demorgan.
    contradict H.
    exact H0.
    Qed.
   
    Theorem T1: Q.
    Proof.
    case absurd.
    Qed.
   
    End Propositional_Logic.