Mutual Recursion

Stream: lean4

[Chiyoku]

Hi, i'm trying to run this code with a mutual recursion but I'm getting a strange error about the tactic assumption

def Ident : Type := String
  deriving BEq

inductive Term where
  | var : Ident → Term
  | abs : Ident → Term → Term
  | app : Term  → Term → Term

  | zero : Term
  | succ : Term → Term

  | case : Term → Term → Ident → Term → Term
  | fixpoint : Ident → Term → Term

open Term

mutual
  def boundSubs (from_ : Ident) (to: Term) (app: Ident → Term → Term) (binder: Ident) (body: Term) : Term :=
    if binder == from_
      then app binder body
      else app binder (substitute from_ to body)

  def substitute (from_ : Ident) (to : Term) : Term → Term
    | var x => if x == from_ then to else var x
    | app a b => app (substitute from_ to a) (substitute from_ to b)
    | zero    => zero
    | succ e  => succ (substitute from_ to e)
    | case cond onZ name onS =>
      let onCase := (case (substitute from_ to cond) (substitute from_ to onZ))
      boundSubs from_ to onCase name onS
    | abs param body => boundSubs from_ to abs param body
    | fixpoint n t => boundSubs from_ to fixpoint n t
end

termination_by
  substitute _ _ expr => sizeOf expr
  boundSubs _ _ _ _ f => sizeOf f

Error

tactic 'assumption' failed,
app : Ident → Term → Term
binder : Ident
body : Term
⊢ sizeOf body < sizeOf body

[Leonardo de Moura]

You should be using an old Lean 4 binary. We have improved the error message. Could you please get the latest nightly build and try again?

[Leonardo de Moura]

Note that boundSubs has a recursive substitute application and the argument body is the same one taken by boundSubs. In the well-founded relation you selected, this application is not "smaller". You can use a slightly different well-founded relation.

termination_by
  boundSubs _ _ _ _ f => (sizeOf f, 1)
  substitute _ _ expr => (sizeOf expr, 0)

[Leonardo de Moura]

BTW, the termination_by notation names arguments from right to left. So, you don't need all the _s.

termination_by
  boundSubs f => (sizeOf f, 1)
  substitute expr => (sizeOf expr, 0)

[sgcs]

I'm running into an error when doing mutual recursion:

fail to show termination for
  normal_does_not_reduce
  neutral_does_not_reduce
with errors
structural recursion does not handle mutually recursive functions

failed to prove termination, use `termination_by` to specify a well-founded relation

Essentially I'm doing a very dumbed down lambda calculus and I've defined mutually inductive Normal and Neutral data types that are indexed by well-typed expressions. The code is the following:

mutual

private theorem normal_does_not_reduce
  {n : Nat} {Γ : Context n} {e₁ e₂ : Expr n} {τ : Ty} {t₁ : Γ ⊢ e₁ : τ} {t₂ : Γ ⊢ e₂ : τ} :
  Normal t₁ → (t₁ ⟶ t₂) → Empty
  | .neutral neut, tr => neutral_does_not_reduce neut tr

private theorem neutral_does_not_reduce
  {n : Nat} {Γ : Context n} {e₁ e₂ : Expr n} {τ : Ty} {t₁ : Γ ⊢ e₁ : τ} {t₂ : Γ ⊢ e₂ : τ} :
  Neutral t₁ → (t₁ ⟶ t₂) → Empty
  | .plus₁ neut₁ _, .ξ_plus₁ tr₁ => neutral_does_not_reduce neut₁ tr₁
  | .plus₁ _ norm₂, .ξ_plus₂ norm₁ tr₂ => normal_does_not_reduce norm₂ tr₂
  | .plus₂ v₁ _, .ξ_plus₁ tr₁ => v₁.does_not_reduce tr₁
  | .plus₂ _ neut₂, .ξ_plus₂ norm₁ tr₂ => neutral_does_not_reduce neut₂ tr₂

end

I spent a good amount of time trying to come up with a MWE, but I didn't succeed (see https://pastebin.com/0pxHUrmw,). It doesn't give the same error for some reason, but that's essentially what I have (except I have contexts and De Bruijn indices added).

