Induction over the height of a derivation tree

Stream: Is there code for X?

[Elias Castegren]

Sometimes it is useful to be able to do induction over the height of a derivation tree rather than the direct shape, especially when doing strong induction. Is there a built-in way to do this in Lean? I come from Rocq, where my approach is to copy my inductive denifition and add a size parameter that decreases for every premise. I can prove equivalence between the heighted and non-heighted version to be able to switch between them in proofs and can then do strong induction on the height.

Here is a small example (where the technique is complete overkill):

inductive Expr
| int (n : Int) : Expr
| add (e1 e2 : Expr) : Expr

inductive Eval : Expr → Int → Prop
| int n :
    Eval (Expr.int n) n
| add e1 e2 n1 n2 :
    Eval e1 n1 →
    Eval e2 n2 →
    Eval (Expr.add e1 e2) (n1 + n2)

inductive Eval' : Nat → Expr → Int → Prop
| int n depth :
    Eval' (Nat.succ depth) (Expr.int n) n
| add e1 e2 n1 n2 depth :
    Eval' depth e1 n1 →
    Eval' depth e2 n2 →
    Eval' (Nat.succ depth) (Expr.add e1 e2) (n1 + n2)

theorem eval'_le {e : Expr} {n : Int} {d1 d2 : Nat} :
  Eval' d1 e n →
  d1 ≤ d2 →
  Eval' d2 e n :=
  by
  intro h lt
  induction h generalizing d2 with
  | int n d1 =>
    cases d2 with
    | zero =>
      contradiction
    | succ d2' =>
      constructor
  | add e1 e2 n1 n2 d1 h1 h2 ih1 ih2 =>
    cases d2 with
    | zero =>
      contradiction
    | succ d2' =>
      constructor
      · apply ih1
        omega
      · apply ih2
        omega

theorem eval_equiv_eval' (e : Expr) (n : Int) :
  Eval e n ↔ ∃ depth : Nat, Eval' depth e n :=
  by
  constructor
  · intro h
    induction h with
    | int n =>
      exists 1
      constructor
    | add e1 e2 n1 n2 h1 h2 ih1 ih2 =>
      cases ih1 with
      | intro d1 hd1 =>
        cases ih2 with
        | intro d2 hd2 =>
          exists Nat.succ (Nat.max d1 d2)
          constructor
          · apply eval'_le hd1
            apply Nat.le_max_left
          · apply eval'_le hd2
            apply Nat.le_max_right
  · intro h
    cases h with
    | intro depth heval' =>
      induction heval' with
      | int n d =>
        constructor
      | add e1 e2 n1 n2 d h1 h2 ih1 ih2 =>
        constructor
        · apply ih1
        · apply ih2

I can now prove properties using strong induction on the height of the derivation tree:

def some_prop (n : Int) : Prop := sorry

theorem eval_prop (e : Expr) (n : Int) :
  Eval e n →
  some_prop n :=
  by
  intro h
  simp only [eval_equiv_eval'] at h
  cases h with
  | intro d h =>
    induction d using Nat.strongRecOn with
    | ind d ih => /- ih : ∀ (m : Nat), m < d → Eval' m e n → some_prop n -/
      cases h with
      ...

This is useful, but it seems like everything from the definition of Eval' is complete boilerplate which could be generated. Is there such automation?

[Aaron Liu]

docs#SizeOf which is completely automatically generated and is the default termination measure for recursive definitions and recursive proofs

[Elias Castegren]

That seems like it would be useful, but it surprises me that the size a rule instance is 0 (and not 1). This means that I cannot use my induction hypothesis properly since I don't have stricly smaller sizes:

theorem eval_prop (e : Expr) (n : Int) :
  Eval e n →
  some_prop n :=
  by
  intro h
  have h_ex : ∃size, sizeOf h = size := ⟨sizeOf h, rfl⟩
  cases h_ex with
  | intro size h_size =>
    induction size using Nat.strongRecOn generalizing e n h with
    | ind size ih =>
      cases h with
      | int n' => -- ih : ∀ m < size, ∀ (e : Expr) (n : ℤ) (h : Eval e n), sizeOf h = m → some_prop n
        -- This surpises me:
        have size_is_zero : size = 0 := by
          rw [← h_size]
          simp
        sorry
      | add e1 e2 n1 n2 h1 h2 =>
        -- This implies that the size is always zero!?
        have : size = sizeOf h1 + sizeOf h2 := by
          rw [← h_size]
          simp
        sorry
        apply ih (sizeOf h1) e1 n1 h1
        apply ih (sizeOf h2) e2 n2 h2

The documentation suggests that there is a default sizeOf that always returns zero, so I am guessing I am seeing that?

[Paul Reichert]

The problem seems to be that you are using Prop-based types. Because Lean is a proof-irrelevant language, any two derivations (i.e. proofs) in Eval' will be equal, and in particular, all of the proof terms have the same size. If you want to induct over derivation trees, you need to make Eval' return a Type -- then sizeOf should return sensible values.

[Aaron Liu]

and usually when I'm working with these sorts of things I can reform my argument to not require strong induction only structural induction so I don't need to do this is the first place

[Elias Castegren]

@Paul Reichert Thanks! With Eval as a Type instead, sizeOf works better but it also includes the size of the Expr and Int (reasonable when checking termination I guess) but it could be problematic for non-compositional premises. Ideally I would like to have just the size of the derivation tree (or the height, really), but this is something to work from.

[Elias Castegren]

@Aaron Liu That's good for you, but I have use cases where (strong) induction over the height at least greatly simplifies the proofs.

[Paul Reichert]

Have you considered writing your own size function? I haven't thought too much about whether there are other termination problems lurking in this approach, though.

[Elias Castegren]

That might work with Eval as a Type (it's a good way to solve induction over mutually recursive datatypes in Rocq) but for Prop it doesn't seem like I can write the size function. Also, not having it as a Prop means you can't negate it (and possibly other things?).

I mean, I do have a method that works (Eval' in my first post), but I was hoping to avoid the boilerplate code somehow. Maybe I should be looking into the metaprogramming facilities of Lean?