unexpected reference to subobject field

Stream: general

[Christian K]

Hello,
take a look at this (extremely contrived) MWE:

import Mathlib

structure Test1 where
  field : ℕ

structure Test2 extends Test1 where
  new_field : ℕ
  toTest1 := new_field

#check Test2.mk

I have a structure Test1 with some field. My new struture Test2 extends Test1 with some other field (which determines the field of Test1). I want to set Test1.field = new_field for every instance of Test2., but with this code I get the error: unexpected reference to subobject field 'Test1'. What am I doing wrong here? (Or is my goal fundamentally wrong?)

[Edward van de Meent]

two things: if you use the := notation inside a structure definition, you're only providing a default value. second thing: if you want to specify the default for the original structure, use field := new_field

[Christian K]

Ohh ok, that makes sense. Am I able to force the value of field to be new_field for every instance of Test2 (without adding h : field = new_field to Test2)?

[Edward van de Meent]

yes, if you don't change the name of the field.

[Christian K]

I don't think I fully understand this yet...

structure Test2 extends Test1 where
  new_field : ℕ
  field := new_field

#check Test2.mk

Test2.mk looks like this: Test2.mk (toTest1 : Test1) (new_field : ℕ) : Test2
Why does it still an instance of Test1 (even though I assigned field:=new_field)?

[Edward van de Meent]

because, like i said, it is only a default value.

def f : Test2 where
  field := 0
  new_field := 2
#eval f.field -- 0
#eval f.new_field -- 2

def g : Test2 where
  new_field := 2
#eval g.field -- 2
#eval g.new_field -- 2

[Christian K]

Ahh, ok, I get it now. So would have to do something like this if i want to force field = new_field for every Test2 (or is there a better way?):

structure Test2 extends Test1 where
  new_field : ℕ
  field := new_field
  h : field = new_field

def Test2.mk' (n : ℕ) : Test2 where
  new_field := n
  h := (by rfl)

[Edward van de Meent]

in order to not have this be an issue, you could define it as:

namespace Option1
structure Test2 extends Test1
protected def Test2.new_field (t:Test2) := t.field
end Option1

namespace Option2
structure Test2 where
  new_field : ℕ
protected def Test2.toTest1 (t:Test2) : Test1 := Test1.mk t.new_field
end Option2

[Edward van de Meent]

what is your use case, btw?

[Christian K]

I have defined Sublocals on a Local E as a structure (= Test1). (The sublocal structure contains the corresponding Nucleus). Now I want to define a new structure for the open sublocals on E (= Test 2). These Open sublocals correspond exactly to the elements of E (so they get a new_field with their corresponding element). But this element e completely determines the Nucleus of the Open sublocal, so it has to be equal to some function of e.

[Christian K]

Thank you for your responses btw, I think the second one is the most suitable for my usecase.

[Edward van de Meent]

is it complicated to compute the element e from the other fields? if not, that can just be a custom projection...

[Edward van de Meent]

i.e. use a variant of option 1

[Christian K]

I don't know of a way to compute the element ´e´ from a nucleus, I don't think it is possible. (It would make things a lot easier though...)