I understand that without a MWE, it may be hard to help, but was hoping someone may have a quick tip to help resolve the issue.

[Heather Macbeth]

@sgcs This is probably the part of the error message you should listen to:

failed to prove termination, use `termination_by` to specify a well-founded relation

[Heather Macbeth]

So your struture will be (fill in the XXX)

mutual

private theorem normal_does_not_reduce
  {n : Nat} {Γ : Context n} {e₁ e₂ : Expr n} {τ : Ty} {t₁ : Γ ⊢ e₁ : τ} {t₂ : Γ ⊢ e₂ : τ} :
  Normal t₁ → (t₁ ⟶ t₂) → Empty
  | .neutral neut, tr => neutral_does_not_reduce neut tr

private theorem neutral_does_not_reduce
  {n : Nat} {Γ : Context n} {e₁ e₂ : Expr n} {τ : Ty} {t₁ : Γ ⊢ e₁ : τ} {t₂ : Γ ⊢ e₂ : τ} :
  Neutral t₁ → (t₁ ⟶ t₂) → Empty
  | .plus₁ neut₁ _, .ξ_plus₁ tr₁ => neutral_does_not_reduce neut₁ tr₁
  | .plus₁ _ norm₂, .ξ_plus₂ norm₁ tr₂ => normal_does_not_reduce norm₂ tr₂
  | .plus₂ v₁ _, .ξ_plus₁ tr₁ => v₁.does_not_reduce tr₁
  | .plus₂ _ neut₂, .ξ_plus₂ norm₁ tr₂ => neutral_does_not_reduce neut₂ tr₂

end
termination_by normal_does_not_reduce => XXX ; neutral_does_not_reduce => XXX

[Heather Macbeth]

See some of the later examples at this link:
https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html#well-founded-recursion-and-induction

[sgcs]

I had given that a shot:

termination_by normal_does_not_reduce norm tr => norm
                neutral_does_not_reduce neut tr => neut

But I was getting:

type mismatch
  norm
has type
  Normal t₁ : Type
but is expected to have type
  ?β : Sort ?u.269218

Which I don't understand since it seems like it should unify just fine? I ended up taking a different approach and got it working though:

private theorem normal_or_neutral_does_not_reduce
  {n : Nat} {Γ : Context n} {e₁ e₂ : Expr n} {τ : Ty} {t₁ : Γ ⊢ e₁ : τ} {t₂ : Γ ⊢ e₂ : τ}
  (norm_or_neut : Sum (Normal t₁) (Neutral t₁)) (tr : t₁ ⟶ t₂) : Empty :=
  match t₁, norm_or_neut, tr with
  | _, .inl (.neutral neut), tr => normal_or_neutral_does_not_reduce (Sum.inr neut) tr
  | .number _, .inl .number, tr => nomatch tr
  | .string _, .inl .string, tr => nomatch tr
  | .plus _ _, .inr (.plus₁ neut₁ _), .ξ_plus₁ tr₁ => normal_or_neutral_does_not_reduce (Sum.inr neut₁) tr₁
  | .plus _ _, .inr (.plus₁ _ norm₂), .ξ_plus₂ norm₁ tr₂ => normal_or_neutral_does_not_reduce (Sum.inl norm₂) tr₂
  | .plus _ _, .inr (.plus₂ v₁ _), .ξ_plus₁ tr₁ => v₁.does_not_reduce tr₁
  | .plus _ _, .inr (.plus₂ _ neut₂), .ξ_plus₂ norm₁ tr₂ => normal_or_neutral_does_not_reduce (Sum.inr neut₂) tr₂

[Mario Carneiro]

your alignment is bad in that example

[Mario Carneiro]

termination_by normal_does_not_reduce norm tr => norm
                neutral_does_not_reduce neut tr => neut

will be interpreted as

termination_by normal_does_not_reduce norm tr => norm neutral_does_not_reduce neut tr => neut

[Mario Carneiro]

which fails since norm isn't a function

[sgcs]

I think the alignment was just a copy-paste issue, it was aligned for my personally