@kikx さんと @lyrical_logical さんに教えてもらってます。
ichii386@count% coqtop [..ecture/functional/coq]
Welcome to Coq 8.2pl2 (July 2010)
Coq < Goal forall (P Q: Prop), (P -> Q) -> P -> Q.
1 subgoal
============================
forall P Q : Prop, (P -> Q) -> P -> Q
Unnamed_thm < intros.
1 subgoal
P : Prop
Q : Prop
H : P -> Q
H0 : P
============================
Q
Unnamed_thm < apply H.
1 subgoal
P : Prop
Q : Prop
H : P -> Q
H0 : P
============================
P
Unnamed_thm < exact H0.
Proof completed.
Unnamed_thm < Qed.
intros.
apply H.
exact H0.
Unnamed_thm is defined
Coq < Goal forall (P Q R: Prop), (P->Q->R)->(P->Q)->P->R.
1 subgoal
============================
forall P Q R : Prop, (P -> Q -> R) -> (P -> Q) -> P -> R
Unnamed_thm0 < intors.
Toplevel input, characters 0-6:
> intors.
> ^^^^^^
Error: The reference intors was not found in the current environment.
Unnamed_thm0 < intros.
1 subgoal
P : Prop
Q : Prop
R : Prop
H : P -> Q -> R
H0 : P -> Q
H1 : P
============================
R
Unnamed_thm0 < apply H.
2 subgoals
P : Prop
Q : Prop
R : Prop
H : P -> Q -> R
H0 : P -> Q
H1 : P
============================
P
subgoal 2 is:
Q
Unnamed_thm0 < exact H1.
1 subgoal
P : Prop
Q : Prop
R : Prop
H : P -> Q -> R
H0 : P -> Q
H1 : P
============================
Q
Unnamed_thm0 < apply H0.
1 subgoal
P : Prop
Q : Prop
R : Prop
H : P -> Q -> R
H0 : P -> Q
H1 : P
============================
P
Unnamed_thm0 < exact H1.
Proof completed.
Unnamed_thm0 < Qed.
intros.
apply H.
exact H1.
apply H0.
exact H1.
Unnamed_thm0 is defined
Coq < Goal forall (P Q R: Prop), (P->Q->R)->(P->Q)->P->R.
1 subgoal
============================
forall P Q R : Prop, (P -> Q -> R) -> (P -> Q) -> P -> R
Unnamed_thm1 < auto.
Proof completed.
Unnamed_thm1 < undo
Unnamed_thm1 < .
Error: No such subgoal
Unnamed_thm1 < Undo.
1 subgoal
============================
forall P Q R : Prop, (P -> Q -> R) -> (P -> Q) -> P -> R
Unnamed_thm1 < info auto.
== intro P; intro Q; intro R; intro H; intro H0; intro H1;
simple apply H.
exact H1.
simple apply H0; exact H1.
Proof completed.
Unnamed_thm1 < Qed.
info auto.
Unnamed_thm1 is defined
Coq < Print Unnamed_thm1.
Unnamed_thm1 =
fun (P Q R : Prop) (H : P -> Q -> R) (H0 : P -> Q) (H1 : P) => H H1 (H0 H1)
: forall P Q R : Prop, (P -> Q -> R) -> (P -> Q) -> P -> R
Argument scopes are [type_scope type_scope type_scope _ _ _]
Coq <Coq < Goal forall (P: Prop), P -> P. 1 subgoal ============================ forall P : Prop, P -> P Unnamed_thm2 < intro. 1 subgoal P : Prop ============================ P -> P Unnamed_thm2 < intro. 1 subgoal P : Prop H : P ============================ P Unnamed_thm2 < intro. Toplevel input, characters 0-5: > intro. > ^^^^^ Error: No product even after head-reduction. Unnamed_thm2 < apply H. Proof completed. Unnamed_thm2 < Qed. intro. intro. apply H. Unnamed_thm2 is defined
