Zulip Chat Archive

Stream: mathlib4

Topic: recursive definitions in instance fields

Jireh Loreaux (Nov 21 2022 at 15:34):

In mathlib4#672 I seem to be stuck on an issue of how to construct something recursively with pattern matching. In Lean 3, it looks like this, and I have included the tactic state at the relevant place (note the _match). In Lean 4, I had to add the extra arguments to match on, but I can't seem to refer recursively to the conn function, where in Lean 3 we could do this with _match.

Lean 3

instance is_order_connected (r : α → α → Prop)
  [is_order_connected α r] [is_trichotomous α r] :
  is_order_connected (list α) (lex r) :=
⟨λ l₁, match l₁ with
| _,     [],    c::l₃, nil    := or.inr nil
| _,     [],    c::l₃, rel _ := or.inr nil
| _,     [],    c::l₃, cons _ := or.inr nil
| _,     b::l₂, c::l₃, nil := or.inl nil
| a::l₁, b::l₂, c::l₃, rel h :=
  (is_order_connected.conn _ b _ h).imp rel rel
| a::l₁, b::l₂, _::l₃, cons h := begin
    rcases trichotomous_of r a b with ab | rfl | ab,
    { exact or.inl (rel ab) },
    {
      /-
      α : Type u,
      r : α → α → Prop,
      _inst_1 : is_order_connected α r,
      _inst_2 : is_trichotomous α r,
      l₁ : list α,
      _match : ∀ (_a b c : list α), lex r _a c → lex r _a b ∨ lex r b c,
      a : α,
      l₁ l₂ l₃ : list α,
      h : lex r l₁ l₃
      ⊢ lex r (a :: l₁) (a :: l₂) ∨ lex r (a :: l₂) (a :: l₃)
      -/
      exact (_match _ l₂ _ h).imp cons cons },
    { exact or.inr (rel ab) }
  end
end⟩

Lean 4

instance isOrderConnected (r : α → α → Prop) [IsOrderConnected α r] [IsTrichotomous α r] :
    IsOrderConnected (List α) (Lex r) where
  conn := fun l₁ l₂ l₃ r' => match l₁, l₂, l₃, r' with
    | _, [], c :: l₃, nil => Or.inr nil
    | _, [], c :: l₃, rel _ => Or.inr nil
    | _, [], c :: l₃, cons _ => Or.inr nil
    | _, b :: l₂, c :: l₃, nil => Or.inl nil
    | a :: l₁, b :: l₂, c :: l₃, rel h => (IsOrderConnected.conn _ b _ h).imp rel rel
    | a :: l₁, b :: l₂, _ :: l₃, cons h => by
      rcases trichotomous_of r a b with (ab | rfl | ab)
      · exact Or.inl (rel ab)
      · exact sorry --(_match _ l₂ _ h).imp cons cons
      · exact Or.inr (rel ab)

Jireh Loreaux (Nov 21 2022 at 16:37):

FYI: asked this in the Lean 4 stream on a simplified example: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/recursive.20definition.20in.20structure.20fields

Adam Topaz (Nov 21 2022 at 17:12):

You could use let rec I suppose. I don't know if this is the best approach though

Jireh Loreaux (Nov 21 2022 at 17:19):

yeah, I thought of that as a last resort, but surely there is (or at least needs to be) a better way, especially because in that case I have to write down the full type.

Adam Topaz (Nov 21 2022 at 17:27):

I guess the following isn't too verbose:

theorem foo : ∀ n : Nat, 0 ≤ n
  | 0 => Nat.le_refl 0
  | n + 1 => Nat.le_trans (foo n) n.le_succ -- works

example : ∀ n : Nat, 0 ≤ n
  | 0 => Nat.le_refl 0
  | n + 1 => Nat.le_trans (_example n) n.le_succ -- works

structure Bar :=
  bar : ∀ n : Nat, 0 ≤ n

def myBar : Bar where
  bar :=
    let rec aux
    | 0 => Nat.le_refl 0
    | n + 1 => Nat.le_trans (aux n) n.le_succ
  aux

Adam Topaz (Nov 21 2022 at 17:27):

but I agree that there should be a better way to do this.

Jireh Loreaux (Nov 21 2022 at 17:30):

In this case it's not too verbose, but if Lean can't infer the type of aux and it's relatively painful to write, then it gets silly.

Jireh Loreaux (Nov 21 2022 at 17:32):

That being said, it can infer the type in my situation as well.

Adam Topaz (Nov 21 2022 at 17:32):

Note that this works as well

theorem foo : ∀ n : Nat, 0 ≤ n
  | 0 => Nat.le_refl 0
  | n + 1 => Nat.le_trans (foo n) n.le_succ -- works

example : ∀ n : Nat, 0 ≤ n
  | 0 => Nat.le_refl 0
  | n + 1 => Nat.le_trans (_example n) n.le_succ -- works

structure Bar :=
  bar : ∀ n : Nat, 0 ≤ n

def myBar : Bar where
  bar := aux where
  aux
    | 0 => Nat.le_refl 0
    | n + 1 => Nat.le_trans (aux n) n.le_succ

Adam Topaz (Nov 21 2022 at 17:34):

and I suppose that's better for the issue you brought up

Henrik Böving (Nov 21 2022 at 17:54):

Jireh Loreaux said:

In this case it's not too verbose, but if Lean can't infer the type of aux and it's relatively painful to write, then it gets silly.

shouldn't it always be able to infer the type given that it is used right afterwards as a value for a field where the type is known?

Jireh Loreaux (Nov 21 2022 at 17:55):

But doesn't it have to ~~parse~~ elaborate the let binding first? I thought that's why Adam's second solution would be better in general.

Henrik Böving (Nov 21 2022 at 17:57):

Not necessarily, the elaboration procedure can always "yield" back to the next highe relaborator and let it do some more work before continuing with its own elaboration later on in hopes that more information (such as the type) might be available. While I am not sure that this is the case here it is very much a possiblity.

Henrik Böving (Nov 21 2022 at 17:59):

For example you can use sorry in the let here:

def myBar : Bar where
  bar :=
    let rec aux := sorry
    aux

in which case it is impossible for lean to derive the type of aux just from looking at the value because sorry already expects the type to be known so I would expect that this delayed elaboration (or some variation) is indeed what is happening here