Dershowitz-Manna Ordering theorem

Stream: new members

[Haitian Wang]

Hi there! I'm Haitian, a PhD student working with @Malvin Gattinger at ILLC, University of Amsterdam, on a Lean4 project involving the formalization of the interpolation property of PDL. As part of our work, we've developed a formal proof of the Dershowitz-Manna theorem on Multiset ordering, which is often used for proving program termination. You can find our proof here: (https://github.com/m4lvin/lean4-pdl/blob/dmnew/Pdl/MultisetOrder.lean).

Our goal is to contribute this theorem to mathlib, but before we do, we want to ensure it meets the necessary standards. We're aware that some cleaning up is required and have a few questions:

1. Firstly, Malvin previously asked about contributing a theorem to mathlib, only to discover it already existed under a different name. So, it would be helpful if you could confirm that the Dershowitz-Manna theorem has not already been added to mathlib.
2. Assuming it hasn't been formalized yet, where should we place this proof within mathlib's structure? Something like Mathlib.Data.Multiset.Order?
3. Is it necessary to replace all instances of aesop with explicit proofs?

Any insights or suggestions you can provide would be greatly appreciated. Looking forward to your guidance!

[Ruben Van de Velde]

I can answer 3: no, that's not necessary. You might look if any of your proofs are noticeably slow, though

[Yaël Dillies]

Nice job! And no, Dershowitz-Manna is not here :)

[Yaël Dillies]

Stupid question: Can you generalise DM to docs#Finsupp, in the sense of docs#Finsupp.toMultiset ?

[Haitian Wang]

Aha, that we haven't thought about yet. We would have a look and let you know :-)

[Malvin Gattinger]

I did not know Finsupp at all before, we will look into it :)

If this makes sense: do you mean that the theorem should be proven about Finsupp "directly" or whether we can use Finsupp.toMultiset andMultiset.toFinsupp to transfer the theorem we already have?

(Thinking aloud, the DM proof uses DecidableEq α anyway in which case Finsupp and Multiset are equivalent, right? Though I don't remember where/why exactly it is needed.)

[Malvin Gattinger]

We hope to prepare a PR for this next week. Can someone here give Haitian the access rights to push to a branch so we can get the CI checks? His GitHub username is haitian-yuki.

[Malvin Gattinger]

@Yaël Dillies sorry to bother you, but maybe you have the rights to add people to the mathlib repository?

[Johan Commelin]

Aah, sorry, I missed this request... 1 sec

[Johan Commelin]

Voila: https://github.com/leanprover-community/mathlib4/invitations

[Malvin Gattinger]

Thank you, no worries!

[Yaël Dillies]

Sorry, I do not!

[Malvin Gattinger]

There is a mathlib branch for this now: dm_ordering, linting and fixes to be done ;-)

[Malvin Gattinger]

Concerning the generalization from Multiset to Finsupp, we thought of two things:

1. Hopefully easy: via docs#Finsupp.toMultiset we can transfer the DM theorem to Finsupp α ℕ.
2. More ambitious: define the DM ordering and prove the DM theorem for Finsupp α M where M is something else than ℕ. Naively for me, we are then talking multisets where multiplicities are of type M. For the DM theorem to make sense M needs to have an order, and notions of addition and subtraction.

We may do (1) still for the PR, but I think we will not do (2) for now, as we do not even know (non-formalized) literature about this.

[Yaël Dillies]

Yes, I know (1) is easy and I know (2) is not standard

[Haitian Wang]

Hi! With some some procrastination, we made a PR here: https://github.com/leanprover-community/mathlib4/pull/14411 Suggestions welcome! Things we may consider in the future include: 1. Extend the theorem to docs#Finsupp (both (1) and (2) mentioned above if applicable). 2. Explore whether the Axiom of Choice is necessary (probably yes) in the proof.

[Yaël Dillies]

If nobody reviews by then, please ask for my review in a week

[Yaël Dillies]

(I am not available until then)

[Haitian Wang]

Hi! We followed the advice of the reviewers and made a separate PR for the (five) lemmas about multisets that are useful for proving the DM thoerem. You can already see in the first comment of the previous PR about the DM theorem that the DM PR now depends on the new PR about multiset.basics. We have a few questions though:

1. For the fourth theorem added, the linarith tactic doesn't work in the Mathlib/Data/Multiset/Basic.lean file. Is there a way to get around this? Leastways we can add it back to the DM file as a lemma specific to the proof.
2. We originally planned to add the theorems to the most appropriate places, The section Subtraction for example. However, some of the proofs require things such as the Multiset.countto be defined first. Therefore, we add them to later places where the things required are already defined, even though the theorems themselves are about subtraction mainly. Is that ok or is there a better way of doing this?

Thanks!

[Yaël Dillies]

Commented on #15645

[Haitian Wang]

Hi, is there a way to avoid the sorries below? Also, thank you @YaelDillies for your comment! But still I am not quite sure how to fix them :sweat_smile:

