Stream: Coq users

Topic: in apply, discharge non-unifiable terms through equalities?

Jonas Oberhauser (Jul 30 2020 at 12:22):

Is there a variant of apply which can discharge non-unifiable terms through equalities? E.g.,

old state:
x, z : nat ; H : forall y, P x 5 y |- P z 5 z
awesome_apply H.
new state:
x, z : nat ; H : P x |- x = z

Simon Hudon (Jul 30 2020 at 18:36):

I haven't seen it in Coq but I've written a similar one in Lean. I can help you write awesome_apply. By the way, great naming there :)

Enrico Tassi (Jul 30 2020 at 21:11):

SSReflect's congr tactic does something like this

Jean-Christophe Léchenet (Aug 03 2020 at 12:27):

The file LibTactics.v distributed in Software Foundations defines a tactic called applys_eq that does this kind of thing, but you must manually specify the variables that should give an equation. In your case, this would give applys_eq H 1 3 (the variables are counted from the right).

Last updated: Sep 28 2023 at 11:01 UTC