Some finmap/multiset lemmas that might be useful

[mituharu]

Hello,

Through an experimental formalization of well-foundedness of multiset ordering, I found the following finmap/multiset lemmas convenient. Some of them might also be useful for general use.

(Update: proofs are slightly simplified. Previously I didn't notice mset1D1.)

Section BigFSetExt.

Local Open Scope fset_scope.

Variable (R : Type) (idx : R) (op : Monoid.com_law idx).

Lemma big_fincl (T : choiceType) (A B : {fset T}) (AsubB : A `<=` B)
      (P : pred B) (F : B -> R) :
  \big[op/idx]_(a : A | P (fincl AsubB a)) F (fincl AsubB a) =
  \big[op/idx]_(b : B | P b && (val b \in A)) F b.
Proof.
  have [Aisfset0 | [d dinA]] := fset_0Vmem A.
  - rewrite !big_pred0 //= => [b | a]; first by rewrite Aisfset0 inE andbF.
    by have := valP a; rewrite [X in _ \in X]Aisfset0 inE.
  - rewrite (reindex (fincl AsubB)).
    + by apply: eq_bigl => /= a; rewrite (valP a) andbT.
    + exists (fun b : B => insubd [` dinA] (val b)) => /= [a _ | a].
      * by apply: val_inj; rewrite val_insubd (valP a).
      * rewrite inE => /andP [_ vainA]; apply: val_inj.
        by rewrite /= val_insubd vainA.
Qed.

End BigFSetExt.


Section BigMSet.
Variable (R : Type) (idx : R) (op : Monoid.law idx).

Lemma big_mset0 (T : choiceType) (P : pred _) (F : _ -> R) :
  \big[op/idx]_(i : @mset0 T | P i) F i = idx :> R.
Proof. by apply: big_pred0 => -[j hj]; have := hj; rewrite in_mset0. Qed.

End BigMSet.


Section MSetTheoryExt.

Local Open Scope fset_scope.
Local Open Scope mset_scope.
Local Open Scope nat_scope.

Context {K : choiceType}.
Implicit Types (a b c : K) (A B C : {mset K}).

Lemma msub1set A a : ([mset a] `<=` A) = (a \in A).
Proof.
  apply/msubsetP/idP; first by move/(_ a); rewrite msetnxx in_mset.
  by move=> ainA b; rewrite msetnE; case: eqP => // ->; rewrite -in_mset.
Qed.

Lemma msetDBA A B C : C `<=` B -> A `+` B `\` C = (A `+` B) `\` C.
Proof.
  by move=> /msubsetP CB; apply/msetP=> a; rewrite !msetE2 addnBA.
Qed.

Lemma mset_0Vmem A : (A = mset0) + {x : K | x \in A}.
Proof.
  have [/fsetP Aisfset0 | [a ainA]] := fset_0Vmem A; last by right; exists a.
  left; apply/msetP => a; rewrite mset0E; apply/mset_eq0P.
  by rewrite Aisfset0 inE.
Qed.

Definition msetsize A := \sum_(a : A) A (val a).

Lemma msetsize0 : msetsize mset0 = 0.
Proof. exact: big_mset0. Qed.

Lemma msetsize_eq0 A : (msetsize A == 0) = (A == mset0).
Proof.
  rewrite sum_nat_eq0.
  apply/forallP/eqP => /= [Ax | -> a]; last by have := valP a; rewrite in_msetE.
  apply/msetP => a; rewrite mset0E; apply/mset_eq0P/negP => ainA.
  by have := Ax [` ainA] => /=; rewrite mset_eq0 ainA.
Qed.

Lemma msetsize1D a A : msetsize (a +` A) = (msetsize A).+1.
Proof.
  pose ainaA := [` mset1D1 a A].
  rewrite /msetsize (bigD1 ainaA) //= mset1DE eqxx add1n addSn; congr S.
  rewrite [X in _ + X](_ : _ = \sum_(b : a +` A | (b != ainaA) && (val b \in A))
                                A (val b)); last first.
  - apply: eq_big => a0; last by rewrite -!val_eqE /= mset1DE => /negbTE ->.
    by have := valP a0; rewrite -!val_eqE /= in_msetE; case: (val a0 == a).
  - have AsubaA: (A `<=` a +` A)%fset
      by apply/fsubsetP => a0; rewrite in_msetE => ->; rewrite orbT.
    have [ainA | aninA] := boolP (a \in A).
    + rewrite (bigD1 [` ainA]) //=; congr addn.
      by rewrite -big_fincl /=; apply: eq_bigl => a0; rewrite -!val_eqE.
    + rewrite (mset_eq0P aninA) add0n -big_fincl /=; apply: eq_bigl => a0.
      by rewrite -val_eqE /=; apply: contraNneq aninA => <-; apply: valP.
Qed.

Lemma mset_ind P:
  P mset0 -> (forall a A, P A -> P (a +` A)) -> forall A, P A.
Proof.
  move=> base step A.
  elim: {A}(msetsize A) {-2}A (erefl (msetsize A)) => [|n IHn] A.
  - by move/eqP; rewrite msetsize_eq0 => /eqP ->.
  - have [-> | [a ainA]] := mset_0Vmem A; first by rewrite msetsize0.
    by rewrite -(msetB1K _ _ ainA) msetsize1D => -[] /IHn; apply: step.
Qed.

Lemma msubset_ind B P:
  P B -> (forall A a, B `<=` A -> P A -> P (a +` A)) ->
  forall A, B `<=` A -> P A.
Proof.
  move=> base step A.
  elim/mset_ind: {A}(A `\` B) {-2}A (erefl (A `\` B)) => [| a D IH] A.
  - move/eqP. rewrite msetB_eq0 => AsubB BsubA.
    by rewrite (_ : A = B) //; apply/eqP; rewrite eqEmsubset AsubB BsubA.
  - move=> AdiffB BsubA.
    have: a \in A by rewrite -(msetBDKC _ _ BsubA) AdiffB in_msetE mset1D1 orbT.
    move/msetB1K => <-.
    have BsubAa: B `<=` A `\ a.
    + rewrite -(msetBBK _ _ BsubA); apply: msetBS.
      by rewrite AdiffB msub1set mset1D1.
    + apply: step => //; apply: IH => //.
      by rewrite -(msetD1K a D) -AdiffB -!msetBDA [in LHS]msetDC.
Qed.

End MSetTheoryExt.

[CohenCyril]

Thank you for this. I might integrate some of your suggestions.
However, I am not in favour of introducting elimination lemmas on multisets, as I think an induction on the size of the multiset is always more general and more elementary.
Also, I am not yet sure I wish to introduce a specific msetsize operator...

[mituharu]

Thank you for the response.

This is not related to the original issue, but I have a quick question about finmap.v.
Is seq_fset for public use? I used [fsetval x : seq_sub s] instead of seq_fset s in my script because seq_fset is not listed in the comment at the beginning of finmap.v. But the latter looks more natural and simpler to work with.