Showing termination for mutually recursive definitions

Stream: general

[Mai]

I believe the List.map is causing the issue, but I am not quite sure how to solve this

import Mathlib

structure PosVar where
  n : Nat
deriving DecidableEq

structure NegVar where
  n : Nat
deriving DecidableEq

mutual
  inductive PosType where
    | func : List (NegVar × Constraint) -> NegType -> PosType -> PosType
    | var : PosVar -> PosType

  inductive NegType where
    | var : NegVar -> NegType

  inductive Constraint where
    | isFunc : PosType -> NegType -> Constraint
end

mutual
  def PosType.freeVars (τ : PosType) : List PosVar × List NegVar :=
    match τ with
    | .func cons dom codom =>
      let (bound, cons) := cons.unzip
      let (pos1, neg1) := cons.map Constraint.freeVars |> List.unzip
      let pos1 := pos1.flatten
      let neg1 := neg1.flatten
      let (pos2, neg2) := dom.freeVars
      let (pos3, neg3) := codom.freeVars
      (pos1 ++ pos2 ++ pos3, (neg1 ++ neg2 ++ neg3) \ bound)
    | .var v => ([v], [])

  def NegType.freeVars : NegType -> List PosVar × List NegVar
    | .var v => ([], [v])

  def Constraint.freeVars (c : Constraint) : List PosVar × List NegVar :=
    match c with
    | .isFunc dom codom =>
      let (pos1, neg1) := dom.freeVars
      let (pos2, neg2) := codom.freeVars
      (pos1 ++ pos2, neg1 ++ neg2)
end

[Malvin Gattinger]

I think docs#List.attach should do the trick, but then I ran into a weird issue about the default instances used for sizeOf :thinking: I'll stop here, maybe the stuff below is useful. Thanks for the rabbit hole :wink:

import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Analysis.Normed.Ring.Lemmas
import Mathlib.Data.Int.Star
-- import Mathlib

structure PosVar where
  n : Nat
deriving DecidableEq

structure NegVar where
  n : Nat
deriving DecidableEq

mutual
  inductive PosType where
    | func : List (NegVar × Constraint) -> NegType -> PosType -> PosType
    | var : PosVar -> PosType

  inductive NegType where
    | var : NegVar -> NegType

  inductive Constraint where
    | isFunc : PosType -> NegType -> Constraint
end

-- This one is not actually mutual.
def NegType.freeVars : NegType -> List PosVar × List NegVar
  | .var v => ([], [v])

-- Oh wait `List.sizeOf_lt_of_mem` is not enough because we do an `unzip` below.

lemma sizeOf_mem_unzip_lt {y : β} {L : List (α × β)} : y ∈ L.unzip.2 → sizeOf y < sizeOf L := by
  intro y_in
  rw [List.unzip_eq_map] at y_in
  simp at y_in
  rcases y_in with ⟨x, xy_in⟩
  have := List.sizeOf_lt_of_mem xy_in
  simp_all
  linarith

mutual
  def PosType.freeVars (τ : PosType) : List PosVar × List NegVar :=
    match τ with
    | .func cons dom codom =>
      let (pos1, neg1) := (cons.unzip.2).attach.map (fun ⟨x,hx⟩ => Constraint.freeVars x) |> List.unzip
      let pos1 := pos1.flatten
      let neg1 := neg1.flatten
      let (pos2, neg2) := dom.freeVars
      let (pos3, neg3) := codom.freeVars
      (pos1 ++ pos2 ++ pos3, (neg1 ++ neg2 ++ neg3) \ cons.unzip.1)
    | .var v => ([v], [])
  termination_by
    sizeOf τ
  decreasing_by
    · have := sizeOf_mem_unzip_lt hx
      simp
      -- Why is linarith not solving this?
      exact calc sizeOf x
             < sizeOf cons := by convert this <;> sorry -- Constraint._sizeOf_inst = instSizeOfDefault Constraint -- ???
           _ < 1 + sizeOf cons + sizeOf dom + sizeOf codom := by linarith
    · simp

  def Constraint.freeVars (c : Constraint) : List PosVar × List NegVar :=
    match c with
    | .isFunc dom codom =>
      let (pos1, neg1) := dom.freeVars
      let (pos2, neg2) := codom.freeVars
      (pos1 ++ pos2, neg1 ++ neg2)
  termination_by
    sizeOf c
