Search code examples
coqcoq-tactic

Tactic for existential hypothesis

Say we have a proposition P1 n, and there exists n for which it holds. Furthermore we have a proposition P2, where P1 n implies P2 for any n. How do we prove P2?

Parameter P1 : nat -> Prop.
Axiom some_p1 : exists n, P1 n.

Parameter P2 : Prop.
Axiom p1_implies_p2 : forall n, P1 n -> P2.

Theorem p2 : P2.

I tried

Proof.
  eapply p1_implies_p2.

which gives me the goal P1 ?n, but I'm not sure how to proceed from there.

Solution

  • You may eliminate some_p1to get a witness nand a hypothesis Hn.

    Theorem p2 : P2.
  case some_p1 ; intros n Hn.  apply (p1_implies_p2 _ Hn).
Qed.