Prove termination of mutually recursive definitions

Stream: new members

[Jakub Nowak]

How can I prove termination of those mutually recursive definitions?

mutual

  structure Foo : Type where
    bar : Option Bar

  structure Bar : Type where
    foo : Foo

end

mutual

  def Foo.func (foo : Foo) : Prop := foo.bar.elim True Bar.func

  def Bar.func (bar : Bar) : Prop := bar.foo.func

end

Or maybe it's impossible to prove that in Lean?
On paper, these definitions terminate, because a finite term for Foo or Bar must at some point have none as a value for foo.bar. So sizeOf should be correct termination_by metric, but Lean unfortunately failed to find proof.

[Jakub Nowak]

The goal for Foo.func is

foo : Foo
bar : Bar
⊢ sizeOf bar < sizeOf foo

so it looks like the way I wrote this function it's impossible to prove it's terminating.

[Jakub Nowak]

I've used match instead of Option.elim:

mutual

  structure Foo : Type where
    bar : Option Bar

  structure Bar : Type where
    foo : Foo

end

mutual

  def Foo.func (foo : Foo) : Prop :=
    match eq : foo.bar with
    | none => True
    | some bar => bar.func
  termination_by sizeOf foo

  def Bar.func (bar : Bar) : Prop := bar.foo.func
  termination_by sizeOf bar

end

and now the goal is

foo : Foo
bar : Bar
eq : foo.bar = some bar
⊢ sizeOf bar < sizeOf foo

which at least looks provable, but I still don't know how to prove it.
The proof should be something like sizeOf bar < sizeOf (some bar) = sizeOf foo.bar < sizeOf foo. But I don't know how to prove sizeOf foo.bar < sizeOf foo.

[Jakub Nowak]

Now I'm utterly confused:

mutual

  structure Foo : Type where
    bar : Option Bar

  structure Bar : Type where
    foo : Foo

end

mutual

  def Foo.func (foo : Foo) : Prop :=
    match eq : foo.bar with
    | none => True
    | some bar => bar.func
  termination_by sizeOf foo
  decreasing_by
    calc
      sizeOf bar < sizeOf (some bar) := by simp
      sizeOf (some bar) = sizeOf foo.bar := by rw [eq]
      sizeOf foo.bar < 1 + sizeOf foo.bar := by simp
      1 + sizeOf foo.bar = sizeOf foo := by
        have : foo = { bar := foo.bar } := rfl
        exact (Foo.mk.sizeOf_spec foo.bar).symm

  def Bar.func (bar : Bar) : Prop := bar.foo.func
  termination_by sizeOf bar

end

Something (delabolator?) replaced foo = { bar := foo.bar } with foo = foo. At the same time Lean complains

Type mismatch
  Eq.symm (Foo.mk.sizeOf_spec foo.bar)
has type
  1 + sizeOf foo.bar = sizeOf { bar := foo.bar }
but is expected to have type
  1 + sizeOf foo.bar = sizeOf foo

???

[Jakub Nowak]

Now I'm missing how to prove foo = Foo.mk foo.bar

mutual

  structure Foo : Type where
    bar : Option Bar

  structure Bar : Type where
    foo : Foo

end

mutual

  def Foo.func (foo : Foo) : Prop :=
    match eq : foo.bar with
    | none => True
    | some bar => bar.func
  termination_by sizeOf foo
  decreasing_by
    calc
      sizeOf bar < sizeOf (some bar) := by simp
      sizeOf (some bar) = sizeOf foo.bar := by rw [eq]
      sizeOf foo.bar < 1 + sizeOf foo.bar := by simp
      1 + sizeOf foo.bar = sizeOf foo := by
        have : foo = Foo.mk foo.bar := by sorry
        rw [this]
        exact (Foo.mk.sizeOf_spec foo.bar).symm

  def Bar.func (bar : Bar) : Prop := bar.foo.func
  termination_by sizeOf bar

end

[Wang Jingting]

It seems that you can tag Foo with @[ext], then you can use ext; rfl to show foo = { bar := foo.bar }.
But I think there should be a better way to do this.

