well_founded finsupp

Stream: general

[Johan Commelin]

Can someone explain to me how to prove that

instance [preorder α] [has_zero α] : preorder (σ →₀ α) :=
{ le := λ f g, ∀ s, f s ≤ g s,
  le_refl := λ f s, le_refl _,
  le_trans := λ f g h Hfg Hgh s, le_trans (Hfg s) (Hgh s) }

(see https://github.com/leanprover-community/mathlib/pull/1216/files#diff-af9f424915b54a36301c2cba4d92a12cR1447)
is well founded in the case α := ℕ

[Chris Hughes]

measure_wf

[Chris Hughes]

But you have to show that lt = λ f g, ∀ s, f s < g s

[Chris Hughes]

And that isn't your definition, but maybe it should be.

[Kenny Lau]

but it isn't

[Johan Commelin]

No, that's not the definition I want

[Chris Hughes]

Ah, it's actually much harder than I thought.

[Kenny Lau]

show that the downset is finite

[Johan Commelin]

Right, you did that.

[Johan Commelin]

How do I turn that into a proof of wf?

[Kenny Lau]

I don't know

[Kenny Lau]

but that seems like an important lemma

[Johan Commelin]

I only ask you to prove important lemmas :stuck_out_tongue_wink:

[Chris Hughes]

This is provable right.

f < g → f.sum (λ _, id) < g.sum (λ _, id)

[Kenny Lau]

I think it is

[Johan Commelin]

I now have an order embedding into multiset. How do I pullback the wellfoundedness?

[Kenny Lau]

subrel of wf is wf; inv_image of wf is wf

[Johan Commelin]

lemma to_multiset_strict_mono : strict_mono (@to_multiset σ _) :=
λ m n h,
begin
  rw lt_iff_le_and_ne at h ⊢, cases h with h₁ h₂,
  split,
  { rw multiset.le_iff_count, intro s, rw [count_to_multiset, count_to_multiset], exact h₁ s },
  { intro H, apply h₂, replace H := congr_arg multiset.to_finsupp H, simpa using H }
end

[Chris Hughes]

inv_image.wf

[Johan Commelin]

Aah, but the well founded relation on multiset is not the subset relation, is it?

[Chris Hughes]

It's strict subset.

[Chris Hughes]

Both ssubset and lt are well founded.

[Johan Commelin]

Is there a proof that lt is well founded?

[Johan Commelin]

Because that is the one I want to pull back

[Johan Commelin]

But typeclass inference finds the other one

[Chris Hughes]

There's probably a proof it implies card < card

[Kevin Buzzard]

I love the way that we mathematicians still don't properly understand induction.

[Johan Commelin]

Does someone see something that is obviously wrong with

def inv_of_unit (φ : mv_power_series σ α) (u : units α) (h : coeff 0 φ = u) : mv_power_series σ α
| n := if n = 0 then ↑u⁻¹ else
  - ↑u⁻¹ * finset.sum (n.diagonal) (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
    if h : x.1 < n then inv_of_unit x.1 * coeff x.2 φ else 0)
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, finsupp.lt_wf σ⟩] }

I get 6 deterministic timeouts, and no other useful error messages...

[Johan Commelin]

For the record:

lemma to_multiset_strict_mono : strict_mono (@to_multiset σ _) :=
λ m n h,
begin
  rw lt_iff_le_and_ne at h ⊢, cases h with h₁ h₂,
  split,
  { rw multiset.le_iff_count, intro s, rw [count_to_multiset, count_to_multiset], exact h₁ s },
  { intro H, apply h₂, replace H := congr_arg multiset.to_finsupp H, simpa using H }
end

lemma sum_lt_of_lt (m n : σ →₀ ℕ) (h : m < n) :
  m.sum (λ _, id) < n.sum (λ _, id) :=
begin
  rw [← card_to_multiset, ← card_to_multiset],
  apply multiset.card_lt_of_lt,
  exact to_multiset_strict_mono _ _ h
end

variable (σ)

def lt_wf : well_founded (@has_lt.lt (σ →₀ ℕ) _) :=
subrelation.wf (sum_lt_of_lt) $ inv_image.wf _ nat.lt_wf

[Johan Commelin]

Full code is available at https://github.com/leanprover-community/mathlib/blob/power-series/src/data/power_series.lean#L666-L670

[Johan Commelin]

def inv_of_unit (φ : mv_power_series σ α) (u : units α) (h : coeff 0 φ = u) : mv_power_series σ α
| n := if n = 0 then ↑u⁻¹ else
  - ↑u⁻¹ * finset.sum (n.diagonal) (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
    if h : x.1 < n then inv_of_unit x.1 * coeff x.2 φ else 0)
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, finsupp.lt_wf σ⟩] }

In this code I call inv_of_unit x.1. Do I recall correctly that I should not put the "default" arguments in recursive calls? That is, I should not replace this with inv_of_unit φ u h x.1. Or should I?
I get timeouts with both of these, so Lean doesn't tell me which one is correct.

