Definitional equality

Stream: Is there code for X?

[Robert Maxton]

Is there a non-meta version of is_def_eq or the like? My specific use case would be being able to decidably conclude that, say, [a, b, c] = [a, b, c] even if a,b,c are of a type without decidable equality... though I may be misunderstanding the entire notion of "decidability" then

[Robert Maxton]

Well, more specifically, I want to write code to take a symbolic list, partition it into disjoint pieces, and conclude that certain operations (like sum) are equivalent if taken over the original list or if combined from the disjoint pieces

and to do this whether or not I'm working on a type with decidable equality, purely on the basis of reflexivity

[Robert Maxton]

and I suppose that could be a tactic, but it feels like it could also be a lemma...

[Patrick Massot]

rfl?

[Damiano Testa]

If rfl does not work, maybe you could try to get congr to break up the proofs?

[Robert Maxton]

mmm
maybe
the other thing I want to do is to filter a list for things that are defeq to the input -- again, working on the basis of "same symbol" rather than "same value"

[Robert Maxton]

mm, maybe I can just include that in the assumptions and let the 'end user' provide a proof that the join of the lists are the same as the original list...? (up to permutation)

[Robert Maxton]

(I would use multiset for this, except multiset seems to have even less in the way of filtering...?)

[Eric Wieser]

(docs#multiset.filter?)

[Robert Maxton]

requires decidable_pred, which gets back to "how can I use definitional equality within a lemma"
mind you I don't really see a great way of using list to filter without also running into decidability issues, but at least it isn't part of the interface...?

[Robert Maxton]

it's a shame we don't have something like javascript's ===

[Robert Maxton]

oh, wait, docs#multiset.filter_map has exactly the same requirements as the list theorem I was looking at

[Robert Maxton]

so okay, I'll probably go back to multisets

[Robert Maxton]

but problem regarding defeq stands

[Eric Rodriguez]

Robert Maxton said:

it's a shame we don't have something like javascript's ===

docs#heq

[Robert Maxton]

isn't that the opposite of what we want? I want something that checks for equality at the unification/symbolic level; this seems like it tries to make equality work even when unification fails...?

[Eric Wieser]

I want to write code to take a symbolic list,

Are you sure you don't want to do this in meta land?

[Eric Wieser]

Can you maybe give a longer explanation of what you're trying to do, preferably with some pseudo-code?

[Eric Rodriguez]

I mean, JS === is just false if they have different types instead of not typechecking, just like heq.

[Robert Maxton]

I'm not at all sure I don't want to do this in meta land, in fact! but it seems like the sort of thing that would also need a lemma that says "and after I do this symbolic level manipulation I do in fact get an equivalent expression at the end"

[Robert Maxton]

Eric Rodriguez said:

I mean, JS === is just false if they have different types instead of not typechecking, just like heq.

the relevant thing is that I want, say, a===a because of symbolic level reflexivity, rather than requiring that a have a type that has decidable equality (so, e.g. not being real or complex)

[Robert Maxton]

Eric Wieser said:

Can you maybe give a longer explanation of what you're trying to do, preferably with some pseudo-code?

Basically, this is ultimately going into a mathematica-style "collect and un-distribute like terms" lemma/tactic

[Eric Wieser]

"symbolic level reflexivity" is a stronger notion than definitional equality

[Eric Wieser]

n + 0 = n definitionally (for n : nat), but not symbolically. Symbolic level reflexivity is equality of docs#expr

[Eric Wieser]

Basically, this is ultimately going into a mathematica-style "collect and un-distribute like terms" lemma/tactic

That very much sounds like a job for a tactic, where you'll be working with exprs

[Robert Maxton]

so that, say, a•r + b•s + c•r + d•s + e•s + f•r becomes (a + c + f)•r + (b + d + e)•s

[Eric Wieser]

(note that expr has decidable equality)

[Robert Maxton]

hmmm, okay

[Robert Maxton]

alright, I'll start there then

[Eric Wieser]

Typically the approach is to oush around the symbols, and then build up a proof term programmatically that shows the shuffling was allowed.

If you're not aware, there's a #metaprogramming / tactics stream that can be helpful for questions about this kind of thing

[Robert Maxton]

I was not! Thanks!

[Damiano Testa]

I have very recently started meta-programming myself and got involved in a similar project: in my case, I wanted to prove terms in a sum can be moved around to produce the same sum. Working at the meta-level gives you quick access to formulating the equality that you want. After that, you set up the goal (similar to a have where you supply the end-result by unchecked meta code) and you use some version of simp [add_smul, add_comm, add_assoc, add_left_comm] to check that the meta-code happened to produce the correct final result.

[Damiano Testa]

If you want to look at the project in which I was involved, it is not in mathlib, but it is #13483.

[Violeta Hernández]

I for one am glad that we don't have a predicate for definitional equality

[Violeta Hernández]

The whole point of equality as a concept is that when two things are equal, they share every single possible property imaginable

[Violeta Hernández]

Distinguishing definitional equality would break this

[Violeta Hernández]

Not to mention, definitional equality will change in Lean 4! Eta reduction isn't currently definitional but will be