# Zulip Chat Archive

## Stream: new members

### Topic: finset.lt_wf fails

#### Anton Lorenzen (Feb 15 2020 at 16:55):

I want to define a procedure for generating fresh names like

def fresh_help : Π (s : finset string) (f : nat -> string) (n : nat), string | s := λ f n, if h : f n ∈ s then have finset.erase s (f n) ⊂ s := by simp [finset.erase_ssubset h], fresh_help (finset.erase s (f n)) f (n+1) else f n using_well_founded {rel_tac := λ _ _, `[exact ⟨_,(@finset.lt_wf string)⟩]} -- | Find a fresh name that is close to x def fresh (e : Exp) (x : string) : string := fresh_help (free_vars e) (λ n, nat.rec_on n x (λ n _, x ++ " " ++ repr n)) 0

However, lean can't find the 'have' for the well-foundedness:

/home/anton/orga/coc/src/CoC.lean:103:3: error: failed to prove recursive application is decreasing, well founded relation @has_well_founded.r (finset string) (@has_well_founded.mk (finset string) (@has_lt.lt (finset string) (@preorder.to_has_lt (finset string) (@partial_order.to_preorder (finset string) (@finset.partial_order string)))) _) The nested exception contains the failure state for the decreasing tactic. nested exception message: match failed state: fresh_help : finset string → (ℕ → string) → ℕ → string, s : finset string, f : ℕ → string, n : ℕ, h : f n ∈ s, this : finset.erase s (f n) ⊂ s ⊢ finset.erase s (f n) ⊂ s

Do you know how I can fix this?

#### Anton Lorenzen (Feb 16 2020 at 09:26):

Also, the lean checker seems to be unhappy with it:

example : fresh (Exp.sort star) "x" = "x" := rfl -- works #eval fresh (Exp.free "x") "x" -- works: "x0" example : fresh (Exp.free "x") "x" = "x0" := rfl -- type mismatch

If I use

using_well_founded {rel_tac := λ e es, `[exact ⟨_,(@finset.lt_wf string)⟩] >> wf_tacs.rel_tac e es}

I get "tactic failed, there are no goals to be solved" which seems better?

#### Floris van Doorn (Feb 17 2020 at 21:43):

This seems to work for me

import data.finset def fresh_help : Π (s : finset string) (f : nat -> string) (n : nat), string | s := λ f n, if h : f n ∈ s then have finset.erase s (f n) ⊂ s := by simp [finset.erase_ssubset h], fresh_help (finset.erase s (f n)) f (n+1) else f n using_well_founded {rel_tac := λ _ _, `[exact ⟨_,(@finset.lt_wf string)⟩], dec_tac := `[assumption] }

I have no idea why specifying `dec_tac`

explicitly helps here. I thought that `assumption`

was the default tactic for proving well-foundedness.

#### Mario Carneiro (Feb 18 2020 at 03:28):

The default tactic is unfortunately not `assumption`

. It is an ad hoc tactic that uses the simplifier with stuff about sizeof and natural numbers, and while I think it uses the context, it does not try `assumption`

first as it should

#### Mario Carneiro (Feb 18 2020 at 03:29):

I almost always specify `dec_tac := `[assumption]`

for a manual well foundedness proof

Last updated: May 07 2021 at 00:30 UTC