[Jakub Nowak]

Thanks!

Now I finally have working code. But getting here was so hard and the code is so elaborate. I hope someone can point out how to make this simpler. :pleading_face:
Ideally I would want to not to have to prove termination manually at all.

mutual

  @[ext]
  structure Foo : Type where
    bar : Option Bar

  @[ext]
  structure Bar : Type where
    foo : Foo

end

mutual

  def Foo.func (foo : Foo) : Prop :=
    match eq : foo.bar with
    | none => True
    | some bar => bar.func
  termination_by sizeOf foo
  decreasing_by
    simp_wf
    calc
      sizeOf bar < sizeOf (some bar) := by simp
      sizeOf (some bar) = sizeOf foo.bar := by rw [eq]
      sizeOf foo.bar < 1 + sizeOf foo.bar := by simp
      1 + sizeOf foo.bar = sizeOf foo := by
        have : foo = Foo.mk foo.bar := by ext; rfl
        rw [this]
        exact (Foo.mk.sizeOf_spec foo.bar).symm

  def Bar.func (bar : Bar) : Prop := bar.foo.func
  termination_by sizeOf bar
  decreasing_by
    simp_wf
    calc
      sizeOf bar.foo < 1 + sizeOf bar.foo := by simp
      1 + sizeOf bar.foo = sizeOf bar := by
        have : bar = Bar.mk bar.foo := by ext; rfl
        rw [this]
        exact (Bar.mk.sizeOf_spec bar.foo).symm

end

[Jakub Nowak]

Maybe the best idea is to follow this advice and not use mutual definitions in the first place:

inductive FooBarTy
| foo
| bar

inductive FooBar : FooBarTy → Type where
| mkFoo : (bar? : Option (FooBar .bar)) → FooBar .foo
| mkBar : (foo : FooBar .foo) → FooBar .bar

def FooBar.func : (foobar : FooBar ty) → Prop
| .mkFoo none => True
| .mkFoo (some bar) => bar.func
| .mkBar foo => foo.func

def Foo := FooBar .foo
def Bar := FooBar .bar

noncomputable instance : SizeOf Foo where
  sizeOf foo := sizeOf (α := FooBar .foo) foo

noncomputable instance : SizeOf Bar where
  sizeOf bar := sizeOf (α := FooBar .bar) bar

@[match_pattern]
def Foo.mk (bar? : Option Bar) : Foo := .mkFoo bar?

@[match_pattern]
def Bar.mk (foo : Foo) : Bar := .mkBar foo

def Foo.bar? : Foo → Option Bar
| .mkFoo bar? => bar?

def Bar.foo : Bar → Foo
| .mkBar foo => foo

@[elab_as_elim, induction_eliminator, cases_eliminator]
def Foo.rec {motive : Foo → Sort _} (mk : ∀ bar?, motive (.mk bar?)) (foo : Foo) : motive foo :=
  match eq : foo with
  | .mkFoo bar? =>
    have : FooBar.mkFoo bar? = Foo.mk bar? := by simp [Foo.mk]
    this ▸ mk bar?

@[elab_as_elim, induction_eliminator, cases_eliminator]
def Bar.rec {motive : Bar → Sort _} (mk : ∀ foo, motive (.mk foo)) (bar : Bar) : motive bar :=
  match eq : bar with
  | .mkBar foo =>
    have : FooBar.mkBar foo = Bar.mk foo := by simp [Bar.mk]
    this ▸ mk foo

def Foo.func (foo : Foo) : Prop := FooBar.func foo

def Bar.func (bar : Bar) : Prop := FooBar.func bar

[Aaron Liu]

By the way, this just works, and without being well-founded recursion

mutual

  structure Foo : Type where
    bar : Option Bar

  structure Bar : Type where
    foo : Foo

end

mutual

def Foo.func (foo : Foo) : Prop :=
  match foo with
  | .mk none => True
  | .mk (some bar) => bar.func

def Bar.func (bar : Bar) : Prop :=
  match bar with
  | .mk foo => foo.func

end

[Robin Arnez]

Yeah, projections are simply not well supported in recursion