Zulip Chat Archive

Stream: general

Topic: Defining inverse as a partial function.


view this post on Zulip Edward Ayers (Nov 01 2018 at 11:08):

I am investigating defining field inverses so that you have to also give the inverse a certificate that the number being put in is not zero. We can have a separate debate about whether that approach is better than having inv(0) = 0, but for now here are my ideas:

My first idea was to treat the 'non-zeroness' as a typeclass then piggyback on the type inference algorithm.

    universe u
    class not_zero {R : Type u} [ring R] (x : R) := (nz : x  0)
    class my_division_ring (R : Type u) extends (ring R) :=
    (inv(x:R) [not_zero x]:  R)
    (inv_l : Π (y : R) [not_zero y], y * (inv y)  = 1 )
    (inv_r : Π (y : R) [not_zero y], (inv y) * y  = 1 )

Sadly, I get a "failed to synthesize typeclass" error.
Even more sadly, the last two lines of the error read:

_inst_1 : not_zero y
 not_zero y

Why is the elaborator not spotting this? This seems like something the elaborator would be able to do. Supposing that the elaborator could do this, then my idea was that you could write things like:

instance {R : Type u} [integral_domain R] {x y : R} [not_zero x] [not_zero y] : not_zero (x * y) := ...

Are there any roadblocks that are stopping this dream from being a feasible way of defining the inverse function?

view this post on Zulip Johan Commelin (Nov 01 2018 at 11:10):

Can this be solved with the haveI magic inserting the instance into the type class system at the right points?

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:12):

My second approach was to use auto_params:

    -- eventually a sophisticated tactic that figures out if an elt is ≠ 0
    meta def nz_tactic := tactic.assumption
    class dvr (R : Type u) extends (ring R) :=
    (inv(x:R) (p:x  0):  R)
    (inv_l : Π (x y : R) (p:y0), x * (inv y p)  = 1 )
    variables {R : Type u} [dvr R]
    def inv (y : R) (nz : y  0 . nz_tactic) : R := dvr.inv y nz

    def div (x y : R) (nz : y  0 . nz_tactic) : R := x * (inv y)
    infix ` /. `:50 := div

    variables {x y : R}
    variable (xz : x  0 . nz_tactic) -- I was really hoping that this would be allowed

    example (x y : R) (xz : x  0) (yz : y  0) : (1 /. (x * y)) = (1 /. x) * (1 /. y) := sorry

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:12):

Can this be solved with the haveI magic inserting the instance into the type class system at the right points?

I don't understand what this means.

view this post on Zulip Johan Commelin (Nov 01 2018 at 11:12):

Neither do I.

view this post on Zulip Johan Commelin (Nov 01 2018 at 11:13):

The point is that the problem you described pops up quite often.

view this post on Zulip Johan Commelin (Nov 01 2018 at 11:13):

And then you can write haveI my_instance, blah and then the type class system will pick up your instance.

view this post on Zulip Johan Commelin (Nov 01 2018 at 11:13):

And the reason you have to do this explicitly is because Lean 3.4.x is pretty frozen.

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:15):

Please could you give a full example of haveI?

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:15):

I get [Lean] unknown identifier 'haveI' errors

view this post on Zulip Johan Commelin (Nov 01 2018 at 11:15):

I'll try. For starters, here are 56 examples: https://github.com/leanprover/mathlib/search?q=haveI&unscoped_q=haveI

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:16):

ah it's a tactic

view this post on Zulip Johan Commelin (Nov 01 2018 at 11:16):

Yes, and it has some friends, like exactI and I don't know what they do, and how they differ.

view this post on Zulip Johan Commelin (Nov 01 2018 at 11:16):

I'm using them cargo-cult style.

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:19):

So my question now is: Is there a fundamental reason why the elaborator can't do my above example? Eg there might be cases where it causes the elaborator to take unbounded time or something.

view this post on Zulip Johan Commelin (Nov 01 2018 at 11:20):

I think the fundamental reason was that Lean 3.4.x is frozen.

view this post on Zulip Johan Commelin (Nov 01 2018 at 11:21):

Also, in your inv_l and inv_r you want y = x.

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:24):

That's not what I mean by reason. Why would the elaborator be able to do the below example but not the one at the top.

def sq {R : Type u} [ring R] (a : R) :=  a * a

It must be something to do with the fact that the elaborator is looking for typeclasses attached to the type of a and not to a itself.

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:24):

Also, in your inv_l and inv_r you want y = x.

fixed!

view this post on Zulip Chris Hughes (Nov 01 2018 at 11:33):

I think it;s actually to do with being left or right of the colon. This doesn't work

example {R : Type*} : Π [ring R] (a : R), a * a = 1 :=

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:52):

(inv_l (x : R) [not_zero x] : (x * (inv x) = 1) ) has the same error though.

