Stream: math-comp users

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

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'].
``````

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.

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

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.

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.
``````

Laurent Théry (Jan 02 2023 at 15:21):

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

Ricardo (Jan 05 2023 at 02:14):

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

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:

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 `Section`s?

Last updated: Jul 15 2024 at 20:02 UTC