The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

Separate question: in Coq, is there a way to add a conjunct to a goal, e.g., for the purpose of obtaining a stronger induction hypothesis?

I don't know if there is a built-in way to do it, but it is easy enough to write a little tactic that will do this, like this:

(* add /\ B to the goal *)
Ltac strengthen B :=
  match goal with
  | |- ?A =>
    let H := fresh in
      assert (H : A /\ B); [ | destruct H; assumption]
  end.


Lemma foo : forall A B,
  A /\ B.
Proof.
  intros A B.
  strengthen (A \/ B).