feat(data/finsupp/lex): linear order on finsupps

[adomani]

EDIT: #16127 is an evolution of this PR. This PR has been closed.

This PR constructs a linear order on finsupps where both source and target are linearly ordered. This is useful for #15983, where these linear orders are used to prove that add_monoid_algebras have no non-trivial zero-divisors.

The PR also proves that the lexicographic linear order on finitely supported functions preserves (one) covariant class assumption.

This is a further step in proving that many add_monoid_algebras have no zero-divisors.

This PR is work in progress and comments or suggestions are as usual really really appreciated!

Zulip discussion

---

• depends on: feat(data/finsupp/witnesses): definition and API for witnesses of finsupps #16026 for some API about differences of supports of finsets.
• depends on: [Merged by Bors] - feat(algebra/*): Algebraic instances on lex/order_dual #16122

[eric-wieser]

Does removing this prevent things being noncomputable below?

[adomani]

Removing open_locale classical prevents union in finsupp from existing.

[eric-wieser]

Then you're missing decidable_eq α on a lemma somewhere. If you find yourself addnig open_locale classical to make a lemma statement compile, you've made a wrong turn.

[adomani]

Should I then also add decidable_pred (λ (a : α), ⇑f a ≠ ⇑g a), which now Lean asks?

[adomani]

(Or maybe decidable_eq N?)

[adomani]

@eric-wieser, I take it that you are happy with the decidable_eq assumption, instead of the ne version that is needed? Is there some rationale between preferring one over the other (besides simplicity of stating)?

[eric-wieser]

Can you copy over as many of the pi lemmas about lex as possible?

[adomani]

Can you copy over as many of the pi lemmas about lex as possible?

If I understand correctly, in the pi.lex file there is an underlying order on the Pi type (on line 66) and this instance is then used to prove monotonicity and various other lemmas. Should I port over this instance as well?

[vihdzp]

I think the suggestion is to prove the finsupp analogues of these pi theorems.

[adomani]

Sure, but those lemmas involve inequalities on the non-lex type, which does not have an order currently.

[eric-wieser]

Sure, but those lemmas involve inequalities on the non-lex type, which does not have an order currently.

What about this one?

mathlib/src/data/finsupp/order.lean

Line 37 in a21a8bc

instance : has_le (ι →₀ α) := ⟨λ f g, ∀ i, f i ≤ g i⟩

[adomani]

Eric, thanks! I was missing the import! I added lt/strict_order instances as well. I copied over some of the pi.lex lemmas. I omitted the bot ones, since the instances for bot on finsupp seem to be on canonically_ordered stuff, which seems not too relevant. Let me know what you think!

[eric-wieser]

Don't forget the lemmas finsupp.to_lex_apply and finsupp.of_lex_apply!

[adomani]

Don't forget the lemmas finsupp.to_lex_apply and finsupp.of_lex_apply!

These lemmas are in!

I tried to use the linear_order.lift, but failed. If I understand your suggestion correctly, I was trying to lift the order from the pi.lex instance. However, that instance has an extra instance of well-order that is not needed here, thanks to the finite support.

#check @pi.lex.linear_order
pi.lex.linear_order :
  Π {ι : Type u_3} {β : ι → Type u_4} [_inst_1 : linear_order ι]
  [_inst_2 : is_well_order ι has_lt.lt]   --  <-- here
  [_inst_3 : Π (a : ι), linear_order (β a)], linear_order (lex (Π (i : ι), β i))

[eric-wieser]

Here's a constructive version that doesn't need wit:

private def lt_trichotomy_rec {P : lex (α →₀ N)→ lex (α →₀ N) → Sort*}
  (h_lt : Π {f g}, f < g → P f g) (h_eq : Π {f g}, f = g → P f g) (h_gt : Π {f g}, g < f → P f g)
  (f g) : P f g  :=
(λ f g : α →₀ N, show P (to_lex f) (to_lex g), from
match _, rfl : ∀ y, (f.diff g).min = y → _ with
| ⊤, h := h_eq (finsupp.diff_eq_empty.mp (finset.min_eq_top.mp h))
| (wit : α), h :=
  have hne : f wit ≠ g wit := mem_diff.mp (finset.mem_of_min h),
  -- have hne' : f ≠ g := finsupp.diff_eq_empty.not.mp (ne_empty_o_,
  if hwit : f wit < g wit then
    h_lt ⟨wit, by exact λ j hj, begin
      refine mem_diff.not_left.mp _,
      replace hj := (with_top.coe_lt_coe.mpr hj).trans_eq h.symm,
      contrapose! hj,
      exact finset.min_le_coe_of_mem hj,
    end, hwit⟩
  else
    have hwit' : g wit < f wit := hne.lt_or_lt.resolve_left hwit,
    h_gt ⟨wit, by exact λ j hj, begin
      rw diff_comm at h,
      refine mem_diff.not_left.mp _,
      replace hj := (with_top.coe_lt_coe.mpr hj).trans_eq h.symm,
      contrapose! hj,
      exact finset.min_le_coe_of_mem hj,
    end, hwit'⟩
end) (of_lex f) (of_lex g)

instance lex.decidable_le : @decidable_rel (lex (α →₀ N)) (≤) :=
lt_trichotomy_rec
  (λ f g h, is_true $ or.inr h)
  (λ f g h, is_true $ or.inl $ congr_arg _ h)
  (λ f g h, is_false $ λ h', (lt_irrefl _ (h.trans_le h')).elim)

instance lex.decidable_lt : @decidable_rel (lex (α →₀ N)) (<) :=
lt_trichotomy_rec
  (λ f g h, is_true h)
  (λ f g h, is_false h.not_lt)
  (λ f g h, is_false h.asymm)

/--  The linear order on `finsupp`s obtained by the lexicographic ordering. -/
instance lex.linear_order : linear_order (lex (α →₀ N)) :=
{ le_total := lt_trichotomy_rec
    (λ f g h, or.inl h.le)
    (λ f g h, or.inl h.le)
    (λ f g h, or.inr h.le),
  decidable_lt := by apply_instance,
  decidable_le := by apply_instance,
  decidable_eq := by apply_instance,
  ..lex.partial_order }

There's one obvious duplication there that would be solved either by wit or more API for diff

[adomani]

@eric-wieser, if you are happy with this version feel free to push it!

I am partly in favour of wit since it is a common way of arguing: you want to prove something, you find a minimal representative where you can test what happens and you decide your statement there. I agree that wit probably does not achieve this in a very general way.

Also, my eventual goal is to be able to prove that several add_monoid_algebras have no zero-divisors and the linear order is just a convenient tool that will actually self-eliminate from the final statement: the order on the source of the finsupp is completely arbitrary, while the order on the target is tied in with covariant assumptions. Since the target is nat in cases of interest, this is ok. For the source, I simply plan to take any linear order on the source, as this is all that is needed.

[eric-wieser]

I've pushed a slightly cleaner version.

I think the problem with your wit is that it has to repeatedly deal with a junk value that doesn't make anything easier. It's not really much more work to write (f.diff g).min or (f.diff g).min' or whatever variant of junk-handling the user actually wants, and the spelling is arguably still very readable.

[adomani]

@eric-wieser, do you mind if I PR the finset.lattice lemmas separately? I am about to open a PR with a proof of covariance that does not use wit (and is much simpler than I thought), so those lemmas would have to be part of the other PR as well.

[adomani]

This PR has been essentially replaced by #16127.