## 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.

#### 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):

(deleted)

Last updated: Dec 20 2023 at 11:08 UTC