coqlogical-foundations

How to apply a lemma to 2 hypothesis

Theorem ev_plus_plus : forall n m p,
  even (n+m) -> even (n+p) -> even (m+p).
Proof.
  intros n m p Hnm Hnp.

We get this:

1 subgoal (ID 189)
  
  n, m, p : nat
  Hnm : even (n + m)
  Hnp : even (n + p)
  ============================
  even (m + p)

Also we have a previously proven theorem:

ev_sum
     : forall n m : nat, even n -> even m -> even (n + m)

We know that (n+m) is even and (n+p) is even. How to create a new hypothesis in the context by applying ev_sum to Hnm and Hnp:

Hsum: even((n+m) + (n+p))

?

Solution

  • You have several options for this. You can use pose proof like this:

    pose proof (ev_sum _ _ Hnm Hnp) as Hsum.

    it will do what you expect. It allows you to give a term and add it as a hypothesis.

    Another option is to use eapply ... in. For instance you can do

    eapply ev_sum in Hnm.

    And then you have to give it Hnp in one of the subgoals.