end

[Joachim Breitner]

Here is a possible definition:

import Mathlib

structure PosVar where
  n : Nat
deriving DecidableEq

structure NegVar where
  n : Nat
deriving DecidableEq

mutual
  inductive PosType where
    | func : List (NegVar × Constraint) -> NegType -> PosType -> PosType
    | var : PosVar -> PosType

  inductive NegType where
    | var : NegVar -> NegType

  inductive Constraint where
    | isFunc : PosType -> NegType -> Constraint
end

mutual
  def PosType.freeVars (τ : PosType) : List PosVar × List NegVar :=
    match τ with
    | .func cons dom codom =>
      let (bound, fvs) := cons.map (fun nc => (nc.1, nc.2.freeVars)) |> List.unzip
      let (pos1, neg1) := fvs.unzip
      let pos1 := pos1.flatten
      let neg1 := neg1.flatten
      let (pos2, neg2) := dom.freeVars
      let (pos3, neg3) := codom.freeVars
      (pos1 ++ pos2 ++ pos3, (neg1 ++ neg2 ++ neg3) \ bound)
    | .var v => ([v], [])
  termination_by sizeOf τ
  decreasing_by
    · have := List.sizeOf_lt_of_mem ‹_›
      grind [Prod.mk.sizeOf_spec]
    · decreasing_tactic

  def NegType.freeVars : NegType -> List PosVar × List NegVar
    | .var v => ([], [v])

  def Constraint.freeVars (c : Constraint) : List PosVar × List NegVar :=
    match c with
    | .isFunc dom codom =>
      let (pos1, neg1) := dom.freeVars
      let (pos2, neg2) := codom.freeVars
      (pos1 ++ pos2, neg1 ++ neg2)
  termination_by sizeOf c
end

The necessary tricks were:

• Don’t first unzip the cons parameter, but map it directly, so that the termination proof doesn’t need to know something about unzip.
• Use projection rather than pattern matching in the argument to map.
• Use List.sizeOf_lt_of_mem explicitly in the manual termination proof before using grind. (I hope that this step will be automatic once grind is used for termination checking by default).

[Mai]

Joachim Breitner said:

• I hope that this step will be automatic once grind is used for termination checking by default

Is there a tracking issue for this?

[Joachim Breitner]

No, it’s just in the back of people’s head, queued up with many other things that need doing :shrug:

[Mai]

Joachim Breitner said:

• Use projection rather than pattern matching in the argument to map.

I really dislike having to do this. I feel like intuitively it shouldn't matter

[Joachim Breitner]

Yes, I’m actually surprised because usually pattern matching works better here than projection. But if I write

      let (bound, fvs) := cons.map (fun (nv, c) => (nv, c.freeVars)) |> List.unzip

I get the unsolvable goal

cons : List (NegVar × Constraint)
dom : NegType
codom : PosType
x✝ : NegVar × Constraint
h✝ : x✝ ∈ cons
c : Constraint
⊢ sizeOf c < sizeOf (PosType.func cons dom codom)

and it’s not clear to me why the connection between c and x✝ is lost.

It works if you already in the function definition indicate that you want that connection to be preserved:

      let (bound, fvs) := cons.map (fun x => match _ : x with | (nv, c) => (nv, c.freeVars)) |> List.unzip

yields

cons : List (NegVar × Constraint)
dom : NegType
codom : PosType
x : NegVar × Constraint
h✝¹ : x ∈ cons
nv : NegVar
c : Constraint
h✝ : x = (nv, c)
⊢ sizeOf c < sizeOf (PosType.func cons dom codom)

Ah, yes, while lean will refine a proof goal if it mentions the scrutinee of a match (as usually the case when using match on a function parameter), in this case the proof goal mentions sizeOf (PosType.func cons dom codom) but the variable x is not present.

Ok, at least it works as intended, even if this isn’t particularly convenient when doing pattern matching this way.

