don't know how to synthesize placeholder for argument

Stream: lean4

[Marcus Rossel]

I'm running into an error on le_total in the following, which I just don't understand:

import Mathlib.Init.Data.Nat.Lemmas
import Mathlib.Order.Basic

def Time := Nat
deriving LinearOrder

@[ext]
structure Time.Tag where
  time : Time
  microstep : Nat

namespace Time.Tag

instance : LinearOrder Time.Tag where
  le g₁ g₂ := (g₁.time < g₂.time) ∨ (g₁.time = g₂.time ∧ g₁.microstep ≤ g₂.microstep)
  le_refl g := .inr ⟨rfl, le_refl _⟩
  le_trans _ _ _
    | .inl h₁, .inl h₂ => .inl $ h₁.trans h₂
    | .inl h₁, .inr ⟨h₂, _⟩ | .inr ⟨h₂, _⟩, .inl h₁ => .inl $ h₂ ▸ h₁
    | .inr ⟨h₁, h₁'⟩, .inr ⟨h₂, h₂'⟩ => .inr ⟨h₁.trans h₂, h₁'.trans h₂'⟩
  le_antisymm _ _
    | .inl h₁, .inl h₂ => absurd h₁ h₂.asymm
    | .inl h₁, .inr ⟨h₂, _⟩ | .inr ⟨h₂, _⟩, .inl h₁ => absurd (h₂ ▸ h₁) (lt_irrefl _)
    | .inr ⟨h₁, h₁'⟩, .inr ⟨h₂, h₂'⟩ => Time.Tag.ext _ _ (h₁ ▸ h₂) (h₁'.antisymm h₂')
  le_total := sorry -- don't know how to synthesize placeholder for argument 'α'
  decidableLE := sorry -- don't know how to synthesize placeholder for argument 'α'
  decidableEq := sorry

end Time.Tag

If I sorry le_antisymm the error goes away:

instance : LinearOrder Time.Tag where
  le g₁ g₂ := (g₁.time < g₂.time) ∨ (g₁.time = g₂.time ∧ g₁.microstep ≤ g₂.microstep)
  le_refl g := .inr ⟨rfl, le_refl _⟩
  le_trans _ _ _
    | .inl h₁, .inl h₂ => .inl $ h₁.trans h₂
    | .inl h₁, .inr ⟨h₂, _⟩ | .inr ⟨h₂, _⟩, .inl h₁ => .inl $ h₂ ▸ h₁
    | .inr ⟨h₁, h₁'⟩, .inr ⟨h₂, h₂'⟩ => .inr ⟨h₁.trans h₂, h₁'.trans h₂'⟩
  le_antisymm := sorry
  le_total := sorry
  decidableLE := sorry
  decidableEq := sorry

What is this error trying to convey?

[Kevin Buzzard]

I'm still getting the hang of Lean 4 structure constructors so I thought I'd wade in:

import Mathlib.Init.Data.Nat.Lemmas
import Mathlib.Order.Basic

def Time := Nat
deriving LinearOrder

@[ext]
structure Time.Tag where
  time : Time
  microstep : Nat

namespace Time.Tag

instance preorder : Preorder Time.Tag where
  le g₁ g₂ := (g₁.time < g₂.time) ∨ (g₁.time = g₂.time ∧ g₁.microstep ≤ g₂.microstep)
  le_refl g := .inr ⟨rfl, le_refl _⟩
  le_trans _ _ _
    | .inl h₁, .inl h₂ => .inl $ h₁.trans h₂
    | .inl h₁, .inr ⟨h₂, _⟩ | .inr ⟨h₂, _⟩, .inl h₁ => .inl $ h₂ ▸ h₁
    | .inr ⟨h₁, h₁'⟩, .inr ⟨h₂, h₂'⟩ => .inr ⟨h₁.trans h₂, h₁'.trans h₂'⟩

