The Coq mailing list

[троль <vuvupik AT gmail.com>]

Sorry, i've made a mistake. It should be
Theorem prove_first_init : forall Q P : Prop,
 Q -> (Q -> P) -> P.
Proof. intuition. Qed.

instead of

Theorem prove_first_init : forall P Q : Prop,
 Q -> (Q -> P) -> P.
Proof. intuition. Qed.

2013/12/25, троль 
<vuvupik AT gmail.com>:
> Theorem conj_assoc : forall P Q R : Prop,
>  P /\ Q /\ R -> (P /\ Q) /\ R.
> Proof. intuition. Qed.
>
> Theorem prove_first_init : forall P Q : Prop,
>  Q -> (Q -> P) -> P.
> Proof. intuition. Qed.
>
> Theorem remove_first : forall P Q : Prop,
>  (Q -> P) -> (Q -> Q /\ P).
> Proof. intuition. Qed.
>
> Theorem remove_middle : forall P1 P2 Q : Prop,
>  (Q -> P1 /\ P2) -> (Q -> P1 /\ Q /\ P2).
> Proof. intuition. Qed.
>
> Theorem remove_last : forall P Q : Prop,
>  (Q -> P) -> (Q -> P /\ Q).
> Proof. intuition. Qed.
>
> Theorem move_to_next_conj : forall P1 P2 P3 Q : Prop,
>  (Q -> (P1 /\ P2) /\ P3) -> (Q -> P1 /\ P2 /\ P3).
> Proof. intuition. Qed.
>
> Tactic Notation "prove_first" ident(P) :=
>  apply (prove_first_init P); [|
>   try (apply remove_first); repeat (apply move_to_next_conj; try
> (apply remove_middle));
>    try (apply remove_last); intro; repeat (apply conj_assoc)
>  ].
>
> Example example : forall Hyp1 Hyp2 P1 P2 P3 P4,
>  Hyp1 -> Hyp2 -> P1 /\ P2 /\ P3 /\ P4.
> Proof.
>  intros. prove_first P3. (*                       goal : P1 /\ P2 /\ P3 /\
> P4 *)
>     admit.               (*                       goal : P3
>  *)
>     prove_first P1.      (* context : P3;         goal : P1 /\ P2 /\ P4
>  *)
>        admit.            (* context : P3;         goal : P1
>  *)
>        prove_first P4.   (* context : P3, P1;     goal : P2 /\ P4
>  *)
>           admit.         (* context : P3, P1;     goal : P4
>  *)
>           admit.         (* context : P3, P1, P4; goal : P2
>  *)
> Qed.
>