Induction for a recursive function

Stream: maths

[Harun Khan]

Hi, I have a function defined like this.

def foo (c : Fin n -> Rat) :=
    if condition then
       output
    else
       let c' : Fin n -> Rat := fun i => if c' i = max c then 0 else c i
       foo c'

This terminates because at least one element is being set to 0 at every iteration and we started with n elements. When the ci's are all zero it actually satisfies condition.
I want to prove a theorem about foo. Say I already proved termination. Is there a theorem that would let me simply reason about the output with the assumption condition in the context because when it terminates, that's what is outputted?

[Timo Carlin-Burns]

I don't think there is a general theorem for this because it requires an analysis of the whole function to see that all of the other return paths are recursive calls. Here is how you could prove a theorem like this in a simplified example:

def Output : Type := sorry
def condition : Nat → Bool := sorry
theorem condition_zero : condition 0 := sorry
def output : Nat → Output := sorry

def foo (n : Nat) :=
   if h : condition n then
      output n
   else
      match n, condition_zero with
      | (n' + 1), _ => foo n'

theorem foo_spec (n : Nat) : ∃ m : Nat, foo n = output m := by
   unfold foo
   split
   · exact ⟨n, rfl⟩
   · -- In the `false` case, we appeal to `foo_spec` inductively, using the same termination argument used to define `foo`.
     match n, condition_zero with
     | (n' + 1), _ => exact foo_spec n'

[Harun Khan]

Oh that's really nice! I see you index by n.