(2, 3, 5).3

Stream: Is there code for X?

[Kenny Lau]

so i was too bored so i made f.3 work where f : Nat × Nat × Nat (the title is clickbait because it doesn't actually work with explicit Prod.mk, which i deemed there is no point in making it work because you would just write 5)

import Lean.MetavarContext
import Mathlib.Init

open Lean Meta Elab Term

-- this will fail for say (2, 3, 5, 7).4 because at that point there is no point
elab t:term"."n:num : term => do
  have n := n.getNat
  let t ← elabTerm t none
  let e ← inferType t
  let mut curr := e
  let mut s := 1
  while true do
    let m₁ ← mkFreshExprMVar none
    let m₂ ← mkFreshExprMVar none
    let u₁ ← mkFreshLevelMVar
    let u₂ ← mkFreshLevelMVar
    if ← isDefEq (mkApp2 (mkConst ``Prod [u₁, u₂]) m₁ m₂) curr then
      let .some c' ← getExprMVarAssignment? m₂.mvarId! | break
      curr := c'
      s := s + 1
    else break
  if s < 2 ∨ s < n then throwUnsupportedSyntax
  have e₁ : Expr := (n - 1).rec t fun _ ih ↦ .proj ``Prod 1 ih
  have e₂ := if s = n then e₁ else .proj ``Prod 0 e₁
  return e₂

variable (f : Nat × Nat × Nat)

#check f.3

def foo := Nat × Nat × Nat

variable (g : foo)

#check g.1
#check g.2
#check g.3

[Kenny Lau]

and this implementation has the flaw that it makes g.1 and g.2 ambiguous (the first one is avoidable)

[Kenny Lau]

the second one can be worked-around by putting (g.2 : Nat)

[Kenny Lau]

or it can be fixed by changing the syntax to say g.get2

[Kenny Lau]

or some special hardcoding that only changes the syntax for g.2 (it's unfair to change the rest just to fit g.2)

[Aaron Liu]

I did this too

[Aaron Liu]

let me find it real quick

[Kenny Lau]

what was your solution to g.2?

[Kenny Lau]

aha i can change the syntax to g.%2

[Kenny Lau]

i think this is good

[Aaron Liu]

https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/thoughts.20on.20elliptic.20curves/near/502148036

[Aaron Liu]

Kenny Lau said:

what was your solution to g.2?

no solution, unfortunately

[Kenny Lau]

ah your solution was g..2

[Kenny Lau]

@Damiano Testa on Aaron's linked thread you mentioned that it's not a good idea, and then if I click your link I see Mario's justification of this opinion that x.3 can mean both x.2.1 and x.2.2, which does not apply in this case; do you still hold this belief that this is bad in general?

[Aaron Liu]

The problem now is that x.2 can mean either x.2 or x.2.1 and this is the problem I have no good solution to

[Kenny Lau]

right, that's also a headache for me

[Kenny Lau]

my current workarounds would be either

1. just disable this, only allow .$n for n>2
2. or create special syntax just for 2, such as .%2 (but keep .3)
3. or make special syntax in general, such as .%2 and .%3

[Kenny Lau]

but i don't think this .2 issue should just overrule the other .3 .4 .5 that would be useful

[Aaron Liu]

but now x.3 can mean x.2.2 or x.2.2.1

[Aaron Liu]

this isn't just a problem with 2

[Kenny Lau]

i don't see why this is a problem, it means different things depending on the type of x

[Kenny Lau]

unless we follow my polyvariable approach and enable say .x .y .z for "this file locally"

[Kenny Lau]

enable_prod_notation x y z

[Aaron Liu]

Kenny Lau said:

i don't see why this is a problem, it means different things depending on the type of x

It means specializing a free variable can change the meaning of the numbers

[Kenny Lau]

i see, that's a good point, but i think enable_prod_notation would solve this? at least for the elliptic curve case

[Aaron Liu]

oh I was thinking about more generality than just prod

[Kenny Lau]

i am aware of the limitations and have deliberately restricted to just Prod

[Aaron Liu]

if it's just prod and you already know how long it is it shouldn't be a problem

[Kenny Lau]

@Kim Morrison if you're here, i think you'd be interested in this thread, what's your opinion in using some sort of notation to hide away the x.2.2.2.1 thing that appears when one works with iterated Prod types?

[Kenny Lau]

https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4%20%22.2.2%22&type=code

[Kenny Lau]

maybe the real usecase is actually \and statements

[Kenny Lau]

image.png

[Kim Morrison]

I have been biting my tongue in this thread, as what I want to say is: "Kenny, you are so great at formalizing mathematics, please go and do that instead of introducing fragile and unhelpful notation, that fragments the ecosystem and increases maintenance burden."

[Kenny Lau]

i think one could make a very strong case for replacing these with .%3 and .%4...

[Kim Morrison]

i.e. I personally think this would be a net negative, even before counting the opportunity cost of you doing something useful. :-)

[Kenny Lau]

Kim Morrison said:

fragile

what if ... .%3 always elaborates to .2.2.1 and .%%3 will take the place of .2.2

[Damiano Testa]

Personally, I think that if you want .3 to work, then you should define your type to have (at least) 3 fields and let the third one by the one that you want to call .3.

Touching the way .n works, in the best of cases, leads to not being sure of what projection you are getting.