Proof equalities

Stream: mathlib4

[Violeta Hernández]

There's a few other things about Logic.Basic that perplex me

[Violeta Hernández]

What's going on with docs#congr_refl_left and co? Surely a lemma that states two proofs are equal is entirely useless in Lean?

[Violeta Hernández]

And it's not like the proof of these equalities are hiding any interesting mathematical reasoning either, they're all just rfl

[Eric Wieser]

In theory such lemmas are useful for constructing a rfl with the correct LHS and RHS

[Eric Wieser]

Probably these are inherited from Lean 3 core, perhaps where they were used internally by tactics

[Eric Wieser]

Or even from the HoTT mode in Lean 2

[Eric Wieser]

(I think this probably is deserving of its own thread with a better title, feel free to move these last few messages)

[Notification Bot]

7 messages were moved here from #mathlib4 > Decidable namespace by Violeta Hernández.

[Violeta Hernández]

These lemmas were added by @Kim Morrison here: https://github.com/leanprover-community/mathlib3/commit/8b8a5a27094f80607f7ee48c91d3bb899e95342c

[Violeta Hernández]

I don't really understand the reasoning, but I think they might be logical versions of categorical theorems?

[Violeta Hernández]

Also worth mentioning that they were originally tagged simp, but simp doesn't do proof rewrites so they didn't do anything

[Eric Wieser]

Can simp be told to do proof rewrites via an option?

[Eric Wieser]

I think the argument is that these simp lemmas (if applied) let Eq.mpr h reduce, because they convert h into a rfl term.

[Violeta Hernández]

Arguably in most real-world scenarios, if you have h : α = β with α and β def-eq, simp should be able to reduce both to the same expression

[Violeta Hernández]

Though actually! It seems like simp might be able to see through def-eqs like this

[Violeta Hernández]

def id' (x : α) := x

example (x : α) : x = id' x := by simp -- simp doesn't know this!
example (h : α = id' α) (x : α) : x = cast h x := by simp -- still works

[Violeta Hernández]

I really can't see any possible use for these theorems
#20849

[Yakov Pechersky]

Not sure why you claim they aren't useful. They specify the behavior of congr_fun and congr_arg.

[Yakov Pechersky]

And this could be useful in an expression construction metaprogram.

[Violeta Hernández]

Well, these theorems are currently entirely unused. So at the very least they're not useful in current Mathlib.

[Violeta Hernández]

I concede that there might be very niche use cases with Eq.rec and such that warrant equalities between proofs, but maybe we shouldn't go around adding them unless we actually need them

[Eric Wieser]

When you're in DTT hell, the last thing you want is missing lemmas

[Eric Wieser]

Lemmas can be useful even if they never actually end up in proofs committed to mathlib; you might use them while searching for a proof or correcting a statement

[Kent Van Vels]

@Violeta Hernández wrote,

theorems are currently entirely unused.

How do you know that? I am not arguing, I am genuinely curious to know how to know that. Did you comment them out and build mathlib? I am interested to know. Thanks.

[Violeta Hernández]

I made a PR deprecating them, and it builds with no warnings

[Yury G. Kudryashov]

@Eric Wieser Do you have any example of a proof that can actually use a proof-rewriting lemma (one of these or another one)?