port to MathComp 1.11.0

Author: palmskog

Core/StatePredicates.v

@@ -267,7 +267,7 @@ Lemma has_all_true xs (ps : seq nid) x:
   all id [seq i.2 | i <- xs] ->
   x \in ps -> (x, true) \in xs.
 Proof.
-move=>P A D; move: (perm_eq_mem P x).
+move=>P A D; move: (perm_mem P x).
 rewrite D=>/mapP[z] I Z; subst x.
 rewrite all_map/= in A; move/allP: A=>/(_ z I)/=<-.
 by rewrite -surjective_pairing.
@@ -277,7 +277,7 @@ Lemma has_some_false (xs : seq (nid * bool)) ps x:
   perm_eq [seq i.1 | i <- xs] ps ->
   x \in ps -> exists b, (x, b) \in xs.
 Proof.
-move=>P D; move: (perm_eq_mem P x).
+move=>P D; move: (perm_mem P x).
 rewrite D=>/mapP[z] I Z; subst x.
 by exists z.2; rewrite -surjective_pairing.
 Qed.

Examples/Calculator/CalculatorClientLib.v

@@ -116,7 +116,7 @@ have P3: l \in dom i2 by rewrite -(cohD(proj2(rely_coh R1)))domPt inE/=.
 rewrite (rely_loc' _ R3)/= locE// /cr_step (getStK (proj1 cohs) L1)/=.
 clear R3 Hw P1 P2 P3; exists (remove_elem rs (cl, from, (behead tms))). 
 move: (remove_elem_in rs (cl, from, (behead tms))); rewrite X.
-by rewrite perm_eq_sym=>H.
+by rewrite perm_sym=>H.
 Qed.
 
 
@@ -241,10 +241,10 @@ apply: call_rule=>//.
 clear R3=>v i5[rs'][from][args'][E5]P5 R C.  
 suff X: args = args' /\ rs' = [::] by case: X=>Z X; subst args' rs'.  
 suff X': rs' = [::].
-- subst rs'; split=>//; move/perm_eq_mem: P5=>P5. 
+- subst rs'; split=>//; move/perm_mem: P5=>P5. 
   move/P5: (cl, server, args).
   by rewrite inE eqxx inE/==>/esym/eqP; case=>_->.
-by case/perm_eq_size: P5=>/esym/size0nil. 
+by case/perm_size: P5=>/esym/size0nil. 
 Qed.
 
 (**************************************************)

Examples/SeqLib.v

@@ -29,15 +29,15 @@ rewrite inE; case: ifP=>/=; last first.
 - case/negbT/norP=>/negbTE; rewrite eq_sym=>->/negbTE Z.
   by rewrite Z in Hi; rewrite Hi.
 case/orP.
-- by move/eqP=>Z; subst e; rewrite eqxx; apply: perm_eq_refl.
+- by move/eqP=>Z; subst e; rewrite eqxx; apply: perm_refl.
 move=>Z; rewrite Z in Hi; case: ifP=>X. 
-- by move/eqP: X=>?; subst e; apply: perm_eq_refl.
+- by move/eqP: X=>?; subst e; apply: perm_refl.
 rewrite -cat1s -[x::_]cat1s-[x::xs]cat0s -[x::xs]cat1s.
-apply/perm_eqlP.
-move: (perm_catCA [::e] [::x] (remove_elem xs e))=>/perm_eqlP H1.
+apply/permPl.
+move: (perm_catCA [::e] [::x] (remove_elem xs e))=>/permPl H1.
 rewrite !cat1s in H1.
 rewrite  -(perm_cons x (e :: remove_elem xs e) xs) in Hi.
-rewrite !cat1s !cat0s; apply/perm_eqlP.
-by apply: (perm_eq_trans H1 Hi).
+rewrite !cat1s !cat0s; apply/permPl.
+by apply: (perm_trans H1 Hi).
 Qed.
 

Examples/TwoPhaseCommit/TwoPhaseCoordinator.v

@@ -137,10 +137,10 @@ case=>[[E1 P1 C1]|].
 (*--------------------------------------*)
 
 - case: to_send P1=>[|to tos Hp].
-  + by move/perm_eq_size=>/=/size0nil=>Z; rewrite Z in (PtsNonEmpty). 
+  + by move/perm_size=>/=/size0nil=>Z; rewrite Z in (PtsNonEmpty). 
 - apply: step; apply:act_rule=>j1 R1/=; split=>[|r k m[Sf]St R2]. 
   split=>//=; first by case: (rely_coh R1).
-  + split; first by split=>//; move/perm_eq_mem: Hp->; rewrite inE eqxx.
+  + split; first by split=>//; move/perm_mem: Hp->; rewrite inE eqxx.
     case: (proj2 (rely_coh R1))=>_ _ _ _/(_ l); rewrite (prEq tpc)=>C; exists C.
     left; exists e; split; last by exists d.
     by rewrite -(rely_loc' _ R1) in E1; rewrite (getStC_K _ E1).
@@ -166,7 +166,7 @@ have Pre:
    else exists ps : seq nid, loc m = st :-> (e, CSentPrep d ps) \+ log :-> lg /\ perm_eq pts (ps ++ tos)).
 - case X: ([::] == tos);[move/eqP: X=>X; subst tos; rewrite eqxx|
                          rewrite eq_sym X].
-  have Y: pts == [:: to] by rewrite (perm_eq_small _ Hp).
+  have Y: pts == [:: to] by rewrite (perm_small_eq _ Hp).
   rewrite /cstep_send/= Y in G. 
   move: (proj2 Hc)=>Y'; rewrite Y' in G=>{Y'}.
   rewrite [cn_safe_coh _ ](pf_irr _ C) E1' in G. (* TADA! *)
@@ -179,7 +179,7 @@ have Pre:
 - exists [:: to]; split; last by rewrite cat_cons/=.
   have Y: pts == [:: to] = false.
   + apply/negP=>/eqP Z; rewrite Z in Hp.
-    move/perm_eq_size: (Hp).
+    move/perm_size: (Hp).
     move => F.
     apply sym_eq in F.
     move: F.
@@ -215,12 +215,12 @@ have Y: exists to tos, to_send = to :: tos.
 case: Y=>to[tos] Z; subst to_send=>{X}.
 - apply: step; apply:act_rule=>j1 R1/=; split=>[|r k m[Sf]St R2]. 
   split=>//=; first by case: (rely_coh R1).
-  + split; first by split=>//; move/perm_eq_mem: Hp->;
+  + split; first by split=>//; move/perm_mem: Hp->;
                     rewrite mem_cat orbC inE eqxx.
     case: (proj2 (rely_coh R1))=>_ _ _ _/(_ l); rewrite prEq=>C; exists C.
     right; exists e, d, ps; split=>//.
       by rewrite -(rely_loc' _ R1) in E1; rewrite (getStC_K _ E1).
-  + move/perm_eq_uniq: Hp; rewrite Puniq.
+  + move/perm_uniq: Hp; rewrite Puniq.
     move => F.
     apply sym_eq in F.
     move: F.
@@ -257,8 +257,8 @@ suff Pre:
     rewrite /cstep_send/= (proj2 Hc)/= in G.
     rewrite [cn_safe_coh _ ](pf_irr _ C) E1' in G.
   have Y: perm_eq (to :: ps) pts.
-    rewrite (perm_eq_sym pts) in Hp.
-    by apply/perm_eqlE; rewrite -cat1s perm_catC; apply/perm_eqlP. 
+    rewrite (perm_sym pts) in Hp.
+    by apply/permEl; rewrite -cat1s perm_catC; apply/permPl. 
   rewrite Y/= in G.     
   rewrite (rely_loc' l R2); subst k; rewrite locE; last apply: (cohVl C).
   + by rewrite -(pf_irr (cn_in cn pts others) (cn_this_in _ _))
@@ -269,11 +269,11 @@ suff Pre:
 rewrite /cstep_send/= (proj2 Hc)/= in G.
 rewrite [cn_safe_coh _ ](pf_irr _ C) E1' in G.
 have Y : perm_eq (to :: ps) pts = false.
-- apply/negP=>Hp'; move: (perm_eq_trans Hp' Hp).
+- apply/negP=>Hp'; move: (perm_trans Hp' Hp).
   rewrite -[to::ps]cat1s -[to::tos]cat1s.
-  move/perm_eqlE: (perm_catC ps [::to])=>Hs.
-  move/(perm_eq_trans Hs); rewrite -[_++[::_]]cats0 catA perm_cat2l.
-  move/perm_eq_size.
+  move/permEl: (perm_catC ps [::to])=>Hs.
+  move/(perm_trans Hs); rewrite -[_++[::_]]cats0 catA perm_cat2l.
+  move/perm_size.
   move => F.
   apply sym_eq in F.
   move: F.
@@ -283,7 +283,7 @@ rewrite (rely_loc' l R2); subst k; rewrite locE; last apply: (cohVl C).
   + rewrite -(pf_irr (cn_in cn pts others) (cn_this_in _ _))
                (getStL_Kc _ (cn_in cn pts others) E1); exists (to::ps).
     split=>//; move: Hp.
-    by rewrite -cat_rcons -cat1s -!catA !(perm_eq_sym pts) -perm_catCA catA cats1. 
+    by rewrite -cat_rcons -cat1s -!catA !(perm_sym pts) -perm_catCA catA cats1. 
   + by rewrite -(cohD (proj2 (rely_coh R1)))/ddom domPt inE/=.
   by apply: (cohS (proj2 (rely_coh R1))).   
 Qed.
@@ -472,12 +472,12 @@ have Pre: Actions.send_act_safe W (p:=tpc) cn l
     by rewrite -(cohD (proj2 (rely_coh R2)))/ddom domPt inE/=.
   case: (proj2 (rely_coh R2))=>_ _ _ _/(_ l); rewrite prEq=>C; split.
   + split=>//; case: H; first by case=>?[_]<-; rewrite inE eqxx.
-    by case=>ps[_]/perm_eq_mem->; rewrite mem_cat orbC inE eqxx.
+    by case=>ps[_]/perm_mem->; rewrite mem_cat orbC inE eqxx.
   exists C; case:H=>[[res][P1]P2 P3|[ps][P1 P2]];[left|right];  
   rewrite -(rely_loc' _ R2) in P1; rewrite (getStC_K _ P1);
   first by exists e, d, res=>//.
   exists e, d, ps; split=>//.
-  move/perm_eq_uniq: P2; rewrite Puniq.
+  move/perm_uniq: P2; rewrite Puniq.
   move => F.
   apply sym_eq in F.
   move: F.
@@ -512,21 +512,21 @@ rewrite (getStC_K _ E1) (getStL_Kc _ _ E1)
         /cstep_send Tp in G.
 have X: perm_eq (to :: ps) pts = (tos == [::]).
 - apply/Bool.eq_iff_eq_true; split.
-  + move=>Hp'; move: (perm_eq_trans Hp' P2).
+  + move=>Hp'; move: (perm_trans Hp' P2).
     rewrite -[to::ps]cat1s -[to::tos]cat1s.
-    move/perm_eqlE: (perm_catC ps [::to])=>Hs.
-    move/(perm_eq_trans Hs); rewrite -[_++[::_]]cats0 catA perm_cat2l.
-    move/perm_eq_size.
+    move/permEl: (perm_catC ps [::to])=>Hs.
+    move/(perm_trans Hs); rewrite -[_++[::_]]cats0 catA perm_cat2l.
+    move/perm_size.
     move => F.
     apply sym_eq in F.
     move: F.
     by move/size0nil=>Z; subst tos. 
-  move/eqP=>Z; subst tos; rewrite perm_eq_sym; apply: (perm_eq_trans P2).
-  by apply/perm_eqlE; move: (perm_catC ps [:: to]).
+  move/eqP=>Z; subst tos; rewrite perm_sym; apply: (perm_trans P2).
+  by apply/permEl; move: (perm_catC ps [:: to]).
 rewrite X in G=>{X}; subst i3.
 rewrite locE//; [|by apply: (cohS C2)|by apply: (cohVl C2')].
 case:ifP=>->//; exists (to :: ps);split=>//.
-apply: (perm_eq_trans P2); apply/perm_eqlE.
+apply: (perm_trans P2); apply/permEl.
 by rewrite -[to::ps]cat1s -[to::tos]cat1s -!catA perm_catCA.
 Qed.
 
@@ -585,12 +585,12 @@ have Pre: Actions.send_act_safe W (p:=tpc) cn l
     by rewrite -(cohD (proj2 (rely_coh R2)))/ddom domPt inE/=.
   case: (proj2 (rely_coh R2))=>_ _ _ _/(_ l); rewrite prEq=>C; split.
   + split=>//; case: H; first by case=>?[_]<-; rewrite inE eqxx.
-    by case=>ps[_]/perm_eq_mem->; rewrite mem_cat orbC inE eqxx.
+    by case=>ps[_]/perm_mem->; rewrite mem_cat orbC inE eqxx.
   exists C; case:H=>[[res][P1]P2 P3|[ps][P1 P2]];[left|right];
   rewrite -(rely_loc' _ R2) in P1; rewrite (getStC_K _ P1);
   first by exists e, d, res=>//.
   exists e, d, ps; split=>//.
-  move/perm_eq_uniq: P2; rewrite Puniq.
+  move/perm_uniq: P2; rewrite Puniq.
   move => F.
   apply sym_eq in F.
   move: F.
@@ -627,21 +627,21 @@ rewrite (getStC_K _ E1) (getStL_Kc _ _ E1)
         /cstep_send Tp in G.
 have X: perm_eq (to :: ps) pts = (tos == [::]).
 - apply/Bool.eq_iff_eq_true; split.
-  + move=>Hp'; move: (perm_eq_trans Hp' P2).
+  + move=>Hp'; move: (perm_trans Hp' P2).
     rewrite -[to::ps]cat1s -[to::tos]cat1s.
-    move/perm_eqlE: (perm_catC ps [::to])=>Hs.
-    move/(perm_eq_trans Hs); rewrite -[_++[::_]]cats0 catA perm_cat2l.
-    move/perm_eq_size.
+    move/permEl: (perm_catC ps [::to])=>Hs.
+    move/(perm_trans Hs); rewrite -[_++[::_]]cats0 catA perm_cat2l.
+    move/perm_size.
     move => F.
     apply sym_eq in F.
     move: F.
     by move/size0nil=>Z; subst tos. 
-  move/eqP=>Z; subst tos; rewrite perm_eq_sym; apply: (perm_eq_trans P2).
-  by apply/perm_eqlE; move: (perm_catC ps [:: to]).
+  move/eqP=>Z; subst tos; rewrite perm_sym; apply: (perm_trans P2).
+  by apply/permEl; move: (perm_catC ps [:: to]).
 rewrite X in G=>{X}; subst i3.
 rewrite locE//; [|by apply: (cohS C2)|by apply: (cohVl C2')].
 case:ifP=>->//; exists (to :: ps);split=>//.
-apply: (perm_eq_trans P2); apply/perm_eqlE.
+apply: (perm_trans P2); apply/permEl.
 by rewrite -[to::ps]cat1s -[to::tos]cat1s -!catA perm_catCA.
 Qed.
 
@@ -734,7 +734,7 @@ have Pre: rc_commit_inv e (d, lg) [::] i.
 - rewrite /rc_commit_inv/= E1/=.
   have X: perm_eq [::] pts = false.
   - apply/negP. 
-    move/perm_eq_size.
+    move/perm_size.
     move => F.
     apply sym_eq in F.
     move: F.
@@ -817,7 +817,7 @@ have Pre: rc_abort_inv e (d, lg) [::] i.
 - rewrite /rc_abort_inv/= E1/=.
   have X: perm_eq [::] pts = false.
   - apply/negP. 
-    move/perm_eq_size.
+    move/perm_size.
     move => F.
     apply sym_eq in F.
     move: F.

Examples/TwoPhaseCommit/TwoPhaseInductiveProof.v

@@ -126,7 +126,7 @@ split; do?[by rewrite /cn_state locE'?(cohVl C)///cstep_send H1 X]=>//;
   by apply:(@pt_PhaseOneE l cn pts others Hnin d e dt lg pt to _ _ C Hp Z1 G).
 
 case Z1: (pt == to); last first.
-- move/perm_eq_mem: X=>/(_ pt); rewrite inE Z1/= Hp=>Z.
+- move/perm_mem: X=>/(_ pt); rewrite inE Z1/= Hp=>Z.
   move: (H4 _ Hp); rewrite Z.
   by apply:(@pt_PhaseOneE l cn pts others Hnin d e dt lg pt to _ _ C Hp Z1 G).
 move/eqP:Z1=>Z1; subst to.
@@ -199,7 +199,7 @@ move=>[[round][next_data][recvd]|[round][next_data][sent]].
     by rewrite /cn_state locE' ?(cohVl C).
     move=>pt Hpt.
     rewrite in_nil.
-    move/perm_eq_mem: X=>/(_ pt); rewrite inE Hpt.
+    move/perm_mem: X=>/(_ pt); rewrite inE Hpt.
     case/orP.
     * move/eqP=>?; subst pt.
       move: (Hsent to Hto).
@@ -317,7 +317,7 @@ move=>[[round][next_data][recvd]|[round][next_data][sent]].
     by rewrite /cn_state locE' ?(cohVl C).
     move=>pt Hpt.
     rewrite in_nil.
-    move/perm_eq_mem: X=>/(_ pt); rewrite inE Hpt.
+    move/perm_mem: X=>/(_ pt); rewrite inE Hpt.
     case/orP.
     * move/eqP=>?; subst pt.
       move: (Hsent to Hto).
@@ -910,7 +910,7 @@ case: ifP.
     by rewrite (getStL_Kc C _ Hst).
   + move=>pt Hpt.
     move/Pts: (Hpt).
-    move: (perm_eq_mem P) => {P}P.
+    move: (perm_mem P) => {P}P.
     move: (Hpt).
     rewrite -P inE.
     case/orP.
@@ -1007,7 +1007,7 @@ case: ifP.
     by rewrite (getStL_Kc C _ Hst).
   + move=>pt Hpt.
     move/Pts: (Hpt).
-    move: (perm_eq_mem P) => {P}P.
+    move: (perm_mem P) => {P}P.
     move: (Hpt).
     rewrite -P inE.
     case/orP.