Stream: math-comp users

Topic: case-analysis on element of union of finite sets


view this post on Zulip Ricardo (Dec 26 2022 at 23:05):

Hi. I have a variable in the context of the form k': domf aFinmap and I know from a lemma that domf aFinmap = aFinset1 `|` aFinset2. I'd like to work separately on the case where k': aFinset1 and the case k': aFinset2. Would that be possible? How?

The full code I'm working on at the moment is the following.

From mathcomp Require Import ssreflect ssrbool ssrnat ssrfun eqtype choice fintype seq finfun finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module ContactGraphs.
Coercion fset_sub_finType : finSet >-> finType.
Local Open Scope fset.
Local Open Scope fmap.
Section FinMap.
Variables (K V : choiceType).

Definition setks (m : {fmap K -> V}) (ks : {fset K}) (v : V) :=
  [fmap k : ks `|` domf m =>
     if val k \in ks then v
     else odflt v (fnd m (val k))].

Lemma setksD (m : {fmap K -> V}) (ks : {fset K}) (v : V) :
  domf (setks m ks v) = ks `|` domf m.
Proof using Type. done. Qed.

Lemma setksC (m : {fmap K -> V}) (ks : {fset K}) (v : V) :
  ks != fset0 ->
  codomf (setks m ks v) = v |` codomf m.[\ ks].
Proof using Type.
  move=> /fset0Pn [k k_in_ks].
  apply/fsetP=> v'. rewrite !inE.
  case H: [exists x, setks m ks v x == v'].
  move: H => /existsP [k' H'].
Admitted.

view this post on Zulip Laurent Théry (Dec 27 2022 at 17:40):

The problem is that aFInset1 and aFinset1 | aFinset2 are two different types, so you will need to do a lot of surgeries maybe you could use concatenation f + g to make your life easier.

view this post on Zulip Karl Palmskog (Dec 27 2022 at 17:44):

I have some operations/results on enlarging finmaps via concatenation here, maybe a small chance they could be helpful: https://github.com/runtimeverification/algorand-verification/blob/master/theories/fmap_ext.v

view this post on Zulip Laurent Théry (Dec 28 2022 at 01:30):

using concatenation here what I could get :

Definition setks (m : {fmap K -> V}) (ks : {fset K}) (v : V) :=
  m + [fmap _ : ks  => v].

Lemma setksD (m : {fmap K -> V}) (ks : {fset K}) (v : V) :
  domf (setks m ks v) = ks `|` domf m.
Proof using Type. by rewrite domf_cat fsetUC. Qed.

Lemma setksC (m : {fmap K -> V}) (ks : {fset K}) (v : V) :
  ks != fset0 ->
  codomf (setks m ks v) = v |` codomf m.[\ ks].
Proof using Type.
move=> /fset0Pn [k k_in_ks]; rewrite /setks.
apply/fsetP=> v'; rewrite ![RHS]inE.
apply/codomfP/orP => [[x /fndSomeP[xI]]|[]].
- have [xIks|xNIks] := (boolP (x \in ks)).
    by rewrite getf_catr // ffunE => ->; left; rewrite inE.
  rewrite getf_catl // => [|x1 <-].
    by rewrite !inE (negPf xNIks) orbF in xI.
  right.
  apply/codomfP; exists x.
  rewrite fnd_rem (negPf xNIks).
  by apply/fndSomeP; exists x1.
- rewrite inE => /eqP->.
  exists k.
  rewrite fnd_cat k_in_ks.
  by apply/fndSomeP; exists k_in_ks; rewrite ffunE.
move=> /codomfP[x].
rewrite fnd_rem.
case: (boolP (_ \in _)) => // xNIks /fndSomeP[xIm <-].
exists x; apply/fndSomeP.
have xH : x \in domf (m + [fmap _ : ks => v]) by rewrite inE xIm.
by exists xH; rewrite getf_catl.
Qed.

hope this helps.

view this post on Zulip Laurent Théry (Dec 28 2022 at 01:41):

Maybe the general statement that is missing from the library is

