Equal Up to Computation but not "Equal Equal"?

Stream: new members

[Andrew Elsey]

aaatest.lean

Hi, I'm running into an issue I'm quite stuck on. Essentially, I have a dependent type, let's say a Vector, which depends on a Coordinate Frame. I can create two Coordinate Frames which are unintentionally equal up to computation, but not "equal equal". Then, I can create two Vectors using the frames which are equal up to computation, but not "equal equal". Next, an operation on Vectors, say, adding two Vectors together, which requires their Coordinate Frame to be the same will fail because of the dependent type.

I am wondering if there's any way in Lean to work around this. If the dependent type values are equal up to computation, I want the type check to succeed.

I attached code, my full solution might be a bit too long but hopefully it is clear. If the code or what I'm describing is not clear, please let me know. Greatly appreciate any ideas here.

[Johan Commelin]

@Andrew Elsey Hi, and welcome! See the recent discussion at:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/reducing.20the.20index.20of.20a.20type/near/218262370

[Johan Commelin]

This is an annoying and common downside of dependent type theory.

[Reid Barton]

I'm not sure if this is the same issue... but it's hard to understand what's going on because there is a lot of guesswork

[Reid Barton]

As far as I can tell, it is just a type class issue

[Reid Barton]

It's hard to understand though because you omit the types of things from defs, and there are pieces missing. But I think what you are finding is that instance search doesn't reduce ordinary definitions, so definitionally equal types can have different instances on them.

[Reid Barton]

(Or, more to the point, an instance might exist for T but not for T' even though T and T' are definitionally equal.)

[Andrew Elsey]

Thanks Johan. I was wondering if quotient types could help me but I wasn't sure how to go about it. It looks like the suggestions are along that vein. Hi Reid, thank you, Yes, I think that's exactly right, the type class instance relies on the dependent type value, which is why it can't find the instance, and when they are "equivalent" with reductions, whatever the term is, I need it to use the same instance. Sorry if the code is not clear, I will try to edit a bit better - didn't want to send 500 lines.

[Reid Barton]

It seems that instance search knows the type of base_vec1 is whatever aff_fr.aff_coord_vec ℝ 1 (affine_coord_frame.base_frame (aff_fr.affine_coord_frame.derived ...)) is, so you can add a has_vadd instance for this pair of types.

[Andrew Elsey]

The expression is ab it nasty looking, but that instance is "there". Sorry, I should try to edit the code a bit better. All of the Frames get subsumed under: "instance : has_vadd (aff_coord_vec K n fr) (aff_coord_pt K n fr) := ⟨aff_group_action_coord K n fr⟩". K is a field, n is dimension, fr is a an "affine_coordinate_frame"

I think you have a relevant post here linked by Johan: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/heq.20alternative/near/210378589

[Reid Barton]

aff_coord_pt is completely different from aff_coord_vec, because they are different structures

[Reid Barton]

(I'm also confused why you're using has_vadd for this, maybe relatedly?)

[Andrew Elsey]

Doh.... instance aff_semimod_coord : semimodule K (aff_coord_vec K n fr) is the action for aff_coord_vec.

However, "has_vadd.vadd vec1 vec2" seems to type check just fine. I am not sure where this occurs but possibly because it is an affine space, too
instance afc : affine_space
(aff_coord_vec K n fr)
(aff_coord_pt K n fr) :=
prf K n fr
affine_space is just an alias for add_torsor, I believe

I'll try to post my full files if I can

[Andrew Elsey]

Not sure if it helps, but I got a thumbs up to post full code.

(Mostly all of) The relevant code is in here:
https://github.com/kevinsullivan/affine_lib/blob/master/affine/affine_coordinate_framed_space_update.lean
https://github.com/kevinsullivan/affine_lib/blob/master/affine/affine_coordinate_framed_space_update_lib.lean
With the type issue demonstrated on lines 146-186 here:
https://github.com/kevinsullivan/affine_lib/blob/master/affine/affine_coordinate_framed_space_update_test.lean

[Kevin Sullivan]

Andrew Elsey said:

Doh.... instance aff_semimod_coord : semimodule K (aff_coord_vec K n fr) is the action for aff_coord_vec.

However, "has_vadd.vadd vec1 vec2" seems to type check just fine. I am not sure where this occurs but possibly because it is an affine space, too
instance afc : affine_space
(aff_coord_vec K n fr)
(aff_coord_pt K n fr) :=
prf K n fr
affine_space is just an alias for add_torsor, I believe

I'll try to post my full files if I can

Thanks, Andrew, and Reid and Johan. Just as some context, this work is part of a US NSF research project at the University of Virginia in which we're, among other things, formalizing aspects of mathematical physics to establish a semantic domain for cyber-physical systems software. We had originally (last summer) written our own affine_space library on which what Andrew is doing was based. Then along came an affine_space contribution to mathlib, so we just ported what we'd built to that underlying library. We'd be happy to see what we're trying to produce here -- an affine coordinate space library -- be of use to the broader community as well. I've made our repo public: https://github.com/kevinsullivan/affine_lib. If it seems appropriate and useful at some point, we'd be glad to contribute a future version of this work to the Lean community.

[Andrew Elsey]

Turns out "[reducible]" is very useful...

[Yakov Pechersky]

You might want to say

local notation `R3_pt1` := aff_lib.affine_coord_space.mk_point R3 ⟨[0,0,0], rfl⟩

and that way you don't even have to undo a def R3_pt1.

[Saroj N]

.