How to make this recursion (?) work?

Stream: new members

[Ilmārs Cīrulis]

Here's a tiny example:

mutual
  inductive Value: Type where
  | function: ℕ → Expression → Value

  inductive Expression where
  | fun_apply: Expression → List Expression → Expression
end

def List.Exists {A} (L: List A) (P: A → Prop): Prop :=
  match L with
  | List.nil => False
  | x :: t => P x ∨ t.Exists P

def freeVariable (n: ℕ) (exp: Expression): Prop :=
  match exp with
  | Expression.fun_apply f L => freeVariable n f ∨ L.Exists (fun e => freeVariable n e)

How to make this work?

Thank you!

[Joachim Breitner]

See https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/ in particular section “Nested recursion”

[Ilmārs Cīrulis]

We can use this function before Lift.map, ignore the proof in the argument to List.map, and suddenly Lean accepts the definition:

Is that Lift.map a spelling error?

[Ilmārs Cīrulis]

Thank you, it works!

mutual
  inductive Value: Type where
  | function: ℕ → Expression → Value

  inductive Expression where
  | fun_apply: Expression → List Expression → Expression
end

def List.Exists {A} (L: List A) (P: A → Prop): Prop :=
  match L with
  | List.nil => False
  | x :: t => P x ∨ t.Exists P

def freeVariable (n: ℕ) (exp: Expression): Prop :=
  match exp with
  | Expression.fun_apply f L => freeVariable n f ∨ List.Exists L.attach (fun ⟨e, _⟩ => freeVariable n e)

[Notification Bot]

Ilmārs Cīrulis has marked this topic as resolved.

[Joachim Breitner]

Ilmārs Cīrulis said:

Is that Lift.map a spelling error?

Thanks, pushed a fix (to be deployed in a bit)

[Notification Bot]

Ilmārs Cīrulis has marked this topic as unresolved.

[Ilmārs Cīrulis]

How to get this to work? I'm stuck, it seems.

inductive Expression where
| var: String → Expression
| object: List (String × Expression) → Expression

def t (exp: Expression): List String :=
  match exp with
  | Expression.var s => [s]
  | Expression.object L => List.foldl (fun L1 L2 => L1 ++ L2) [] (L.attach.map (fun x => t x.1.2))

[Ilmārs Cīrulis]

I managed to do it this way, using decreasing_by.

inductive Expression where
| var: String → Expression
| object: List (String × Expression) → Expression

def t (exp: Expression): List String :=
  match exp with
  | Expression.var s => [s]
  | Expression.object L => List.foldl (fun L1 L2 => L1 ++ L2) [] ((L.map (fun x => x.2)).attach.map (fun ⟨x, h⟩ => t x))
  decreasing_by
    simp at *
    obtain ⟨a, Ha⟩ := h
    simp_wf
    have H := List.sizeOf_lt_of_mem Ha
    simp at H
    omega