mathlib4#560

Stream: mathlib4

[Ruben Van de Velde]

mathlib4#560 could use help from someone who knows how decreasing_by works

[Jireh Loreaux]

Haven't looked at the PR but you should just need to provide a proof that the recursive argument is smaller than the input.

[Mario Carneiro]

This is the definition:

theorem WellFounded.asymmetric {α : Sort _} {r : α → α → Prop} (h : WellFounded r) :
    ∀ ⦃a b⦄, r a b → ¬r b a
  | a => fun b hab hba => asymmetric h hba hab
termination_by _ => h
decreasing_by {
  sorry
}

this is not a recursive definition, it is a name resolution issue. (We need to document this on the port wiki page.)

[Mario Carneiro]

you need to use an appropriately qualified version of asymmetric here; lean 3 would resolve this without WellFounded.asymmetric in scope but lean 4 will think you are calling yourself here

[Scott Morrison]

Over in mathlib3 we have

theorem well_founded.asymmetric {α : Sort*} {r : α → α → Prop} (h : well_founded r) :
  ∀ ⦃a b⦄, r a b → ¬ r b a
| a := λ b hab hba, well_founded.asymmetric hba hab
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, h⟩],
                     dec_tac := tactic.assumption }

[Mario Carneiro]

oh, I stand corrected

[Mario Carneiro]

I don't even know what mathport does with using_well_founded clauses

[Mario Carneiro]

the answer is: nothing at all, it completely forgot those existed

[Scott Morrison]

Something is weird, here, however.

[Scott Morrison]

You can replace the sorry above with change (0 : ℕ) < 0, so it's not going to be provable as written.

[Mario Carneiro]

the termination_by is incorrect and was not added by mathport

[Mario Carneiro]

oof, there is a bug in lean 3 causing using_well_founded clauses not to be exported at all, so we'll need to cut a new release

[Yakov Pechersky]

The termination_by is my attempt to approximate the rel_tac in mathlib3, not knowing what I am doing!

[Scott Morrison]

I've fixed this now, using an auxiliary definition