view this post on Zulip Chris Hughes (Nov 01 2018 at 11:56):

Maybe because it's part of a structure. Does the ring example work as part of a structure?

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:58):

This works:

    variables {R : Type u} [my_division_ring R]
    def inv (y : R) [not_zero y] : R := my_division_ring.inv y

view this post on Zulip Edward Ayers (Nov 01 2018 at 11:58):

so maybe it is because it is part of a structure.

view this post on Zulip Reid Barton (Nov 01 2018 at 12:55):

by exactI is the most succinct option here

view this post on Zulip Edward Ayers (Nov 01 2018 at 13:40):

Right but ideally I wouldn't even have to use a tactic.

view this post on Zulip Edward Ayers (Nov 01 2018 at 13:40):

The elaborator would just do it.

view this post on Zulip Edward Ayers (Nov 01 2018 at 14:07):

I think that I've got the elaborator to "just do it" now:

    class not_zero {R : Type u} [ring R] (x : R) := (nz:x  0)
    class my_division_ring (R : Type u) extends (integral_domain R) :=
    (inv : Π(x:R) [not_zero x],  R)
    (inv_l (x : R) [nz:not_zero x] : x * (@inv x nz)  = 1 )
    (inv_r : Π (x : R) [nz:not_zero x] , (@inv x nz) * x  = 1 )

    variables {R : Type u} [my_division_ring R]
    def inv (y : R) [not_zero y] : R := my_division_ring.inv y

    def div (x y : R) [not_zero y] : R := x * (inv y)
    infix ` ÷ `:50 := div

    variables {x y : R} [not_zero x] [not_zero y]
    instance : not_zero (x * y) := mul_ne_zero (not_zero.nz x) (not_zero.nz y)

    example : (1 ÷ (x * y)) = (1 ÷ x) * (1 ÷ y) := sorry

view this post on Zulip Edward Ayers (Nov 01 2018 at 14:08):

So I was badmouthing the elaborator but I only have to be explicit with inv within the class definition.

view this post on Zulip Edward Ayers (Nov 01 2018 at 14:09):

I much prefer this approach to making the inverse total.

view this post on Zulip Edward Ayers (Nov 01 2018 at 14:11):

But it has its own caveats

view this post on Zulip Floris van Doorn (Nov 01 2018 at 14:17):

One problem you'll run into is that sooner or later type class inference is not going to figure out that arguments are not_zero, because the reasons get too complicated. But if you're fine with writing

haveI : not_zero t := ...,

here and there, it should be fine.

view this post on Zulip Edward Ayers (Nov 01 2018 at 14:34):

Right. The problem is that the reasons get too complicated, so the elaborator would end up needing to be a general purpose prover. It seems to me that in practice, if a function needs an implicit guard proposition like x != 0, it is usually easy for a human to work out where the certificate is coming from, so it should be possible to make a tactic that can also figure it out 80% of the time. It would be so useful if one were able to augment the elaborator with ones own tactics, similar to the (x:P . my_tactic) syntax, but where I don't have to explicitly write out the tactic name all of the time and one can also write variables {x : R} (x != 0 . my_tactic).
I think my ideal syntax would be to extend the typeclass brackets to also take arbitrary propositions.

    class my_division_ring (R : Type u) extends (integral_domain R) :=
    (inv : Π(x:R) [x  0],  R)

    variables {x y : R} [x  0] [y  0]
    instance : (x * y)  0 := mul_ne_zero x  0 y  0

I know that there are lots of practical difficulties that this would surface, but I think the idea makes sense. The meaning of [x ≠ 0] is that this is a fact that needs to be present but which should be hidden from the user as much as possible.

view this post on Zulip Edward Ayers (Nov 01 2018 at 14:40):

You can already pretend that a proposition is a typeclass, but the elaborator doesn't know what to do with them because they don't have the class attribute on them.

view this post on Zulip Simon Hudon (Nov 03 2018 at 13:15):

I think you might consider auto params. It allows you to specify a tactic to use to prove non-zeroness

view this post on Zulip Simon Hudon (Nov 03 2018 at 13:18):

ˋlean
(inv (x : R) (h : x /= 0 . prove_non_zero) : R)
ˋ

view this post on Zulip Simon Hudon (Nov 03 2018 at 13:20):

(Sorry for the bad formatting, I’m on my phone)

view this post on Zulip Reid Barton (Nov 03 2018 at 15:03):

Now I'm confused why this code that I found in Scott's limits branch actually does work:

class preserves_limits (F : C  D) :=
(preserves : Π {J : Type v} [small_category J] {K : J  C} {c : cone K}, is_limit c  is_limit (F.map_cone c))

view this post on Zulip Reid Barton (Nov 03 2018 at 15:04):

J \func C depends on the [small_category J], and if I delete the latter then I get errors.


Last updated: May 14 2021 at 06:16 UTC