The Coq mailing list

[троль <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.