Lemma codomf_cat (f g : {fmap K -> V}) :
  codomf (f + g) = codomf g `|` codomf f.[\domf g].
Proof.
apply/fsetP=> v'; rewrite ![RHS]inE.
apply/codomfP/orP => [[x /fndSomeP[xI]]|[]].
- have [xIg|xNIg] := (boolP (x \in domf g)).
    by rewrite getf_catr // => <-; left; rewrite in_codomf.
  rewrite getf_catl // => [|x1 <-].
    by rewrite !inE (negPf xNIg) orbF in xI.
  right.
  apply/codomfP; exists x.
  rewrite fnd_rem (negPf xNIg).
  by apply/fndSomeP; exists x1.
- move=> /codomfP[x /fndSomeP[xI xM]].
  exists x.
  rewrite fnd_cat xI.
  by apply/fndSomeP; exists xI.
move=> /codomfP[x].
rewrite fnd_rem.
case: (boolP (_ \in _)) => // xNIg /fndSomeP[xIm <-].
exists x; apply/fndSomeP.
have xH : x \in domf (f + g) by rewrite inE xIm.
by exists xH; rewrite getf_catl.
Qed.

view this post on Zulip Laurent Théry (Jan 02 2023 at 15:21):

For your information, codomf_cat will be in the next release of finmap

view this post on Zulip Ricardo (Jan 05 2023 at 02:14):

Thank you very much @Laurent Théry and @Karl Palmskog.

view this post on Zulip Ricardo (Jan 05 2023 at 02:21):

Laurent Théry said:

For your information, codomf_cat will be in the next release of finmap

That's great news :smile:

view this post on Zulip Ricardo (Jan 05 2023 at 03:02):

With the new codomf_cat lemma and a codomf_const lemma that I wrote I can solve the setksC lemma in one line.

From mathcomp Require Import ssreflect ssrbool ssrnat ssrfun eqtype choice fintype seq finfun finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module ContactGraphs.
Lemma neqxx (T: eqType) (x : T) : ~(x != x).
Proof. move=> /eqP xNEx. by apply: xNEx. Qed.
Section FinMap.
Variables (K V : choiceType).

Lemma codomf_cat (f g : {fmap K -> V}) :
  codomf (f + g) = codomf g `|` codomf f.[\domf g].
Proof using Type.
  apply/fsetP => v. rewrite ![RHS]inE.
  apply/codomfP/(orPP (codomfP _ _) (codomfP _ _)); last first.
  - move=> [] [x xI]; exists x; rewrite fnd_cat.
    + by case: fndP xI.
    + move: xI. rewrite fnd_rem. by case: ifP.
  - move=> [] x. rewrite fnd_cat. case: fndP => // [xg gx|xNg fx].
    + left. exists x. by rewrite in_fnd.
    + right. exists x. by rewrite fnd_rem ifN.
Qed.

Definition setks (m : {fmap K -> V}) (ks : {fset K}) (v : V) :=
  m + [fmap _ : ks => v].

Lemma codomf_const (ks : {fset K}) (v : V) :
  ks != fset0 -> codomf [fmap _ : ks => v] = [fset v].
Proof using Type.
  move=> /fset0Pn [k k_in_ks].
  apply/fsetP=> x. rewrite !inE. apply/existsP.
  case: (boolP (x == v)) => [/eqP-> | xNEv] /=.
  - exists [` k_in_ks]. by rewrite ffunE.
  - move=> [x' /eqP H]. rewrite ffunE in H.
    rewrite H in xNEv. by apply: (@neqxx _ x).
Qed.

Lemma setksC (m : {fmap K -> V}) (ks : {fset K}) (v : V) :
  ks != fset0 ->
  codomf (setks m ks v) = v |` codomf m.[\ ks].
Proof using Type.
  move=> H. by rewrite codomf_cat codomf_const.
Qed.

The last bit in the proof of codomf_const doesn't look very elegant but it works :smile:

Side question: why do I have to use Proof using Type in Sections?


Last updated: Jul 15 2024 at 20:02 UTC