Zulip Chat Archive

Stream: new members

Topic: Equal Up to Computation but not "Equal Equal"?


view this post on Zulip Andrew Elsey (Dec 02 2020 at 12:24):

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.

view this post on Zulip Johan Commelin (Dec 02 2020 at 12:32):

@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

view this post on Zulip Johan Commelin (Dec 02 2020 at 12:32):

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

view this post on Zulip Reid Barton (Dec 02 2020 at 12:37):

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

view this post on Zulip Reid Barton (Dec 02 2020 at 12:38):

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

view this post on Zulip Reid Barton (Dec 02 2020 at 12:41):

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.

view this post on Zulip Reid Barton (Dec 02 2020 at 12:46):

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

view this post on Zulip Andrew Elsey (Dec 02 2020 at 12:48):

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.

view this post on Zulip Reid Barton (Dec 02 2020 at 12:55):

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.

view this post on Zulip Andrew Elsey (Dec 02 2020 at 13:03):

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

view this post on Zulip Reid Barton (Dec 02 2020 at 13:07):

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

view this post on Zulip Reid Barton (Dec 02 2020 at 13:07):

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

view this post on Zulip Andrew Elsey (Dec 02 2020 at 13:16):

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

view this post on Zulip Andrew Elsey (Dec 02 2020 at 16:10):

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

view this post on Zulip Kevin Sullivan (Dec 02 2020 at 16:12):

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.

view this post on Zulip Andrew Elsey (Dec 03 2020 at 22:13):

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

view this post on Zulip Yakov Pechersky (Dec 03 2020 at 22:16):

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.

view this post on Zulip Saroj N (Dec 04 2020 at 00:06):

.


Last updated: May 13 2021 at 21:12 UTC