import Mathlib.Data.Multiset.Basic

import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax -- needed for le_or_le_of_add_le_add

theorem inter_add_sub_of_eq {α} [dec : DecidableEq α] {M N P Q: Multiset α} (h : M + N = P + Q) :
    N = N ∩ Q + (P - M) := by
  ext x
  rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]
  have h0 : M.count x + N.count x = P.count x + Q.count x := by
    rw [Multiset.ext] at h
    simp_all only [Multiset.mem_add, Multiset.count_add]

  -- The sorries below used to be "linarith", but how can we avoid it?

  -- suggestion by @YaelDillies:
  -- have := le_or_le_of_add_le_add h0.ge -- >> failed to synthesize CovariantClass ... ?

  by_cases l_u : M.count x ≤ P.count x
  · have : N.count x ≥ Q.count x := sorry
    simp_all only [ge_iff_le, min_eq_right]
    -- have := tsub_add_cancel_of_le l_u
    sorry
  · simp_all only [not_le, gt_iff_lt]
    have : Multiset.count x N ≤ Multiset.count x Q := by sorry
    have := le_of_lt l_u
    simp_all

[Andrés Goens]

This can be golfed a bit but I would just calc (they seem very reasonable, and I like calc, I think it's readable)

import Mathlib.Data.Multiset.Basic
import Mathlib.Tactic

import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax -- needed for le_or_le_of_add_le_add

theorem inter_add_sub_of_eq {α} [dec : DecidableEq α] {M N P Q: Multiset α} (h : M + N = P + Q) :
    N = N ∩ Q + (P - M) := by
  ext x
  rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]
  have h0 : M.count x + N.count x = P.count x + Q.count x := by
    rw [Multiset.ext] at h
    simp_all only [Multiset.mem_add, Multiset.count_add]

  -- The sorries below used to be "linarith", but how can we avoid it?

  -- suggestion by @YaelDillies:
  -- have := le_or_le_of_add_le_add h0.ge -- >> failed to synthesize CovariantClass ... ?

  by_cases l_u : M.count x ≤ P.count x
  · have : N.count x ≥ Q.count x := sorry
    simp_all only [ge_iff_le, min_eq_right]
    symm
    calc
      Multiset.count x Q + (Multiset.count x P - Multiset.count x M) = (Multiset.count x Q + Multiset.count x P) - Multiset.count x M := by exact Eq.symm (Nat.add_sub_assoc l_u (Multiset.count x Q))
      _ = (Multiset.count x P + Multiset.count x Q) - Multiset.count x M  := by rw [Nat.add_comm]
      _ = (Multiset.count x M + Multiset.count x N) - Multiset.count x M  := by rw [h0]
      _ = (Multiset.count x N + Multiset.count x M) - Multiset.count x M  := by rw [Nat.add_comm]
      _ = Multiset.count x N + (Multiset.count x M - Multiset.count x M) := by rw [Nat.add_sub_assoc (Nat.le_refl (Multiset.count x M))]
      _ = Multiset.count x N := by rw [Nat.sub_self, Nat.add_zero]

    -- have := tsub_add_cancel_of_le l_u
  · simp_all only [not_le, gt_iff_lt]
    have : Multiset.count x N ≤ Multiset.count x Q := by sorry
    have := le_of_lt l_u
    simp_all

[Andrés Goens]

@Haitian Wang or are you talking about the N.count x ≥ Q.count x ?

[Malvin Gattinger]

All of the sorries ;-) We were wondering if the suggestion from Yael can be used earlier already, maybe even without the by_cases l_u part.

[Andrés Goens]

hm, I see. I don't get the failed to synthesize CovariantClass, but essentially if things used to be linarith, then you should be able to reconstruct linarith's reasoning (although I'm surprised that it stops working tbf).

[Malvin Gattinger]

Ah, I only saw now that you imported Mathlib.Tactic above. Our goal is to have a proof that can become part of Mathlib.Data.Multiset.Basic so we do not want to import too much. That's probably also why you don't get the error about the missing CovariantClass instance (that I guess is only provided "later" in Mathlib).

[Andrés Goens]

Oh, I added that to try linarith, but thought I didn't need it later. I guess you want to just add the one instance (if you're importing Mathlib.Algebra.Order.Monoid.Unbundled.MinMax anyway)

[Andrés Goens]

it looks like import Mathlib.Algebra.Order.Ring.Nat is what you need to get you there

[Andrés Goens]

On the other hand, why don't you just prove it for Nats and use that?

import Mathlib.Data.Multiset.Basic

lemma version_for_nats {m n p q : Nat} (h : m + n = p + q) : n = min n q + (p - m) := sorry

theorem inter_add_sub_of_eq {α} [dec : DecidableEq α] {M N P Q: Multiset α} (h : M + N = P + Q) :
    N = N ∩ Q + (P - M) := by
  ext x
  rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]
  have h0 : M.count x + N.count x = P.count x + Q.count x := by
    rw [Multiset.ext] at h
    simp_all only [Multiset.mem_add, Multiset.count_add]
  exact (version_for_nats h0)

