5

I have two hypothesis, and I would like to use forward reasoning to apply a theorem that uses both of them.

My specific I have the hypothes

H0 : a + b = c + d
H1 : e + f = g + h

and I want to apply the theorem from the standard library:

f_equal2_mult
     : forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2

Now I know I could manually give the values for x1, y1, x2, y2, but I would like Coq to automatically determine those values when it unified with H0 and H1. I have figured out that I can get it to work like so:

eapply f_equal2_mult in H0; try exact H1.

But this feels like a hack, with the broken symmetry and the try. I really would like to be able to say apply f_equals2_mult in H0, H1 or something similarly clear. Is there a way like this?

Jeremy Salwen
  • 8,061
  • 5
  • 50
  • 73

1 Answers1

4

You could use pose proof to introduce the lemma in the context, and specialize to apply it to other hypotheses.

Lemma f (a b c d : nat) : a = b -> c = d -> False.
intros H1 H2.
pose proof f_equal2_mult as pp.
specialize pp with (1 := H1).
specialize pp with (1 := H2).

(* or *)
specialize pp with (1 := H1) (2 := H2).
Li-yao Xia
  • 31,896
  • 2
  • 33
  • 56
  • 3
    Or `specialize (f_equal2_mult _ _ _ _ H1 H2).`, or `pose proof (f_equal2_mult _ _ _ _ H1 H2).` – eponier Nov 05 '18 at 11:16
  • What about the case where it is an iff relation (<->)? e.g. apply Nat.mul_cancel_r to `H1: n<>0` and `H2: a*n=b*n` ? – Jeremy Salwen Nov 06 '18 at 01:14
  • If you have `H : P <-> Q` in the context, you can use `apply proj1 in H` to convert it to `H : P -> Q`. – Li-yao Xia Nov 06 '18 at 05:24
  • Combining proj1 with post proof, I was able to get the one-liner `pose proof (proj1 (Nat.mul_cancel_r _ _ _ H1)) H2` for the bidirectional case. – Jeremy Salwen Nov 07 '18 at 20:51