Problems with Well Founded Recursion

Stream: new members

[Devon Richards]

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]

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

[Devon Richards]

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]

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

[Devon Richards]

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]

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]

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]

It only works if the inequality is at type nat

[Devon Richards]

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

[Reid Barton]

Add

using_well_founded { dec_tac := `[assumption] }

[Devon Richards]

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]

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]

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]

(deleted)