Generic strong recursion over naturals

Stream: Is there code for X?

[Thomas Vigouroux]

Hey there, I am encountering a lot of instances of theorems which proofs are along the lines of "by recursion on the size of T" where T is an inductive type.

I am wondering if there could be a lemma that generalize Nat.strongRec to work when the strong recursion is actually the result of a function T -> Nat, and if possible, have the proof that his principle is correct?

[Thomas Vigouroux]

I thin the actual lemma is somewhere along the lines of:

theorem map_rec {motive: T -> Sort _} (weight: T -> Nat) (ind: /- translation of Nat.strongRec ind argument -/) (v: T): motive v

[Mario Carneiro]

This is usually done using well founded recursion where you use termination_by t => weight t

[Thomas Vigouroux]

With the ind argument being along the lines of \all (v:T), (\all v', weight v' < weight v -> motive v') -> motive v

[Thomas Vigouroux]

Mario Carneiro said:

This is usually done using well founded recursion where you use termination_by t => weight t

Hmm I think I am not familiar enough with termination_by then... I wanted to use this principle as part of proofs that are not necessarily termination proofs (actually proofs about sequent calculus G4ip)

[Mario Carneiro]

It's not a termination proof, it's a proof by well founded recursion on T

[Thomas Vigouroux]

I don't really understand that
For me my question we just about doing strong recursion on natural numbers, but casting the property as a property on T and the recursion on a "weight function" given by the user

[Timo Carlin-Burns]

For example, you could prove map_rec using well-founded recursion on T with termination_by _ => weight x

theorem map_rec {motive : T -> Sort _} (weight : T -> Nat)
    (ind : (x : T) → ((y : T) → weight y < weight x → motive y) → motive x)
    (x : T) : motive x :=
  ind x (fun y _ => map_rec weight ind y)
termination_by map_rec weight _ x => weight x

[Timo Carlin-Burns]

In general, there are sort of two styles of inductive proof in lean, those using the induction tactic and those using recursive definitions.

For example, you can prove 0 + n = n using two different syntaxes for induction:

theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n zero_add_n =>
    rw [Nat.add_succ]
    rw [zero_add_n]

theorem zero_add' (n : Nat) : 0 + n = n := by
  cases n with
  | zero => rfl
  | succ n =>
    rw [Nat.add_succ]
    rw [zero_add' n] -- Note: This is recursive. We are referring to `zero_add` in its own definition.
    -- Lean needs to infer a proof that this recursion terminates

If you want to use the induction tactic to do the kind of "weighted induction" you're talking about, you would indeed need a lemma like map_rec so you could say induction x using map_rec, but with the approach where you use a recursive definition, all you would need is to add termination_by => weight x to the end of your definition, which might be easier.

[Mario Carneiro]

you can also use let rec in the middle of a proof if your inductive hypothesis doesn't match the original theorem