using_well_founded

Stream: new members

[Paul Rowe]

I have a rather complicated recursive function and I'm having trouble getting Lean to accept the recursion. Hoping to get some advice. Below is a fake version that has enough of the same structure to illustrate my issue. When the third case hits, it uses f to select another element. Several facts seem relevant:
E is a fintype, so I can't keep decreasing forever.
Applying f will immediately land me in one of the previous non-recursive cases, so in fact, there should only ever be one recursive call.

import data.fintype.basic

section my_section

parameters (N : Type) [fintype N]

inductive E : Type
| t1 : N → E
| t2 : N → E
| t3 : N → E
open E

parameters [fintype E] [has_lt E]

-- This mimic real parts of the file
parameter (f : E → E)
parameter (h : ∀ (n : N), f (t3 n) < (t3 n))
parameter (h1 : ∀ (n : N), f (t3 n) = (t1 n) ∨ f (t3 n) = (t2 n))

def cs : E → ℕ
| (t1 n) := 12
| (t2 n) := 37
| (t3 n) := --tried: have f (t3 n) < (t3 n), from h n,
   cs (f (t3 n))
--tried: using_well_founded {dec_tac := `[tactic.assumption]}

end my_section

[Alex J. Best]

If you use the fintype derive handler you can prove that E is a fintype rather than adding it as a parameter, unfortunately it doesn't work if N is a parameter, only a variable (parameters aren't really used so much in mathlib for this sort of reason)

import data.fintype.basic
import tactic.derive_fintype

section my_section

variables (N : Type) [fintype N]

@[derive fintype]
inductive E : Type
| t1 : N → E
| t2 : N → E
| t3 : N → E
open E

[Floris van Doorn]

Hopefully in your actual proof the < is a partial order (or preorder). In that case, this works:

import data.fintype.basic

section my_section

parameters (N : Type) [fintype N]

inductive E : Type
| t1 : N → E
| t2 : N → E
| t3 : N → E
open E

parameters [fintype E] [preorder E]

-- This mimic real parts of the file
parameter (f : E → E)
parameter (h : ∀ (n : N), f (t3 n) < (t3 n))
parameter (h1 : ∀ (n : N), f (t3 n) = (t1 n) ∨ f (t3 n) = (t2 n))

def cs : E → ℕ
| (t1 n) := 12
| (t2 n) := 37
| (t3 n) := have f (t3 n) < (t3 n), from h n,
   cs (f (t3 n))
using_well_founded { rel_tac := λ _ _, `[exact ⟨(<),  fintype.preorder.well_founded⟩],
                     dec_tac := `[tactic.assumption] }

I also had to tell Lean w.r.t. what relation the recursion is decreasing and why it is well-founded (docs#fintype.preorder.well_founded)

[Paul Rowe]

Interesting! I didn't know about derive fintype. Since I didn't want to bother proving it for the purposes of a mwe I just added it as a parameter. Good to know I didn't need to do any work.

[Paul Rowe]

It is a partial order! Let me go try that and study it a bit to understand it.

[Paul Rowe]

I was searching everywhere for something like fintype.preorder.well_founded but couldn't get the docs search to turn it up. That's exactly what I need. Thanks!

[Alex J. Best]

Maybe I'm missing something or the MWE is too minimal, but if as soon as it hits t3 it goes straight to one of the other cases then you can define a function which will have the same equational properties without worrying about well_founded, or a relation on E at all

import data.fintype.basic
import tactic.derive_fintype

section my_section

variables (N : Type) [fintype N]

@[derive fintype]
inductive E : Type
| t1 : N → E
| t2 : N → E
| t3 : N → E
open E

--variable [has_lt (E N)]

-- This mimic real parts of the file
variable (f : E N → E N)
-- variable (h : ∀ (n : N), f (t3 n) < (t3 n))
-- variable (h1 : ∀ (n : N), f (t3 n) = (t1 n) ∨ f (t3 n) = (t2 n))

def cs_aux : ℕ → E N → ℕ
| _ (t1 n) := 12
| _ (t2 n) := 37
| 1 (t3 n) := cs_aux 0 (f (t3 n))
| _ (t3 n) := 0

def cs : E N → ℕ := cs_aux N f 1
end my_section

[Floris van Doorn]

Paul Rowe said:

I was searching everywhere for something like fintype.preorder.well_founded but couldn't get the docs search to turn it up. That's exactly what I need. Thanks!

I got it by searching for ​well_founded_of_fintype https://leanprover-community.github.io/mathlib_docs/find/well_founded_of_fintype

[Floris van Doorn]

usually if you search for the names of what you want and what you have, separated by an underscore, the search engine will find it.

[Paul Rowe]

@Alex J. Best Interesting idea. It's true that the mwe is much more minimal than the real thing. In fact, it does a few case splits on facts that might be true of the argument. So it might take some work for me to figure out the right aux function.

[Paul Rowe]

I honestly didn't think about the fact that it should only ever have at most one recursive call until I was writing up the question!

[Paul Rowe]

Floris van Doorn said:

usually if you search for the names of what you want and what you have, separated by an underscore, the search engine will find it.

Yeah, I was trying to do things like that. I must have just missed the right combinations. Thanks for the advice though!