simp_wf to prove sizeOf of structure >= sizeOf of field

Stream: lean4

[Andrea Censi]

I am learning Lean 4.

I am working with large inductive structures and I need to prove terminations by relying on sizeOf.
However, the suggestions that I get from LLMs seem to be specific for Lean 3 and something changed in Lean 4 (specifically instSizeOf not available).

At this point, my understanding is that

1. Lean 4 creates SizeOf for all structures (adding a deriving SizeOf shows the conflict);
2. simp_wf includes tactics that look specifically at the inequality of the sizeOf of a structure vs its fields.
3. proving that sizeOf s.FIELD ≤ sizeOf s should be only a couple of lines.

Something like this should work:

structure A where
  description : String

def field_smaller_than_structure (s : A) : sizeOf s.description ≤ sizeOf s := by
  simp_wf
  omega -- maybe

but it doesn't.

Also various random applications of unfolding of sizeOf don't really expand to the definition of sizeOf for the structure.

Can somebody offer any hint?

[Aaron Liu]

It would be great to have more context

[Aaron Liu]

what function are you proving terminates?

[Andrea Censi]

@Aaron Liu It is a boring large function, think of a syntax -> semantics functor between two categories. I have no problem with writing the termination_by clauses, if I can rely on the sizeOf axioms like the above.

[Aaron Liu]

the problem is you probably won't need this fact ever when proving termination

[Aaron Liu]

so I want to know what weird circumstances have lead you to need this theorem

[Andrea Censi]

@Aaron Liu Sure, I can give you the link to the structures I am operating on. This link goes directly to one of the mutual blocks for the inductive structure Poset: https://gist.github.com/AndreaCensi/d569effe029c7349cdcbf48a093101ad#file-mcdp_schema_lean-lean-L477
(The file contains many other similar examples)
This is a link to my draft of the function interpret: https://gist.github.com/AndreaCensi/d569effe029c7349cdcbf48a093101ad#file-temp-lean
It is not self contained but I imagine it can give you an idea of what's going on.

[Aaron Liu]

ok you have convinced me that whatever it is that made you need this fact it's not worth my time to figure out

[Aaron Liu]

anyways here's the theorem you asked for

structure A where
  description : String

def field_smaller_than_structure (s : A) : sizeOf s.description ≤ sizeOf s := by
  cases s; simp

[Andrea Censi]

@Aaron Liu thanks!

[Andrea Censi]

@Aaron Liu I dug deeper into the problem and see you were right: the sizeOf approach is showing its limitations.

I prepared a minimal example with a tree-like inductive type with three variants (a leaf, a node with two branches, a node with n branches). The example function, which represents a common pattern in my code, is a structural equality that ignores one of the fields. It simply recurses into the tree and computes a Bool.

The specific problem with this sizeOf approach is that, in the NodeN case where the branches are stored in a list, the generated goals don't include the information that the elements belong to the list, so I cannot finish the proof.

What approaches other than sizeOf would you recommend for cases like this?

Thanks in advance!

import Mathlib.Tactic.Linarith

-- Simple tree-like structure type
inductive A : Type 0
  -- a leaf with data
  | Leaf             (description : Option String) (payload: Nat)

  -- a node with two branches (easy to prove termination)
  | Node2      (description : Option String) (P : A) (Q : A)

  -- a node with n branches
  | NodeN (description : Option String) (subs : List A)


-- Structural equality that ignores the description field
def A.struct_eq  (P1 P2: A) : Bool :=
  match P1, P2 with
  | .Leaf desc1 data1, .Leaf desc2 data2   => data1 = data2

  | .Node2 desc1 Q1 R1, .Node2 desc2 Q2 R2 =>
      A.struct_eq Q1 Q2 && A.struct_eq R1 R2

  | .NodeN desc1 subs1, .NodeN desc2  subs2 =>
      (subs1.length == subs2.length) &&
        (List.zip subs1 subs2).all (fun (a, b) => A.struct_eq a b)

  -- All different constructor combinations are false
  | _, _ => false

termination_by sizeOf P1 + sizeOf P2
decreasing_by
  next => simp_wf; omega
  next => simp_wf; omega
  next =>
    -- goal is
    --  ⊢ sizeOf a + sizeOf b
    --      < sizeOf (NodeN desc1 subs1) + sizeOf (NodeN desc2 subs2)
    simp_wf
    have h1: sizeOf a < sizeOf subs1 := by sorry -- cannot derive a ∈ subs1
    have h2: sizeOf b < sizeOf subs2 := by sorry -- cannot derive b ∈ subs2
    have h := Nat.add_lt_add h1 h2
    linarith

[Aaron Liu]

docs#List.attach

[Andrea Censi]

@Aaron Liu Thanks!

For the record, here is the solution:

import Mathlib.Tactic.Linarith

-- Simple tree-like structure type
inductive A : Type 0
  -- a leaf with data
  | Leaf             (description : Option String) (payload: Nat)

  -- a node with two branches (easy to prove termination)
  | Node2      (description : Option String) (P : A) (Q : A)

  -- a node with n branches
  | NodeN (description : Option String) (subs : List A)


-- Structural equality that ignores the description field
def A.struct_eq  (P1 P2: A) : Bool :=
  match P1, P2 with
  | .Leaf _ data1, .Leaf _ data2   => data1 = data2

  | .Node2 _ Q1 R1, .Node2 _ Q2 R2 =>
      A.struct_eq Q1 Q2 && A.struct_eq R1 R2

  | .NodeN _ subs1, .NodeN _  subs2 =>
      (subs1.length == subs2.length) &&
        (List.zip subs1.attach subs2.attach).all (fun (⟨a, _ha⟩, ⟨b, _hb⟩) => A.struct_eq a b)

  -- All different constructor combinations are false
  | _, _ => false

termination_by sizeOf P1 + sizeOf P2
decreasing_by
  next => simp_wf; omega
  next => simp_wf; omega
  next =>
    -- goal is
    --  ⊢ sizeOf a + sizeOf b
    --      < sizeOf (NodeN desc1 subs1) + sizeOf (NodeN desc2 subs2)
    simp_wf
    -- we have _ha : a ∈ subs1 and _hb : b ∈ subs2 from List.attach
    have h1: sizeOf a < sizeOf subs1 := List.sizeOf_lt_of_mem _ha
    have h2: sizeOf b < sizeOf subs2 := List.sizeOf_lt_of_mem _hb
    omega

[Andrea Censi]

(duplicate message)