Equalities which are “the wrong way round” involving boun...

Stream: Is there code for X?

[Will Fourie]

Hi all, this is a problem that has come up a few times and has resulted in what feels like unnecessary work.

I will have a goal of the form, say, $∃(x:A),…(c(x)=t)$ where $t$ may or may not have bound variables as well. I will have a term of type $∃(x:A),…(t=c(x))$.

Lean will not accept that that term means I have proved the theorem, which means I have to unwind it all, seemingly unnecessarily. I cannot use rw because $x$ is bound. I can’t seem to get simp_rw to work either, but maybe I am not feeding it the right type of theorem.

What is the generic solution to this problem?

[Will Fourie]

Or rather, is there a generic solution to this problem?

[Yaël Dillies]

simpa only [eq_comm] using your_proof_term

[Floris van Doorn]

simp_rw [@eq_comm _ _ t] or simp_rw [@eq_comm _ t] at your_proof_term might also be useful intermediate steps.

[Floris van Doorn]

When writing this, you can use _ for the bound variables in t. You just have to specify one of the arguments of eq_comm enough so that it matches with t, but not with c(x) (or the other way around).

[Will Fourie]

I suspected this was just me not knowing how to use the tactic properly. Thanks so much, both of you :tada:

[Eric Wieser]

Should eq_comm take explicit arguments?

[Floris van Doorn]

I think there is a whole bunch of basic propositional/predicate logic iffs that could use more explicit arguments. Examples:
docs#and.left_comm
docs#imp.swap
I think explicit arguments are useful if the lemma might match multiple times, but you only want to rewrite some of them. An example of where I don't think the explicit argument is useful is docs#or_true, since I will want to rewrite all of them anyway (though I don't mind that the argument is explicit in this case).

[Yaël Dillies]

The case for implicit arguments on iffs is less valid here, because we usually have one way lemmas with dot notation. So the only use for implicit arguments would be using in conjunction with iff.trans or similar, which is much rarer.