[Malvin Gattinger]

That helps!

import Mathlib.Data.Multiset.Basic
import Mathlib.Algebra.Order.Ring.Nat

theorem eq_min_add_sub_of_add_eq_add {m n p q : Nat} (h : m + n = p + q) : n = min n q + (p - m) := by
  by_cases m_p : m ≤ p
  · have : n ≥ q := by
      cases lt_or_le_of_add_le_add h.ge <;> simp_all only [ge_iff_le]
      have := not_lt_of_le m_p
      tauto
    simp_all only [ge_iff_le, min_eq_right]
    symm
    calc
      q + (p - m) = (q + p) - m := by exact Eq.symm (Nat.add_sub_assoc m_p q)
      _ = (p + q) - m  := by rw [Nat.add_comm]
      _ = (m + n) - m  := by rw [h]
      _ = (n + m) - m  := by rw [Nat.add_comm]
      _ = n + (m - m) := by rw [Nat.add_sub_assoc (Nat.le_refl m)]
      _ = n := by rw [Nat.sub_self, Nat.add_zero]
  · simp only [not_le, gt_iff_lt] at m_p
    have : n ≤ q := by
      have := not_lt_of_le m_p
      cases lt_or_le_of_add_le_add h.le <;> tauto
    have := le_of_lt m_p
    simp_all

theorem inter_add_sub_of_eq {α} [dec : DecidableEq α] {M N P Q: Multiset α} (h : M + N = P + Q) :
    N = N ∩ Q + (P - M) := by
  ext x
  rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]
  have h0 : M.count x + N.count x = P.count x + Q.count x := by
    rw [Multiset.ext] at h
    simp_all only [Multiset.mem_add, Multiset.count_add]
  exact (eq_min_add_sub_of_add_eq_add h0)

[Malvin Gattinger]

I think it would be good to update the PR with this, @Haitian Wang but I am now also wondering whether eq_min_add_sub_of_add_eq_add the right name and should we add it in another file that is only about Nat, now that it has nothing to do with Multiset? Maybe @Yaël Dillies can tell us?

[Yaël Dillies]

Data.Nat.Defs is the correct file for that

[Yaël Dillies]

Note that you will need to replace the generic typeclass-based lemmas you used by Nat-specific lemmas, which you should find mostly in Data.Nat.Defs

[Malvin Gattinger]

Ah, I see.

import Mathlib.Data.Nat.Defs

theorem eq_min_add_sub_of_add_eq_add {m n p q : Nat} (h : m + n = p + q) : n = min n q + (p - m) := by
  by_cases m_p : m ≤ p
  · have : n ≥ q := by
      sorry
      -- TOOD: replace with Nat specific lemmas!
      -- cases lt_or_le_of_add_le_add h.ge <;> simp_all only [ge_iff_le]
      -- have := not_lt_of_le m_p
      -- tauto
    simp_all only [ge_iff_le, min_eq_right]
    symm
    calc
      q + (p - m) = (q + p) - m := by exact Eq.symm (Nat.add_sub_assoc m_p q)
      _ = (p + q) - m  := by rw [Nat.add_comm]
      _ = (m + n) - m  := by rw [h]
      _ = (n + m) - m  := by rw [Nat.add_comm]
      _ = n + (m - m) := by rw [Nat.add_sub_assoc (Nat.le_refl m)]
      _ = n := by rw [Nat.sub_self, Nat.add_zero]
  · simp only [not_le, gt_iff_lt] at m_p
    have : n ≤ q := by
      have := not_lt_of_le m_p
      sorry
      -- cases lt_or_le_of_add_le_add h.le <;> tauto
    have := le_of_lt m_p
    simp_all

[Kevin Buzzard]

theorem eq_min_add_sub_of_add_eq_add {m n p q : Nat} (h : m + n = p + q) : n = min n q + (p - m) := by
  omega

[Malvin Gattinger]

Oh nice, but can we use omega if this should go into Data.Nat.Defs or as a have := claim inside Data.Multiset.Basic?

[Ruben Van de Velde]

I assume so

[Malvin Gattinger]

Ah, cool, I did not know that omega is from Lean itself and thus available without any import.

[Malvin Gattinger]

Ah, so this should be it I guess:

import Mathlib.Data.Multiset.Basic

theorem inter_add_sub_of_eq {α} [dec : DecidableEq α] {M N P Q: Multiset α} (h : M + N = P + Q) :
    N = N ∩ Q + (P - M) := by
  ext x
  rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]
  have h0 : M.count x + N.count x = P.count x + Q.count x := by
    rw [Multiset.ext] at h
    simp_all only [Multiset.mem_add, Multiset.count_add]
  omega

[Malvin Gattinger]

The PR #14411 for this has now been merged. Congratulations to @Haitian Wang and many thanks to all who helped us on the way!