Adding a keyed locking layer to fperm

Author: CohenCyril

finperm.v

@@ -97,7 +97,7 @@ Elpi mlock Definition fperm_one {T} : {fperm T} :=
   @FPerm T [fsfun] (@fperm_one_subproof T).
 Notation "1" := fperm_one : fperm_scope.
 
-Section BuildAndRenaming.
+Section InverseTheory.
 Variable T : choiceType.
 Implicit Types (s : {fperm T}) (x : T) (X Y : {fset T}) (f : T -> T).
 
@@ -113,17 +113,31 @@ move=> /eqP e; apply/eqP/fpermP=> x; rewrite fperm1; case: (finsuppP s) => //.
 by rewrite e in_fset0.
 Qed.
 
-Definition fperm_def (X : {fset T}) (f : T -> T) x :=
+End InverseTheory.
+
+Definition fperm_def {T} (X : {fset T}) (f : T -> T) (x : T) :=
   let Y1 : {fset T} := [fset f x | x in X] `\` X in
   let Y2 : {fset T} := X `\` [fset f x | x in X] in
   if x \in Y1 then nth x Y2 (index x Y1) else f x.
 
-Definition fperm X f :=
-  odflt 1 (insub [fsfun x in (X `|` f @` X) => fperm_def X f x]).
+Elpi mlock Definition fperm_keyed (key : unit) {T} X f :=
+  odflt 1 (insub [fsfun x in (X `|` f @` X) => @fperm_def T X f x]).
+
+Arguments fperm_keyed key {T} X f.
+
+Fact default_key : unit. Proof. by []. Qed.
+Notation fperm := (@fperm_keyed default_key).
+
+Section BuildAndRename.
+Variable T : choiceType.
+Implicit Types (s : {fperm T}) (x : T) (X Y : {fset T}) (f : T -> T).
+
+Lemma fperm_default_key k : @fperm_keyed k = @fperm.
+Proof. by rewrite !unlock. Qed.
 
-Lemma fpermE f X : {in X &, injective f} -> {in X, fperm X f =1 f}.
+Lemma fpermE k f X : {in X &, injective f} -> {in X, fperm_keyed k X f =1 f}.
 Proof.
-move=> /card_in_imfsetP inj; rewrite /fperm insubT /=; last first.
+move=> /card_in_imfsetP inj; rewrite unlock insubT /=; last first.
   by move=> _ x x_X; rewrite fsfunE in_fsetU /fperm_def /= in_fsetD x_X.
 set D := X `|` _; apply/fsinjectivebP; exists D; rewrite ?finsupp_sub //.
 rewrite /fperm_def; set Y1 := f @` X `\` X; set Y2 := X `\` f @` X.
@@ -151,23 +165,27 @@ rewrite !fsfunE x_D y_D; case: ifPn => x_Y1; case: ifPn => y_Y1.
 - by apply: (card_in_imfsetP _ _ inj); rewrite nY1_X.
 Qed.
 
-Lemma finsupp_fperm f X : finsupp (fperm X f) `<=` X `|` f @` X.
+Lemma finsupp_fperm k f X : finsupp (fperm_keyed k X f) `<=` X `|` f @` X.
 Proof.
-rewrite /fperm; case: insubP => /= [g _ ->|_]; first exact: finsupp_sub.
+rewrite fperm_keyed.unlock; case: insubP => /= [g _ ->|_].
+  exact: finsupp_sub.
 by rewrite finsupp1 fsub0set.
 Qed.
 
-Lemma fpermEst f X x : f @` X = X -> fperm X f x = if x \in X then f x else x.
+Lemma fpermEst k f X x : f @` X = X ->
+  fperm_keyed k X f x = if x \in X then f x else x.
 Proof.
 move=> st; case: ifPn=> /= [|x_nin].
   by apply/fpermE/card_in_imfsetP/eqP; rewrite st.
-suff: x \notin finsupp (fperm X f) by case: finsuppP.
+suff: x \notin finsupp (fperm_keyed k X f) by case: finsuppP.
 apply: contra x_nin; apply/fsubsetP.
 by rewrite -{2}[X]fsetUid -{3}st finsupp_fperm.
 Qed.
 
+Fact rename_key : unit. Proof. by []. Qed.
+
 Definition fperm_rename (X Y : {fset T}) : {fperm T} :=
-  fperm X (fun x => nth x Y (index x X)).
+  @fperm_keyed rename_key T X (fun x => nth x Y (index x X)).
 
 Lemma fperm_renameP X Y :
   let s := fperm_rename X Y in
@@ -185,11 +203,19 @@ have im_f: f @` X = Y.
       by rewrite mem_nth // size_X index_mem.
     by rewrite /f nthK ?fset_uniq //= ?inE ?size_X ?index_mem // nth_index.
   by case/imfsetP: y_in => x /= x_in ->; rewrite mem_nth // -size_X index_mem.
-rewrite -im_f; split; first by rewrite finsupp_fperm.
+rewrite -im_f; split; first by rewrite  finsupp_fperm.
 by apply: eq_in_imfset; apply: fpermE.
 Qed.
 
-End BuildAndRenaming.
+End BuildAndRename.
+
+Elpi mlock Definition fperm_mul {T} (s1 s2 : {fperm T}) :=
+  fperm (finsupp s1 `|` finsupp s2) (s1 \o s2).
+Infix "*" := fperm_mul : fperm_scope.
+
+Elpi mlock Definition fperm_exp {T} (s : {fperm T}) n :=
+  iter n (fperm_mul s) 1.
+Infix "^+" := fperm_exp : fperm_scope.
 
 Section InverseSubDef.
 Variable T : choiceType.
@@ -209,24 +235,13 @@ apply/fsetP=> x; apply/(sameP idP)/(iffP idP).
 by case/imfsetP=> [y Py -> {x}]; case: pickP => /=.
 Qed.
 
-Fact fperm_mul_key : unit. exact: tt. Qed.
-
 End InverseSubDef.
 
-Elpi mlock Definition fperm_mul {T} (s1 s2 : {fperm T}) :=
-  fperm (finsupp s1 `|` finsupp s2) (s1 \o s2).
-Infix "*" := fperm_mul : fperm_scope.
-
 Elpi mlock Definition fperm_inv {T} (s : {fperm T}) :=
   fperm (finsupp s) (fun x => oapp val x [pick y : finsupp s | x == s (val y)]).
 Notation "x ^-1" := (fperm_inv x) : fperm_scope.
 
-Elpi mlock Definition fperm_exp {T} (s : {fperm T}) n :=
-  iter n (fperm_mul s) 1.
-Infix "^+" := fperm_exp : fperm_scope.
-
-
-Section Inverse.
+Section InverseTheory.
 Variable T : choiceType.
 Implicit Types (x : T) (X Y : {fset T}).
 Variable (s : {fperm T}).
@@ -259,9 +274,9 @@ Qed.
 Lemma fperm_finsuppV x : (s^-1 x \in finsupp s) = (x \in finsupp s).
 Proof. by rewrite -{1}finsupp_inv fperm_finsupp finsupp_inv. Qed.
 
-End Inverse.
+End InverseTheory.
 
-Section Multiplication.
+Section Operations.
 Variable T : choiceType.
 Implicit Types (s : {fperm T}) (x : T) (X Y : {fset T}).
 Local Notation "1" := (1 : {fperm T}).
@@ -379,7 +394,8 @@ case/imfsetP=> [w /fset2P [->|->] ->] /=; rewrite eqxx ?fset22 //.
 case: ifP=> ?; by [apply fset21|apply fset22].
 Qed.
 
-Definition fperm2 x y := fperm [fset x; y] (fperm2_def x y).
+Fact fperm2_key : unit. Proof. by []. Qed.
+Definition fperm2 x y := fperm_keyed fperm2_key [fset x; y] (fperm2_def x y).
 
 Lemma fperm2E x y : fperm2 x y =1 [fun z => z with x |-> y, y |-> x].
 Proof.
@@ -529,11 +545,9 @@ elim: n => /= [|n IH]; rewrite ?fperm_exp0 ?finsupp1 // fperm_expSl.
 by rewrite (fsubset_trans (finsupp_mul _ _)) // fsubUset fsubset_refl /=.
 Qed.
 
-End Multiplication.
-
-Prenex Implicits fperm_inv fperm_mul fperm2.
-
+End Operations.
 
+Prenex Implicits fperm2.
 
 Section Extend.