-- works
instance partialOrder : PartialOrder Time.Tag where
  toPreorder := preorder
  le_antisymm _ _
    | .inl h₁, .inl h₂ => absurd h₁ h₂.asymm
    | .inl h₁, .inr ⟨h₂, _⟩ | .inr ⟨h₂, _⟩, .inl h₁ => absurd (h₂ ▸ h₁) (lt_irrefl _)
    | .inr ⟨h₁, h₁'⟩, .inr ⟨h₂, h₂'⟩ => Time.Tag.ext _ _ (h₁ ▸ h₂) (h₁'.antisymm h₂')

-- fails
instance partialOrder' : PartialOrder Time.Tag :=
  { preorder with
    le_antisymm _ _ -- error `expected '}'`
      | .inl h₁, .inl h₂ => absurd h₁ h₂.asymm
      | .inl h₁, .inr ⟨h₂, _⟩ | .inr ⟨h₂, _⟩, .inl h₁ => absurd (h₂ ▸ h₁) (lt_irrefl _)
      | .inr ⟨h₁, h₁'⟩, .inr ⟨h₂, h₂'⟩ => Time.Tag.ext _ _ (h₁ ▸ h₂) (h₁'.antisymm h₂')
  }

-- works
instance linearOrder : LinearOrder Time.Tag :=
  { partialOrder with
    le_total := sorry
    decidableLE := sorry
    decidableEq := sorry
  }

Now I'm just confused. Is it something to do with definitions by pattern matching not being valid in some places?

[Sebastian Ullrich]

{ ... } structure instance notation simply does not accept parameters to the left of := at all. We mostly think of it generating data, while where is more used for generating code/functions, thus the slightly different syntactic options

[Eric Wieser]

Can the where syntax be used in an expression / a substructure?

[Marcus Rossel]

Regarding the initial question: Using a by block for le_antisymm fixes the problem for some reason ¯\_(ツ)_/¯ :

instance : LinearOrder Time.Tag where
  le_refl g := .inr ⟨rfl, le_refl _⟩
  le_trans _ _ _
    | .inl h₁, .inl h₂ => .inl $ h₁.trans h₂
    | .inl h₁, .inr ⟨h₂, _⟩ | .inr ⟨h₂, _⟩, .inl h₁ => .inl $ h₂ ▸ h₁
    | .inr ⟨h₁, h₁'⟩, .inr ⟨h₂, h₂'⟩ => .inr ⟨h₁.trans h₂, h₁'.trans h₂'⟩
  le_antisymm := by
    intro _ _; intro
    | .inl h₁, .inl h₂ => exact absurd h₁ h₂.asymm
    | .inl h₁, .inr ⟨h₂, _⟩ | .inr ⟨h₂, _⟩, .inl h₁ => exact absurd (h₂ ▸ h₁) (lt_irrefl _)
    | .inr ⟨h₁, h₁'⟩, .inr ⟨h₂, h₂'⟩ => exact Time.Tag.ext _ _ (h₁ ▸ h₂) (h₁'.antisymm h₂')
  le_total := by
    intro ⟨t₁, m₁⟩ ⟨t₂, m₂⟩
    by_cases ht : t₁ = t₂ <;> by_cases hm : m₁ = m₂ <;> simp_all
    · exact .inr ⟨rfl, le_rfl⟩
    · cases Nat.le_total m₁ m₂
      · exact .inl $ .inr ⟨rfl, ‹_›⟩
      · exact .inr $ .inr ⟨rfl, ‹_›⟩
    all_goals
      cases Nat.le_total t₁ t₂
      · exact .inl $ .inl $ lt_of_le_of_ne ‹_› ht
      · exact .inr $ .inl $ lt_of_le_of_ne ‹_› (ht ·.symm)
  decidableLE := inferInstance
  decidableEq := inferInstance

[Kevin Buzzard]

You can pattern match on an intro in tactic mode?? Nice!

[Marcus Rossel]

Kevin Buzzard said:

You can pattern match on an intro in tactic mode?? Nice!

In Lean 4 it feels like you can pattern match all the things :D

[Mario Carneiro]

Sebastian Ullrich said:

{ ... } structure instance notation simply does not accept parameters to the left of := at all. We mostly think of it generating data, while where is more used for generating code/functions, thus the slightly different syntactic options

FYI this is on my list of "grammar inconsistencies to PR fix once I find the time and stomach for it"