[Chris Hughes]

You should only put the stuff right of the colon into a recursive call.

[Johan Commelin]

Right, so I did it correctly.

[Johan Commelin]

Any idea why Lean is unhappy?

[Chris Hughes]

Because there are no arguments right of the colon?

[Johan Commelin]

mv_power_series σ α := (σ →₀ ℕ) → α

[Johan Commelin]

Is that good enough?

[Johan Commelin]

If I replace the summand if h : x.1 < n then inv_of_unit x.1 * coeff x.2 φ else 0 with 0 then Lean is perfectly happy.

[Chris Hughes]

There's no closed curly bracket on the last line?

[Johan Commelin]

There is in my local copy :sad:

[Johan Commelin]

So that's also not the issue

[Chris Hughes]

MWE

[Chris Hughes]

Is it some decidability thing?

[Johan Commelin]

Voila: https://gist.github.com/jcommelin/a521437d3886968db4a54154da503f3e

[Johan Commelin]

The MWE is a bit long... I included the ring structure on power series.

[Johan Commelin]

The problem is all the way at the bottom. The rest of the file is mostly uninteresting.

[Johan Commelin]

I have [decidable_eq σ]... so that shouldn't be the issue, I think.

[Johan Commelin]

Hmmm.... but #check (by apply_instance : decidable_rel (@has_lt.lt (σ →₀ ℕ) _)) times out.

[Johan Commelin]

Is that bad?

[Johan Commelin]

Does the wf relation have to be decidable?

[Johan Commelin]

Defining that instance using sorry the inv_of_unit suddenly no longer times out, but gives an error message:

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r (σ →₀ ℕ)
    (@has_well_founded.mk (σ →₀ ℕ)
       (@has_lt.lt (σ →₀ ℕ)
          (@preorder.to_has_lt (σ →₀ ℕ)
             (@finsupp.preorder σ ℕ (λ (a b : σ), _inst_1 a b)
                (@partial_order.to_preorder ℕ
                   (@ordered_comm_monoid.to_partial_order ℕ
                      (@ordered_cancel_comm_monoid.to_ordered_comm_monoid ℕ
                         (@ordered_semiring.to_ordered_cancel_comm_monoid ℕ nat.ordered_semiring))))
                nat.has_zero)))
       _)

[Chris Hughes]

local attribute [instance, priority 0] classical.dec

noncomputable def inv_of_unit (φ : mv_power_series σ α) (u : units α) (h : coeff 0 φ = u) : mv_power_series σ α
| n := if n = 0 then ↑u⁻¹ else
- ↑u⁻¹ * finset.sum (n.diagonal) (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
   if h : x.1 < n then inv_of_unit x.1 * coeff x.2 φ else 0)
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, finsupp.lt_wf σ⟩],
  dec_tac := tactic.assumption }

[Chris Hughes]

You need decidable lt on finsupp because of the if

[Johan Commelin]

@Chris Hughes Thanks a lot!

[Johan Commelin]

Any hints on how I could prove that < is decidable?

[Chris Hughes]

What's the definition?

[Chris Hughes]

It might be unfold lt; apply_instance

[Johan Commelin]

The definition of le is \for s, f s ≤ g s.

[Johan Commelin]

So < is \exists s, f + single s 1 ≤ g.

[Chris Hughes]

Show it's equivalent to forall s in the support.

[Johan Commelin]

Exactly

[Johan Commelin]

Ok, this seems to work, but I don't know why :oops:

instance decidable_lt : decidable_rel (@has_lt.lt (σ →₀ ℕ) _) :=
λ m n,
begin
  have h : _ := _,
  rw lt_iff_le_and_ne, refine @and.decidable _ _ h _,
  rw le_iff, apply_instance
end

[Johan Commelin]

@Mario Carneiro Should we also have nat.diagonal?

[Johan Commelin]

Isomorphic to the special case finsupp unit nat...

[Johan Commelin]

Or is it better to use range n and subtraction?

[Johan Commelin]

Compare coeff_mul for polynomial: https://github.com/leanprover-community/mathlib/blob/master/src/data/polynomial.lean#L169-L170

[Mario Carneiro]

sure. I guess it's not hard to prove that (list.range (n+1)).map (\lam i, (i, n - i))has the requisite property

[Johan Commelin]

Also... shouldn't these things be called antidiagonal?

[Mario Carneiro]

I've been thinking about that

[Mario Carneiro]

simplex might also work in the finsupp generalization

[Johan Commelin]

Hmm, I would say finsupp.simplex (a : \a) is the set of finsupp X \a that sum up to a.

[Johan Commelin]

Or something like that.

[Johan Commelin]

@Mario Carneiro Would you approve of a PR that changes all diagonals to antidiagonals?

[Mario Carneiro]

sure

[Johan Commelin]

@Mario Carneiro Should something like nat.antidiagonal go into data/nat/basic? Or is it not basic enough?

[Mario Carneiro]

It should go in data.list.basic, data.multiset.basic, or data.finset.basic depending on which version you are talking about