Proving refinement is a partial order

Stream: new members

[VayusElytra]

Hi!
I have a decomposition structure which is such that an object S : Decomp n for some natural number n corresponds to a way of writing n as a sum of integers. To implement this, S has as field a multiset DecompMultiset representing the integers in the decomposition. (There should of course be a proof that the sum of those numbers is actually n, but I am leaving this aside for this question).

From there, I define a relation on decompositions in the following way: if S and T are both decompositions of n, then T refines S if every integer in S.DecompMultiset is a sum of integers in T.DecompMultiset. For instance, {1,1,3} can be refined into {1,1,1,2}.

Question now: I am having a lot of issues proving that this relationship is transitive, so if T refines S and U refines T, then U refines S. Each element in S corresponds to a sub-multiset in T, and each element in these sub-multisets yields another sub-multiset in U. I think it would be sufficient to take the disjoint union of all these objects, but it is really unclear to me how to actually implement this. What is the clever way of accessing all these subsets and indexing them so i can build a disjoint union?

MWE for reference:

structure Decomp (n : ℕ) where
  DecompMultiset : Multiset ℕ
  --there would of course be a 2nd property here to express that n is the sum of the elements
  --in the multiset

variable (n : ℕ)

def Refinement n (S₁ : Decomp n) (S₂ : Decomp n) : Prop :=
  ∀ k ∈ S₁.DecompMultiset, (∃ Ssub : Decomp k, Ssub.DecompMultiset ⊆ S₂.DecompMultiset)

lemma RefinementTrans (S₁ : Decomp n) (S₂ : Decomp n) (S₃ : Decomp n)
  (h₁ : Refinement n S₁ S₂) (h₂ : Refinement n S₂ S₃) : Refinement n S₁ S₃ := by
  rw[Refinement]
  rw[Refinement] at h₁
  rw[Refinement] at h₂ --doing this thrice is very inelegant...
  intro k hmem
  sorry

[Etienne Marion]

I’ve never used multisets, but from what I gathered in the docs, it seems to me that what you actually need is docs#Multiset.add and docs#Multiset.Le.

[VayusElytra]

For Le, this seems like a different partial order than the one I am working with. In my case, {1,1,3} > {1,1,1,2}, but these sets have no relation between them in the partial order from the documentation.

For add: this makes sense. How can I take a binary operation like this add and sum way more than 2 things?

[Etienne Marion]

I meant that your Refinement statement should be stated I think with Le rather than inclusion, namely Ssub.DecompMultiset ≤ S₂.DecompMultiset. As an addition is defined and it gives some structure, you should be able to write finite sums using ∑.

[Etienne Marion]

Is {1,2} supposed to be a refinement of {1,3}? Because it is in the Lean definition.

[Etienne Marion]

And in that case, {1,1} is a refinement of {1,2}, but not of {1,3}. So I don't think the definition you wrote in Lean is transitive.

[VayusElytra]

No - that would be excluded by the other condition, which I did not take the time to write out here but probably should have. In this case, {1,3} is a decomposition of 4, and {1,2} would be a decomposition of 3, so they would not be of compatible types for Lean.

[VayusElytra]

Thank you for the comment on multiset addition, that makes a lot of sense. One additional question if that's OK: the ∑ symbol is already defined, so this is easy to deal with, but I have been in situations in the past where I had some hand-made binary operation that I needed to be able to define for large finite sets, and for which Lean had no pre-written code. In that case, what is the correct approach to define these repeated operations?

[Etienne Marion]

docs#Multiset.sum and docs#Finset.sum are available as long as you proved an AddCommMonoid instance on the type where you take the sum. The ∑ symbol is a notation for docs#Finset.sum. In the case of multisets for example, this instance is docs#Multiset.instOrderedCancelAddCommMonoid (from which Lean automatically deduces AddCommMonoid by typeclass inference).

[Etienne Marion]

Note that Multiset.sum and Finset.sum work differently. The latter takes the sum of the values taken by a function, while the former computes the sum of the elements in the multiset (counting multiplicity).

[VayusElytra]

Thank you very much, I'll look into this properly! That's very helpful to know!

[Etienne Marion]

You’re welcome!

[Etienne Marion]

Oh also, about the three rw, you can use rw [Refinement] at *, which will rewrite in the goal and all the hypotheses. More generally, rw [...] at h1 h2 ... hn will rewrite at the given hypotheses.