nseg-jp/rirondb#2

log-proof0.txt

$ coqtop
Welcome to Coq 8.4pl4 (June 2014)

Coq < Definition proof0 : forall (P Q : Prop), ((P \/ Q) /\ ~P) -> Q.
1 subgoal

  ============================
   forall P Q : Prop, (P \/ Q) /\ ~ P -> Q

proof0 < intros.
1 subgoal

  P : Prop
  Q : Prop
  H : (P \/ Q) /\ ~ P
  ============================
   Q

proof0 < destruct H.
1 subgoal

  P : Prop
  Q : Prop
  H : P \/ Q
  H0 : ~ P
  ============================
   Q

proof0 < destruct H.
2 subgoals

  P : Prop
  Q : Prop
  H : P
  H0 : ~ P
  ============================
   Q

subgoal 2 is:
 Q

proof0 < destruct H0.
2 subgoals

  P : Prop
  Q : Prop
  H : P
  ============================
   P

subgoal 2 is:
 Q

proof0 < apply H.
1 subgoal

  P : Prop
  Q : Prop
  H : Q
  H0 : ~ P
  ============================
   Q

proof0 < apply H.
No more subgoals.

proof0 < Qed.
intros.
destruct H.
destruct H.
 destruct H0.
 apply H.

 apply H.

proof0 is defined

Coq < Check proof0.
proof0
     : forall P Q : Prop, (P \/ Q) /\ ~ P -> Q

Coq < Print proof0.
proof0 =
fun (P Q : Prop) (H : (P \/ Q) /\ ~ P) =>
match H with
| conj (or_introl H2) H1 => match H1 H2 return Q with
                            end
| conj (or_intror H2) _ => H2
end
     : forall P Q : Prop, (P \/ Q) /\ ~ P -> Q

Argument scopes are [type_scope type_scope _]

Coq <

proof0.v

Definition proof0 : forall (P Q : Prop), ((P \/ Q) /\ ~P) -> Q.
Proof.
  intros.
  destruct H.
  destruct H.
    destruct H0.
    apply H.

    apply H.
Qed.