finset.lt_wf fails

Stream: new members

[Anton Lorenzen]

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]

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]

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]

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]

I almost always specify dec_tac := `[assumption] for a manual well foundedness proof