coercions from polynomials

Stream: general

[Kevin Buzzard]

import data.mv_polynomial

open mv_polynomial

variables {k : Type*} [comm_ring k]

variable {n : Type*}

instance : has_coe_to_fun (mv_polynomial n k) :=
{ F := λ f, (n → k) → k,
  coe := λ f x, eval x f}

def 𝕍 (S : set (mv_polynomial n k)) : set (n → k) :=
-- {x : n → k | ∀ s ∈ S, s x = 0} -- doesn't work
-- {x : n → k | ∀ s ∈ S, s.eval x = 0} -- also doesn't work
{x : n → k | ∀ s ∈ S, eval x s = 0} -- works BUT VARIABLES IN STUPID ORDER!

[Kevin Buzzard]

If s is a polynomial and x is some assignment of the variables, I want to write s(x) to be the evaluation of the polynomial at the assignment of the variables. As does every mathematician. Why am I failing in the above?

[Chris Hughes]

eval x is a ring hom. That's why they're in the current order.

[Kevin Buzzard]

I don't understand why s.eval x = 0 fails. Is this an issue with the elaborator?

[Johan Commelin]

It's because of ∀ s ∈ S, I think.

[Johan Commelin]

If you would write ∀ f, f ∈ S → f.eval x = 0, I think it would work

[Johan Commelin]

But of course that is ugly

[Johan Commelin]

At least∀ f : mv_polynomial n k, f ∈ S → f.eval x = 0 should work

[Kevin Buzzard]

If you would write ∀ f, f ∈ S → f.eval x = 0, I think it would work

It doesn't work for me:

import data.mv_polynomial

open mv_polynomial

variables {k : Type*} [comm_ring k]

variable {n : Type*}

instance : has_coe_to_fun (mv_polynomial n k) :=
{ F := λ f, (n → k) → k,
  coe := λ f x, eval x f}

def 𝕍 (S : set (mv_polynomial n k)) : set (n → k) :=
-- {x : n → k | ∀ f, f ∈ S →  f x = 0} -- doesn't work
-- {x : n → k | ∀ f, f ∈ S → f.eval x = 0} -- also doesn't work
-- {x : n → k | ∀ f ∈ S, eval x f = 0} -- works BUT VARIABLES IN STUPID ORDER!
{x : n → k | ∀ f, f ∈ S → eval x f = 0} -- works BUT VARIABLES IN STUPID ORDER!

[Reid Barton]

oh yeah, inference with has_mem is super annoying

[Mario Carneiro]

When using "forall in" so that I can't write the type, I usually do something like this:

 {x : n → k | ∀ f ∈ S, (f : mv_polynomial n k).eval x = 0}

[Johan Commelin]

:thumbs_up: But it is still 3.1415 miles away from what mathematicians would write...

[Johan Commelin]

Are there examples of has_mem X Y in mathlib where X is not uniquely determined by Y? More precisely, can someone point me to two instances with types has_mem X_1 Y and has_mem X_2 Y such that X_1 differs from X_2?

[Johan Commelin]

(The dual case is clear: has_mem X (set X) and has_mem X (finset X), etc... all exist and are desirable.)

[Reid Barton]

X is an out_param so I think the case you suggest is not supposed to happen, but I never really understood whether out_param behaves like I would expect from Haskell

[Reid Barton]

Like here we definitely know that S : set (mv_polynomial n k), so there should be no problem inferring f : mv_polynomial n k and yet here we are

[Johan Commelin]

class has_mem' (Y : Type u) :=
(T : Type u)
(mem : T → Y → Prop)

[Reid Barton]

Also I think it would be better if ∈ was not overloaded at all, but only had type a -> set a -> Prop. The other cases you refer to could be handled using coercions.

[Reid Barton]

after all, a set S is exactly determined by its membership predicate so there is no loss of information this way

[Johan Commelin]

Also I think it would be better if ∈ was not overloaded at all, but only had type a -> set a -> Prop. The other cases you refer to could be handled using coercions.

But you run the risk that you have to explicitly tell Lean that you want to coerce...

[Johan Commelin]

Suppose I write ∀ f ∈ S, and S : finset X. Then Lean doesn't know the type of f yet. It will want to coerce S to set m_1?, but probably isn't smart enough to figure out that finset X only coerces to set X.

[Reid Barton]

oh this might be an issue, yes, but isn't that already broken?

[Johan Commelin]

So you end up writing ∀ f ∈ (S : set (mv_polynomial k n)), which is what we want to avoid.

[Reid Barton]

Anyways that's the same as the coercion to function issue which will hopefully be fixed in :four_leaf_clover:

[Johan Commelin]

Well, not if you allow multiple has_mems, I think

[Johan Commelin]

What do you think of my has_mem'?

[Johan Commelin]

It's probably broken as well... I dunno

[Reid Barton]

I think this encoding might get annoying in practice because Lean will naturally synthesize a type like (@set.has_mem a).T and then it will need to be reduced to a and it might not happen automatically in the right places

[Reid Barton]

Other than that, I think it would work

[Johan Commelin]

I think the problem with out_param was that it kicks in too late. My version would hopefully kick in at the right time

[Patrick Massot]

Do whatever you want as long as we don't loose sets being members of a filter.

[Johan Commelin]

Patrick, as long as nothing else can be member of a filter, that should be fine.

[Johan Commelin]

I wish we could register lookup tables in the parser and/or elaborator. Where you say: Oh, you've got ∀ f ∈ S? Figure out the type of S, and I'll look in the table what the type of f must be.

[Johan Commelin]

But that is a very ad hoc thing to do, I guess

[Patrick Massot]

Isn't it covered by unification hints?

[Johan Commelin]

Je ne sais pas

[Patrick Massot]

I don't know either, I'm only trolling.