define a function by iterating

Stream: new members

[Jake Levinson]

I have a function that either maps α → α or α → β depending on whether a "termination" predicate p : α → Prop holds. I know that the function terminates after finitely many steps, so I'd like to define f_total : α → β by repeating the function until it finishes. What's the best way to do this?

I'm not sure how to express the "terminates in finitely many steps" thing (as in ∀ (a : α), ∃ (n : ℕ), ... something p n a), but conveniently there is a decreasing natural number associated to each a and the function must stop if the number is 0 (but may finish sooner), so I managed to use that instead.

Still my formalization feels messy. In particular I have a tactic-based definition of f_total. Here it is:

import tactic
import data.set.basic

variables {α β : Type}

def p : α → Prop := sorry
def f_go {a : α} (hp : p a) : α := sorry
def f_stop {a : α} (hnp : ¬ p a) : β := sorry

def p_rank : α → ℕ := sorry
lemma p_rank_decr {a : α} (hp : p a) :
  (p_rank (f_go hp)).succ = p_rank a := sorry
lemma p_stop0 {a : α} (hpr : p_rank a = 0) : ¬ p a := sorry

def totalf_0 : {a : α // p_rank a = 0} → β :=
  λ a, f_stop (p_stop0 a.prop)

noncomputable def totalf_succ (n : ℕ) (fn : {a : α // p_rank a = n} → β) :
  {a : α // p_rank a = n.succ} → β :=
λ a, begin
  by_cases hp : p a.val,
  -- fn ∘ f_go
  apply fn ⟨f_go hp, _⟩,
  rw [← nat.succ_inj', p_rank_decr hp],
  exact a.prop,
  -- f_stop
  exact f_stop hp,
end

noncomputable def totalf' : Π (n : ℕ), {a : α // p_rank a = n} → β :=
  λ (n : ℕ), nat.rec totalf_0 totalf_succ n

noncomputable def totalf : α → β := λ a, totalf' (p_rank a) ⟨a, rfl⟩

So this basically works for this toy case, but the tactic-based definition of totalf_succ makes me worry it would be hard to work with.
The function I'm trying to work with is quite a bit more complicated, so I also wonder if I'm missing an easier way to use nat.rec or something.

Thanks for any help!

[Jake Levinson]

Maybe this is better, using dite:

def totalf_0 : {a : α // p_rank a = 0} → β :=
  λ a, f_stop (p_stop0 a.prop)

lemma totalf_aux {n : ℕ} {a : α} (h : p a) (h' : p_rank a = n.succ) :
  p_rank (f_go h) = n :=
begin
  rw [← nat.succ_inj', p_rank_decr h],
  exact h',
end

def totalf_succ [∀ (a : α), decidable (p a)] (n : ℕ)
  (fn : {a : α // p_rank a = n} → β) : {a : α // p_rank a = n.succ} → β :=
λ a, dite (p a.val) (λ h, fn ⟨f_go h, totalf_aux h a.prop⟩) f_stop

def totalf' [∀ (a : α), decidable (p a)] : Π (n : ℕ), {a : α // p_rank a = n} → β :=
  λ (n : ℕ), nat.rec totalf_0 totalf_succ n

def totalf [∀ (a : α), decidable (p a)] : α → β :=
  λ a, totalf' (p_rank a) ⟨a, rfl⟩

[Mario Carneiro]

That sounds pretty similar to docs#pfun.fix

[Mario Carneiro]

It produces a partial function, but you can prove it terminates separately and thus get a regular function out

[Mario Carneiro]

The usual way we would write this is using well founded recursion like so:

variables {α β : Type}

def p : α → Prop := sorry
def f_go (a : α) (hp : p a) : α := sorry
def f_stop (a : α) (hnp : ¬ p a) : β := sorry
instance : decidable_pred (@p α) := sorry

def p_rank : α → ℕ := sorry
lemma p_rank_decr {a : α} (hp : p a) : (p_rank (f_go a hp)).succ = p_rank a := sorry

def totalf : α → β
| a :=
  if h : p a then
    have p_rank (f_go a h) < p_rank a, by rw [← p_rank_decr h]; apply nat.lt_succ_self,
    totalf (f_go a h)
  else f_stop a h
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf p_rank⟩] }

[Jake Levinson]

Interesting, yes this looks very much like what I wanted. Thank you very much!

[Jake Levinson]

What does the notation

`[...]

mean?

[Jake Levinson]

@Mario Carneiro Further question, is there a way to do this without having to write down the output type?

[Mario Carneiro]

The `[...] syntax constructs a tactic unit using the interactive parser. It is just like begin ... end, but instead of running the tactic on the current goal it just constructs the tactic and returns it. The using_well_founded syntax is a bit arcane and 99% of the time it's just exact of some term like here, but in principle you can use a tactic to generate the well founded relation.

[Mario Carneiro]

I'm not sure which output type you are referring to. If you mean the T in have T, from ... in the example, you don't really need it but the decreasing tactic is using assumption to find a proof that the call is decreasing so you need something defeq to that in the context one way or another. Also the rw proof doesn't really work if the type is not known.

[Mario Carneiro]

All of the sorry'd definitions can be inlined, there is no need to have them separate

[Jake Levinson]

Actually I just meant α and β. My function is actually of the form Π (a : α), α_aux a → Σ' (b : β), β_aux b and it's a bit involved to write down the full type of the output. (Some intermediate steps in what I have were just defined as foo x := ... without explicitly writing down the type of foo x.)

I actually managed to get the function working based on the skeleton you provided!

I also just tried to add some more stuff to it and encountered this error: rec_fn_macro only allowed in meta definitions. Any idea what this means? It would be a little tricky to extract a mwe for this.

[Jake Levinson]

Mario Carneiro said:

I'm not sure which output type you are referring to. If you mean the T in have T, from ... in the example, you don't really need it but the decreasing tactic is using assumption to find a proof that the call is decreasing so you need something defeq to that in the context one way or another. Also the rw proof doesn't really work if the type is not known.

Ah, that's quite enlightening. Thanks.

[Jake Levinson]

The rec_fn_macro error seems to arise when I try to replace β by a dependent type of the form Σ' (b : β) (h1 : p1 b) (h2 : p2 b), β_aux b where p1 b and p2 b are some extra Props about the function output type.

The problem seems to occur with only one of the extra Props, namely one that involves set.finite.to_finset.card... roughly it's like h2 : b.size = a.size + 1 where b.size and a.size are two finset.card's associated to the input and output.

[Jake Levinson]

(I realize this is vague, I'll try to extract a mwe... but whatever it is is something subtle)

[Jake Levinson]

Maybe it would be simpler to leave the output type as just Σ' (b : β), β_aux b since I had that one working. In that case I have one more question, which is how do I inductively prove facts about the output of the totalf function, given appropriate facts about f_go and f_stop?

[Jake Levinson]

I'm not sure how to prove things about a function defined with using_well_founded. Continuing with the totalf function defined above, given a property preserved by f_go and f_stop, how can I prove it holds for outputs of totalf? This is the lemma r_totalf below (I have an attempt at a proof, which doesn't seem to work). Complete mwe, sorry it's getting a bit long:

import tactic
import data.set.basic

def α : Type := sorry
def β : Type := sorry

def p : α → Prop := sorry
instance : decidable_pred p := sorry
def f_go {a : α} (hp : p a) : α := sorry
def f_stop {a : α} (hnp : ¬ p a) : β := sorry

def p_rank : α → ℕ := sorry
lemma p_rank_decr {a : α} (hp : p a) : (p_rank (f_go hp)) < p_rank a := sorry

def totalf : α → β
| a :=
  if h : p a then
    have p_rank (f_go h) < p_rank a := p_rank_decr h,
    totalf (f_go h)
  else f_stop h
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf p_rank⟩]}

-- A property preserved by f:
def r : α → Prop := sorry
def rβ : β → Prop := sorry
lemma rf_go {a : α} (hp : p a) : r a → r (f_go hp) := sorry
lemma rf_stop {a : α} (hnp : ¬ p a) : r a → rβ (f_stop hnp) := sorry

lemma r_totalf : Π {a : α}, r a → rβ (totalf a)
| a h :=
begin
  rw totalf,
  by_cases hp : p a; simp [hp], rotate,
  exact rf_stop hp h,
  have wf : p_rank (f_go hp) < p_rank a := p_rank_decr hp,
  exact r_totalf (rf_go hp h), -- *** this line is not accepted
end
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ ⟨a, h⟩, p_rank a)⟩]}

I get the following error message:

1 goal
r_totalf: ∀ {a : α}, r a → rβ (totalf a)
a: α
h: r a
hp: p a
wf: p_rank (f_go hp) < p_rank a
⊢ rβ (totalf (f_go _))
Messages (1)
failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r (Σ' {a : α}, r a)
    (@has_well_founded.mk (Σ' {a : α}, r a)
       (@measure (Σ' {a : α}, r a)
          (λ (_x : Σ' {a : α}, r a),
             (λ (_a : Σ' {a : α}, r a), _a.cases_on (λ (fst : α) (snd : r fst), id_rhs ℕ (p_rank fst))) _x))
       _)
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
default_dec_tac failed
state:
r_totalf : ∀ (_p : Σ' {a : α}, r a), rβ (totalf _p.fst),
a : α,
h : r a,
hp : p a
⊢ id_rhs ℕ (p_rank (f_go hp)) < id_rhs ℕ (p_rank a)

It looks like the desired well-foundedness inequality id_rhs ℕ (p_rank (f_go hp)) < id_rhs ℕ (p_rank a) is pretty close to the hypothesis wf: p_rank (f_go hp) < p_rank a, I'm not sure what's wrong.

[Jake Levinson]

Figured it out, and I might as well include the answer for posterity (in case anyone else encounters the same error message):

https://leanprover-community.github.io/extras/well_founded_recursion.html

"Note that the have must not be in tactics mode, i.e. inside any begin end. If you are in tactics mode, there is the option of putting the have statement inside the exact statement."

So for the example above, it's enough to change

have wf : p_rank (f_go hp) < p_rank a := p_rank_decr hp,
exact r_totalf (rf_go hp h),  -- *** this line is not accepted

to this:

exact have p_rank (f_go hp) < p_rank a := p_rank_decr hp,
      r_totalf (rf_go hp h), -- works!