Zulip Chat Archive

Stream: new members

Topic: Problems with Well Founded Recursion

Devon Richards (Jan 07 2021 at 19:08):

I have an issue where my definition is erroring out that it can't prove the recursive application is decreasing. The state it gives me though is

α : Type u,
t : topological_space α,
is_sigma_0_ξ : Π (ξ : ordinal), 1  ξ  ξ < (cardinal.aleph 1).ord  set α  Prop,
ξ : ordinal,
h : 1  ξ  ξ < (cardinal.aleph 1).ord,
s : set α,
heo : ¬ξ = 1,
hgo : 1 < ξ,
T : set (set α),
t : set α,
 : t  T,
ξₙ : ordinal,
hₙ : 1  ξₙ  ξₙ < ξ,
hdec : ξₙ < ξ,
hrec : 1  ξₙ  ξₙ < (cardinal.aleph 1).ord
 ξₙ < ξ

which has the goal as one of the hypotheses so I'm not sure what I can do to so it recognizes that the application is valid.

Bryan Gin-ge Chen (Jan 07 2021 at 19:09):

This page may help: https://leanprover-community.github.io/extras/well_founded_recursion.html

Devon Richards (Jan 07 2021 at 19:10):

I've looked at that and it helped me make some progress with the suggestion to push extra arguments into lambdas, but I didn't see anything that seems to apply specifically here. Am I missing something?

Reid Barton (Jan 07 2021 at 19:13):

Try turning on pp.all to see if there are some hidden differences?

Devon Richards (Jan 07 2021 at 19:16):

Trimming the output from that gives

hdec : @has_lt.lt.{?l_1+1} ordinal.{?l_1} ordinal.has_lt.{?l_1} ξₙ ξ,
      @has_lt.lt.{?l_1+1} ordinal.{?l_1} ordinal.has_lt.{?l_1} ξₙ ξ

which look identical to me

Devon Richards (Jan 07 2021 at 19:18):

Here's the definition that is causing the issues

def is_sigma_0_ξ : Π (ξ : ordinal), (1  ξ  ξ < (cardinal.aleph 1).ord)  set α  Prop
| ξ := λ h s,
  if heo: ξ = 1 then is_open s
  else  (T : set (set α)),
    ( (t : set α),
      t  T   (ξₙ : ordinal) (hₙ : 1  ξₙ  ξₙ < ξ),
        have hdec : ξₙ < ξ := hₙ.2,
        have hrec : 1  ξₙ  (ξₙ < (cardinal.aleph 1).ord),
          { split, exact hₙ.1, exact (lt_trans hₙ.2 h.2) },
        is_sigma_0_ξ ξₙ hrec t
    )  T.countable  (s = ⋃₀ T)

Reid Barton (Jan 07 2021 at 19:32):

I think the statement " - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions." is a lie

Reid Barton (Jan 07 2021 at 19:36):

It only works if the inequality is at type nat

Devon Richards (Jan 07 2021 at 19:38):

Well that would explain it. So I guess I need to rewrite it and use well_founded.fix to make it?

Reid Barton (Jan 07 2021 at 19:39):


using_well_founded { dec_tac := `[assumption] }

Devon Richards (Jan 07 2021 at 19:40):

Ah, that did work, thank you very much. Would a PR to update that error message be welcome so others don't get confused in the same way?

Reid Barton (Jan 07 2021 at 19:42):

The problem is in https://github.com/leanprover-community/lean/blob/master/library/init/meta/well_founded_tactics.lean#L201
cancel_nat_add_lt fails if the goal is not an inequality between nats, but instead it should just succeed without doing anything

Bryan Gin-ge Chen (Jan 07 2021 at 20:08):

I should come back to lean#288 which aimed to remove default_dec_tac altogether. I think all that's needed is fixing / deleting all the broken tests.

I'm not entirely clear on what the plan is afterwards; maybe things have changed in light of Lean 4. cc: @Mario Carneiro

Joao Bregunci (Mar 24 2021 at 16:59):


Last updated: Dec 20 2023 at 11:08 UTC