default values problem

Stream: lean4

[Yiming Fu]

Hi everyone,
If I have a dependent constructor that provides a default value in a structure or class, I want to extend it while preserving the default value. How should I manage this? Additionally, can I control which constructors use default values when I provide a structure or class?

structure simple where
  a : ℕ
  b : ℕ
  u : Prop := a + b = 0

structure simple₁ extends simple where
  c : ℕ
  d : ℕ

example (p : simple) (p1 : simple₁) : p.u = p1.u := by
  unfold simple.u simple₁.tosimple
  sorry
  -- This cannot be proved
  -- possibly because Lean doesn't know the values for `p.u` and `p1.u`

example (p : simple) (p1 : simple₁) : p.u ≠ p1.u := by
  -- I want `p` to not use the default value, but I want `p1` to use the default value
  sorry

[Robin Arnez]

It preserves the default value? But I probably don't quite know what you want to achieve

structure simple where
  a : Nat
  b : Nat
  u : Prop := a + b = 0

structure simple₁ extends simple where
  c : Nat
  d : Nat

example : { a := 1, b := 2, c := 3, d := 4 : simple₁ }.u = (1 + 2 = 0) := rfl

[Yiming Fu]

Sorry. What I want is the following: if I don't provide data for the structures, I only supply two abstract variables. How should I manage how they use default values in this case?

[Robin Arnez]

Hmm, do you mean something like:

example (x : simple) (h : x.u = (x.a + x.b = 0)) : True := by
  sorry

[Robin Arnez]

Default values only matter for constructors though

[Robin Arnez]

So if you're just taking them as arguments, you could just as well have omitted the default value

[Yiming Fu]

Yes, that’s exactly what I meant. Thanks for your help! I understand that this approach works. It seems there’s no way to control how default values are used outside of constructors.

[Kyle Miller]

Default values are just default values, and they're not really part of the logical specification of the structure. Think of them as being a convenience. It seems like you're possibly wanting a feature like

structure simple where
  a : ℕ
  b : ℕ
  let u : Prop := a + b = 0

that actually specifies that u is the sum of a and b? That feature does not exist, but you can simulate it using a separate definition:

structure simple where
  a : ℕ
  b : ℕ

def simple.u (s : simple) : Prop :=
  s.a + s.b = 0

That said, your first example still can't be proved. It's

example (p : simple) (p1 : simple₁) : p.u = p1.u := by
  unfold simple.u simple₁.tosimple
  /-
  p : simple
  p1 : simple₁
  ⊢ (p.a + p.b = 0) = (p1.1.a + p1.1.b = 0)
  -/
  sorry

but there's no reason for the truth of these two propositions to be related. They depend on the values of a and b for p and p1.

[Kyle Miller]

Or maybe you somehow want u to be fixed in the child structure? It's possible in a roundabout way, but I don't see why you would want this, and also the example is still not provable, even if both variables are simple₁, since it depends on the values of a and b for the two structures.

structure simple (useDefault := false) where
  a : ℕ
  b : ℕ
  u : Prop := a + b = 0
  hu : if useDefault then u = (a + b = 0) else True := by exact trivial

structure simple₁ extends simple (useDefault := true) where
  c : ℕ
  d : ℕ

example (p : simple₁) (p' : simple₁) : p.u = p'.u := by
  rw [p.hu, p'.hu]
  /-
  p p' : simple₁
  ⊢ (p.a + p.b = 0) = (p'.a + p'.b = 0)
  -/
  sorry

[Yiming Fu]

Kyle Miller said:

Or maybe you somehow want u to be fixed in the child structure? It's possible in a roundabout way, but I don't see why you would want this, and also the example is still not provable, even if both variables are simple₁, since it depends on the values of a and b for the two structures.

structure simple (useDefault := false) where
  a : ℕ
  b : ℕ
  u : Prop := a + b = 0
  hu : if useDefault then u = (a + b = 0) else True := by exact trivial

structure simple₁ extends simple (useDefault := true) where
  c : ℕ
  d : ℕ

example (p : simple₁) (p' : simple₁) : p.u = p'.u := by
  rw [p.hu, p'.hu]
  /-
  p p' : simple₁
  ⊢ (p.a + p.b = 0) = (p'.a + p'.b = 0)
  -/
  sorry

Thanks for the clarification! I realize that I gave an example that shouldn't be provable unless I provide values for a and b. Sorry for the confusion :confounded: . My original goal is more aligned with the quoted message. I want to know if there's an option to control whether I use "default values" like this:

structure simple (useDefault := false) where
  a : ℕ
  b : ℕ
  u : Prop
  hu : if useDefault then u = (a + b = 0) else true

structure simple₁ extends simple (useDefault := true) where
  c : ℕ
  d : ℕ

example (p : simple₁)
-- can I control (useDefault = true or false) here?
-- something like `p : simple₁ (useDefault := _)`
    : p.u = (p.a + p.b = 0) := by
  rw [p.hu]

example (p : simple) : p.u = (p.a + p.b = 0) := by
  sorry
  /- p : simple
  ⊢ p.u false = (p.a false + p.b false = 0) -- not provable without value of `p.u`
  -/