Zulip Chat Archive

Stream: new members

Topic: using_well_founded


Paul Rowe (Jan 12 2022 at 22:12):

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 (Jan 12 2022 at 22:21):

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 (Jan 12 2022 at 22:23):

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 (Jan 12 2022 at 22:23):

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 (Jan 12 2022 at 22:24):

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

Paul Rowe (Jan 12 2022 at 22:28):

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 (Jan 12 2022 at 22:29):

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 (Jan 12 2022 at 22:32):

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 (Jan 12 2022 at 22:32):

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 (Jan 12 2022 at 22:35):

@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 (Jan 12 2022 at 22:36):

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 (Jan 12 2022 at 22:38):

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!


Last updated: Dec 20 2023 at 11:08 UTC