Zulip Chat Archive

Stream: new members

Topic: finset.lt_wf fails


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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