[Mai]

I am not sure what you're saying, is there a reason it shouldn't maintain the relationship when pattern matching in the parameter?

[Joachim Breitner]

It’s desireable from a user point of view, but changing the match on the fly from match x to match h : x is a non-trivial operation, so that’s why it’s not being one universally right now.

[Mai]

So I am back working on this, with a slightly different configuration:

import Mathlib.Data.List.Defs

structure TypeVar where
  n : Nat
deriving DecidableEq

mutual
  inductive PosType where
    | func : List (TypeVar × List Constraint) -> NegType -> PosType -> PosType
    | var : TypeVar -> PosType

  inductive NegType where
    | var : TypeVar -> NegType

  inductive Constraint where
    | isFunc : PosType -> NegType -> Constraint
end

mutual
  def PosType.freeVars (τ : PosType) : List TypeVar :=
    match τ with
    | .func vars dom codom =>
      let bound := vars.map Prod.fst
      let consVars := vars.flatMap fun v => v.2.flatMap fun c => c.freeVars
      (consVars ∪ dom.freeVars ∪ codom.freeVars) \ bound
    | .var v => [v]
  termination_by sizeOf τ
  decreasing_by
    · have := List.sizeOf_lt_of_mem ‹c ∈ v.2›
      have := List.sizeOf_lt_of_mem ‹v ∈ vars›
      grind
    · grind

  def NegType.freeVars (τ : NegType) : List TypeVar :=
    match τ with
    | .var v => [v]
  termination_by sizeOf τ

  def Constraint.freeVars (c : Constraint) : List TypeVar :=
    match c with
    | .isFunc dom codom => dom.freeVars ∪ codom.freeVars
  termination_by sizeOf c
end

Seems to work just fine. However, if I replace

let consVars := vars.flatMap fun v => v.2.flatMap fun c => c.freeVars

with

let consVars := (vars.flatMap fun v => v.2).flatMap fun c => c.freeVars

I lose the membership hypotheses. any ideas why?

[Mirek Olšák]

This termination_by for mutual functions feels a bit magical. @Joachim Breitner , do I understand correctly that in general, one must use the same well-ordered type for all termination_by, and the different measures get collected all across the mutual block into each individual decreasing_by proof goal?

[Mirek Olšák]

Mai said:

I lose the membership hypotheses. any ideas why?

I guess you are asking too much from the heuristics that automatically inserts the .attach. You can do it manually with

let consVars := (vars.flatMap fun v => v.2).attach.flatMap fun ⟨c, hin⟩ => c.freeVars

and get the hypothesis

hin : c ∈ List.flatMap (fun v => v.snd) vars

[Mai]

ahh, what's .attach?

[Mai]

I don't think I've seen it before really :grinning_face_with_smiling_eyes:

[Joachim Breitner]

Mirek Olšák schrieb:

This termination_by for mutual functions feels a bit magical. Joachim Breitner , do I understand correctly that in general, one must use the same well-ordered type for all termination_by, and the different measures get collected all across the mutual block into each individual decreasing_by proof goal?

Exactly. Every recursive call must be decreasing wrt to some measure, whether the call is to the same function or another.

[Ruben Van de Velde]

docs#List.attach

[Mirek Olšák]

Mai said:

ahh, what's .attach?

That is the underlying mechanism why such a hypothesis appeared in the first place.
Consider the most basic example. You can write a function

example (l : List Nat) := l.map (fun x ↦ x+1)

You could want to proof something inside this function, for example

example (l : List Nat) := l.map (fun x ↦
  have : x ∈ l := by
    sorry
  x+1
)

but you will fail. The only variables that you have in the context are the variables l and x but nothing relating them together. The attach trick is to "retype" the elements of l to a different type that contains more information.

variable (l : List Nat)
#check l.attach -- l.attach : List { x // x ∈ l }
example := l.attach.map (fun ⟨x, pf⟩ ↦
  have : x ∈ l := pf
  x+1
)

The list elements gets "attached" the information that they are members of that list.

This is happening automatically in decreasing_by to some degree but figuring out what extra context to capture is a bit heuristic, so not fully reliable.