{"action":"created","comment":{"url":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/comments/316540812","pull_request_review_id":278246633,"id":316540812,"node_id":"MDI0OlB1bGxSZXF1ZXN0UmV2aWV3Q29tbWVudDMxNjU0MDgxMg==","diff_hunk":"@@ -107,932 +116,906 @@ End Ops.\n Prenex Implicits fnd ins rem supp.\n \n Section Laws.\n-Variables (K : ordType) (V : Type). \n-Notation fmap := (finMap K V). \n+\n+Variables (K : ordType) (V : Type).\n+Notation fmap := (finMap K V).\n Notation nil := (nil K V).\n \n-Lemma ord_path (x y : K) s : ord x y -> path ord y s -> path ord x s.\n+Lemma ord_path (x y : K) s :\n+  ord x y -> path ord y s -> path ord x s.\n Proof.\n-elim: s x y=>[|k s IH] x y //=.\n-by move=>H1; case/andP=>H2 ->; rewrite (trans H1 H2).\n-Qed.\n+elim: s x y => [|k s IH] x y //=.\n+by move=> H1; case/andP=> H2->; rewrite (trans H1 H2). Qed.\n \n-Lemma last_ins' (x : K) (v : V) s : \n-        path ord x (map key s) -> ins' x v s = (x, v) :: s.\n-Proof. by elim: s=>[|[k1 v1] s IH] //=; case: ifP. Qed.\n+Lemma last_ins' (x : K) (v : V) s :\n+  path ord x (map key s) -> ins' x v s = (x, v) :: s.\n+Proof. by elim: s => [|[k1 v1] s IH] //=; case: ifP. Qed.\n \n-Lemma first_ins' (k : K) (v : V) s : \n-        (forall x, x \\in map key s -> ord x k) -> \n-        ins' k v s = rcons s (k, v).\n+Lemma first_ins' (k : K) (v : V) s :\n+  (forall x, x \\in map key s -> ord x k) -> ins' k v s = rcons s (k, v).\n Proof.\n-elim: s=>[|[k1 v1] s IH] H //=.\n+elim: s=> [|[k1 v1] s IH] H //=.\n move: (H k1); rewrite inE eq_refl; move/(_ (erefl _)).\n-case: totalP=>// O _; rewrite IH //.\n-by move=>x H'; apply: H; rewrite inE /= H' orbT.\n-Qed.\n+  case: totalP => //O _; rewrite IH //.\n+by move=> x H'; apply: H; rewrite inE /= H' orbT. Qed.\n \n Lemma notin_path (x : K) s : path ord x s -> x \\notin s.\n-Proof. \n-elim: s=>[|k s IH] //=.\n-rewrite inE negb_or; case/andP=>T1 T2; case: eqP=>H /=.\n+Proof.\n+elim: s=> [|k s IH] //=.\n+rewrite inE negb_or; case/andP=> T1 T2; case: eqP => H /=.\n - by rewrite H irr in T1.\n-by apply: IH; apply: ord_path T2.\n-Qed. \n-\n-Lemma path_supp_ord (s : fmap) k : \n-        path ord k (supp s) -> forall m, m \\in supp s -> ord k m.\n-Proof.\n-case: s=>s H; rewrite /supp /= => H1 m H2; case: totalP H1 H2=>//.\n-- by move=>H1 H2; move: (notin_path (ord_path H1 H2)); case: (m \\in _). \n-by move/eqP=>->; move/notin_path; case: (k \\in _).\n-Qed.\n-\n-Lemma notin_filter (x : K) s : \n-        x \\notin (map key s) -> filter (predk V x) s = [::].\n-Proof.\n-elim: s=>[|[k v] s IH] //=.\n-rewrite inE negb_or; case/andP=>H1 H2.\n-by rewrite eq_sym (negbTE H1); apply: IH.\n-Qed.         \n-   \n-Lemma fmapP (s1 s2 : fmap) : (forall k, fnd k s1 = fnd k s2) -> s1 = s2. \n-Proof.\n-rewrite /fnd; move: s1 s2 => [s1 P1][s2 P2] H; rewrite fmapE /=.\n-elim: s1 P1 s2 P2 H=>[|[k v] s1 IH] /= P1.\n-- by case=>[|[k2 v2] s2 P2] //=; move/(_ k2); rewrite eq_refl.\n+  by apply: IH; apply: ord_path T2. Qed.\n+\n+Lemma path_supp_ord (s : fmap) k :\n+  path ord k (supp s) ->\n+  forall m, m \\in supp s -> ord k m.\n+Proof.\n+case: s => s H; rewrite /supp /= => H1 m H2; case: totalP H1 H2 => //.\n+-\n+by move=> H1 H2; move: (notin_path (ord_path H1 H2)); case: (m \\in _).\n+by move/eqP=> ->; move/notin_path; case: (k \\in _). Qed.\n+\n+Lemma notin_filter (x : K) s :\n+  x \\notin (map key s) -> filter (predk V x) s = [::].\n+Proof.\n+elim: s=> [|[k v] s IH] //=.\n+rewrite inE negb_or; case/andP=> H1 H2.\n+  by rewrite eq_sym (negbTE H1); apply: IH. Qed.\n+\n+Lemma fmapP (s1 s2 : fmap) :\n+  (forall k, fnd k s1 = fnd k s2) -> s1 = s2.\n+Proof.\n+rewrite /fnd; move: s1 s2 => [s1 P1] [s2 P2] H; rewrite fmapE /=.\n+elim: s1 P1 s2 P2 H => [|[k v] s1 IH] /= P1.\n+-\n+by case=> [|[k2 v2] s2 P2] //=; move/(_ k2); rewrite eq_refl.\n have S1: sorted ord (map key s1) by apply: path_sorted P1.\n-case=>[|[k2 v2] s2] /= P2; first by move/(_ k); rewrite eq_refl.\n+case=> [|[k2 v2] s2] /= P2; first by move/(_ k); rewrite eq_refl.\n have S2: sorted ord (map key s2) by apply: path_sorted P2.\n-move: (IH S1 s2 S2)=>{IH} /= IH H.\n-move: (notin_path P1) (notin_path P2)=>N1 N2.\n+  move: (IH S1 s2 S2) => {IH}/= IH H.\n+move: (notin_path P1) (notin_path P2) => N1 N2.\n case E: (k == k2).\n-- rewrite -{k2 E}(eqP E) in P2 H N2 *.\n-  move: (H k); rewrite eq_refl=>[[E2]]; rewrite -E2 {v2 E2} in H *.\n+-\n+rewrite -{k2 E}(eqP E) in P2 H N2 *.\n+move: (H k); rewrite eq_refl=> [[E2]]; rewrite -E2 {v2 E2} in H *.\n   rewrite IH // => k'.\n-  case E: (k == k'); first by rewrite -(eqP E) !notin_filter.\n-  by move: (H k'); rewrite E.\n+case E: (k == k'); first by rewrite -(eqP E) !notin_filter.\n+by move: (H k'); rewrite E.\n move: (H k); rewrite eq_refl eq_sym E notin_filter //.\n-move: (total k k2); rewrite E /=; case/orP=>L1.\n+  move: (total k k2); rewrite E /=; case/orP=> L1.\n - by apply: notin_path; apply: ord_path P2.\n-move: (H k2); rewrite E eq_refl notin_filter //.\n-by apply: notin_path; apply: ord_path P1.\n-Qed.\n+  move: (H k2); rewrite E eq_refl notin_filter //. by apply: notin_path; apply: ord_path P1. Qed.\n \n-Lemma predkN (k1 k2 : K) : predI (predk V k1) (predCk V k2) =1 \n-                           if k1 == k2 then pred0 else predk V k1.\n-Proof. \n-by move=>x; case: ifP=>H /=; [|case: eqP=>//->]; rewrite ?(eqP H) ?andbN ?H. \n-Qed.\n+Lemma predkN (k1 k2 : K) :\n+  predI (predk V k1) (predCk V k2) =1\n+  if k1 == k2 then pred0 else predk V k1.\n+Proof.\n+by move=> x; case: ifP => H /=; [|case: eqP =>//->]; rewrite ?(eqP H) ?andbN ?H. Qed.\n \n CoInductive supp_spec x (s : fmap) : bool -> Type :=\n-| supp_spec_some v of fnd x s = Some v : supp_spec x s true\n-| supp_spec_none of fnd x s = None : supp_spec x s false. \n+  | supp_spec_some v of fnd x s = Some v : supp_spec x s true\n+  | supp_spec_none of fnd x s = None : supp_spec x s false.\n \n Lemma suppP x (s : fmap) : supp_spec x s (x \\in supp s).\n-Proof. \n-move E: (x \\in supp s)=>b; case: b E; move/idP; last first.\n-- move=>H; apply: supp_spec_none.\n-  case E: (fnd _ _)=>[v|] //; case: H.\n-  rewrite /supp /fnd in E *; case: s E=>/=.\n-  elim=>[|[y w] s IH] H1 //=.\n-  case: ifP=>H; first by rewrite (eqP H) inE eq_refl.\n-  rewrite -topredE /= eq_sym H; apply: IH.\n-  by apply: path_sorted H1.\n-case: s; elim=>[|[y w] s IH] /= H1 //; rewrite /supp /= inE in IH *.\n-case: eqP=>[-> _|H] //=.\n-- by apply: (@supp_spec_some _ _ w); rewrite /fnd /= eq_refl.\n-move: (path_sorted H1)=>H1'; move/(IH H1'); case=>[v H2|H2]; \n-[apply: (@supp_spec_some _ _ v) | apply: supp_spec_none];\n-by rewrite /fnd /=; case: eqP H=>// ->.\n-Qed.\n-\n-Lemma suppE (s1 s2 : fmap) : supp s1 =i supp s2 <-> supp s1 = supp s2.\n-Proof.\n-split; last by move=>->.\n-case: s1 s2=>s1 H1 [s2 H2]; rewrite /supp /=. \n-elim: s1 s2 H1 H2=>[|[k1 _] s1 IH][|[k2 _] s2] //=.\n-- by move=>_ _; move/(_ k2); rewrite inE eq_refl. \n-- by move=>_ _; move/(_ k1); rewrite inE eq_refl.\n-case: (totalP k1 k2)=>/= O H1 H2.\n-- move/(_ k1); rewrite !inE eq_refl /= eq_sym.\n+Proof.\n+move E: (x \\in supp s)=> b; case: b E; move/idP; last first.\n+-\n+move=> H; apply: supp_spec_none.\n+case E: (fnd _ _)=> [v |] //; case: H.\n+rewrite /supp /fnd in E *; case: s E => /=.\n+elim=> [|[y w] s IH] H1 //=.\n+  case: ifP=> H; first by rewrite (eqP H) inE eq_refl.\n+rewrite -topredE /= eq_sym H; apply: IH. by apply: path_sorted H1.\n+case: s; elim=> [|[y w] s IH] /= H1 //; rewrite /supp /= inE in IH *.\n+case: eqP => [-> _|H] //=.\n+-\n+by apply: (@supp_spec_some _ _ w); rewrite /fnd /= eq_refl.\n+move: (path_sorted H1)=> H1'; move/(IH H1'); case=> [v H2|H2]; [ apply: (@supp_spec_some _ _ v)\n+| apply: supp_spec_none];\n+  by rewrite /fnd /=; case: eqP H => //->. Qed.\n+\n+Lemma suppE (s1 s2 : fmap) :\n+  supp s1 =i supp s2 <-> supp s1 = supp s2.\n+Proof.\n+  split; last by move=> ->.\n+case: s1 s2 => s1 H1 [s2 H2]; rewrite /supp /=.\n+elim: s1 s2 H1 H2 => [|[k1 _] s1 IH] [|[k2 _] s2] //=.\n+-\n+  by move=> _ _; move/(_ k2); rewrite inE eq_refl.\n+-\n+  by move=> _ _; move/(_ k1); rewrite inE eq_refl.\n+  case: (totalP k1 k2) => /= O H1 H2.\n+-\n+  move/(_ k1); rewrite !inE eq_refl /= eq_sym.\n+case: totalP O => //= O _.\n+by move/(ord_path O)/notin_path/negbTE: H2 => ->.\n+-\n+  rewrite -{k2 O}(eqP O) in H1 H2 *.\n+move=> H; congr (_ :: _); apply: IH.\n+- by apply: path_sorted H1.\n+- by apply: path_sorted H2.\n+move=> x; move: (H x); rewrite !inE /=.\n+case: eqP => //-> /= _.\n+by move/notin_path/negbTE: H1=> ->; move/notin_path/negbTE: H2=> ->.\n+  move/(_ k2); rewrite !inE eq_refl /= eq_sym.\n   case: totalP O => //= O _.\n-  by move/(ord_path O)/notin_path/negbTE: H2=>->.\n-- rewrite -{k2 O}(eqP O) in H1 H2 *.\n-  move=>H; congr (_ :: _); apply: IH.\n-  - by apply: path_sorted H1.\n-  - by apply: path_sorted H2.\n-  move=>x; move: (H x); rewrite !inE /=. case: eqP=>// -> /= _.\n-  by move/notin_path/negbTE: H1=>->; move/notin_path/negbTE: H2=>->. \n-move/(_ k2); rewrite !inE eq_refl /= eq_sym.\n-case: totalP O=>//= O _.\n-by move/(ord_path O)/notin_path/negbTE: H1=>->. \n-Qed.\n-\n-Lemma supp_nil : supp nil = [::]. Proof. by []. Qed.\n+by move/(ord_path O)/notin_path/negbTE: H1=> ->. Qed.\n+\n+Lemma supp_nil : supp nil = [::].\n+Proof. by []. Qed.\n \n Lemma supp_nilE (s : fmap) : (supp s = [::]) <-> (s = nil).\n-Proof. by split=>[|-> //]; case: s; case=>// H; rewrite fmapE. Qed.\n+Proof.\n+by split=> [|-> //]; case: s; case=> // H; rewrite fmapE. Qed.\n \n-Lemma supp_rem k (s : fmap) : \n-        supp (rem k s) =i predI (predC1 k) (mem (supp s)).\n+Lemma supp_rem k (s : fmap) :\n+  supp (rem k s) =i predI (predC1 k) (mem (supp s)).\n Proof.\n case: s => s H1 x; rewrite /supp inE /=.\n-by case H2: (x == k)=>/=; rewrite -filter_map mem_filter /= H2.\n-Qed.\n- \n-Lemma supp_ins k v (s : fmap) : \n-        supp (ins k v s) =i [predU pred1 k & supp s].\n-Proof. \n+by case H2: (x == k)=> /=; rewrite -filter_map mem_filter /= H2. Qed.\n+\n+Lemma supp_ins k v (s : fmap) :\n+  supp (ins k v s) =i [predU pred1 k & supp s].\n+Proof.\n case: s => s H x; rewrite /supp inE /=.\n-elim: s x k v H=>[|[k1 v1] s IH] //= x k v H.\n-case: ifP=>H1 /=; first by rewrite inE.\n-case: ifP=>H2 /=; first by rewrite !inE (eqP H2) orbA orbb.\n-by rewrite !inE (IH _ _ _ (path_sorted H)) orbCA.\n-Qed.\n+elim: s x k v H => [|[k1 v1] s IH] //= x k v H.\n+case: ifP => H1 /=; first by rewrite inE.\n+  case: ifP => H2/=; first by rewrite !inE (eqP H2) orbA orbb.\n+  by rewrite !inE (IH _ _ _ (path_sorted H)) orbCA. Qed.\n \n-Lemma fnd_empty k : fnd k nil = None. Proof. by []. Qed.   \n+Lemma fnd_empty k : fnd k nil = None.\n+Proof. by []. Qed.\n \n-Lemma fnd_rem k1 k2 (s : fmap) : \n-        fnd k1 (rem k2 s) = if k1 == k2 then None else fnd k1 s.\n-Proof. \n+Lemma fnd_rem k1 k2 (s : fmap) :\n+  fnd k1 (rem k2 s) = if k1 == k2 then None else fnd k1 s.\n+Proof.\n case: s => s H; rewrite /fnd -filter_predI (eq_filter (predkN k1 k2)).\n-by case: eqP=>//; rewrite filter_pred0. \n-Qed.\n+by case: eqP => //; rewrite filter_pred0. Qed.\n \n-Lemma fnd_ins k1 k2 v (s : fmap) : \n-        fnd k1 (ins k2 v s) = if k1 == k2 then Some v else fnd k1 s. \n+Lemma fnd_ins k1 k2 v (s : fmap) :\n+  fnd k1 (ins k2 v s) = if k1 == k2 then Some v else fnd k1 s.\n Proof.\n case: s => s H; rewrite /fnd /=.\n-elim: s k1 k2 v H=>[|[k' v'] s IH] //= k1 k2 v H.\n-- by case: ifP=>H1; [rewrite (eqP H1) eq_refl | rewrite eq_sym H1].\n-case: ifP=>H1 /=.\n-- by case: ifP=>H2; [rewrite (eqP H2) eq_refl | rewrite (eq_sym k1) H2].\n-case: ifP=>H2 /=. \n-- rewrite (eqP H2).   \n-  by case: ifP=>H3; [rewrite (eqP H3) eq_refl | rewrite eq_sym H3].\n-case: ifP=>H3; first by rewrite -(eqP H3) eq_sym H2.\n-by apply: IH; apply: path_sorted H.\n-Qed.\n- \n-Lemma ins_rem k1 k2 v (s : fmap) : \n-        ins k1 v (rem k2 s) = \n-        if k1 == k2 then ins k1 v s else rem k2 (ins k1 v s).\n-Proof.\n-move: k1 k2 v s.\n-have L3: forall (x : K) s, \n-  path ord x (map key s) -> filter (predCk V x) s = s.\n-- move=>x t; move/notin_path; elim: t=>[|[k3 v3] t IH] //=.\n-  rewrite inE negb_or; case/andP=>T1 T2. \n+  elim: s k1 k2 v H => [|[k' v'] s IH] //= k1 k2 v H.\n+-\n+  by case: ifP => H1; [rewrite (eqP H1) eq_refl | rewrite eq_sym H1].\n+case: ifP => H1 /=.\n+-\n+  by case: ifP => H2; [rewrite (eqP H2) eq_refl | rewrite (eq_sym k1) H2].\n+case: ifP => H2/=.\n+-\n+rewrite (eqP H2).\n+  by case: ifP => H3; [rewrite (eqP H3) eq_refl | rewrite eq_sym H3].\n+  case: ifP=> H3; first by rewrite -(eqP H3) eq_sym H2.\n+by apply: IH; apply: path_sorted H. Qed.\n+\n+Lemma ins_rem k1 k2 v (s : fmap) :\n+  ins k1 v (rem k2 s) =\n+  if k1 == k2 then ins k1 v s else rem k2 (ins k1 v s).\n+Proof. move: k1 k2 v s.\n+have L3: forall (x : K) s, path ord x (map key s) -> filter (predCk V x) s = s.\n+-\n+  move=> x t; move/notin_path; elim: t => [|[k3 v3] t IH] //=.\n+  rewrite inE negb_or; case/andP=> T1 T2.\n   by rewrite eq_sym T1 IH.\n-have L5: forall (x : K) (v : V) s, \n+have L5: forall (x : K) (v : V) s,\n   sorted ord (map key s) -> ins' x v (filter (predCk V x) s) = ins' x v s.\n-- move=>x v s; elim: s x v=>[|[k' v'] s IH] x v //= H.\n-  case H1: (ord x k').\n-  - case H2: (k' == x)=>/=; first by rewrite (eqP H2) irr in H1.\n-    by rewrite H1 L3 //; apply: ord_path H1 H.\n-  case H2: (k' == x)=>/=.\n-  - rewrite (eqP H2) eq_refl in H *.\n-    by rewrite L3 //; apply: last_ins' H.\n-  rewrite eq_sym H2 H1 IH //.\n-  by apply: path_sorted H.\n-move=>k1 k2 v [s H]. \n-case: ifP=>H1; rewrite /ins /rem fmapE /=.\n-- rewrite {k1 H1}(eqP H1).\n-  elim: s k2 v H=>[|[k' v'] s IH] //= k2 v H.\n-  case H1: (k' == k2)=>/=.\n-  - rewrite eq_sym H1 (eqP H1) irr in H *.\n-    by rewrite L3 // last_ins'.\n-  rewrite eq_sym H1; case: ifP=>H3.\n-  - by rewrite L3 //; apply: ord_path H3 H.\n-  by rewrite L5 //; apply: path_sorted H.\n-elim: s k1 k2 H1 H=>[|[k' v'] s IH] //= k1 k2 H1 H; first by rewrite H1.\n-case H2: (k' == k2)=>/=.\n-- rewrite (eqP H2) in H *; rewrite H1. \n-  case H3: (ord k1 k2)=>/=.\n-  - by rewrite H1 eq_refl /= last_ins' // L3 //; apply: ord_path H.\n-  by rewrite eq_refl /= IH //; apply: path_sorted H.\n-case H3: (ord k1 k')=>/=; first by rewrite H1 H2.\n-case H4: (k1 == k')=>/=; first by rewrite H1.\n-by rewrite H2 IH //; apply: path_sorted H.\n-Qed.\n-       \n-Lemma ins_ins k1 k2 v1 v2 (s : fmap) : \n-        ins k1 v1 (ins k2 v2 s) = if k1 == k2 then ins k1 v1 s \n-                                  else ins k2 v2 (ins k1 v1 s).\n+-\n+move=> x v s; elim: s x v => [|[k' v'] s IH] x v //= H.\n+case H1: (ord x k').\n+-\n+case H2: (k' == x)=> /=; first by rewrite (eqP H2) irr in H1.\n+by rewrite H1 L3 //; apply: ord_path H1 H.\n+case H2: (k' == x) => /=.\n+-\n+rewrite (eqP H2) eq_refl in H *. by rewrite L3 //; apply: last_ins' H.\n+  rewrite eq_sym H2 H1 IH //. by apply: path_sorted H.\n+move=> k1 k2 v [s H].\n+case: ifP => H1; rewrite /ins /rem fmapE /=.\n+-\n+rewrite {k1 H1}(eqP H1).\n+  elim: s k2 v H => [|[k' v'] s IH] //= k2 v H.\n+case H1: (k' == k2)=> /=.\n+-\n+rewrite eq_sym H1 (eqP H1) irr in H *. by rewrite L3 // last_ins'.\n+rewrite eq_sym H1; case: ifP => H3.\n+-\n+by rewrite L3 //; apply: ord_path H3 H. by rewrite L5 //; apply: path_sorted H.\n+  elim: s k1 k2 H1 H => [|[k' v'] s IH] //= k1 k2 H1 H; first by rewrite H1.\n+case H2: (k' == k2)=> /=.\n+-\n+rewrite (eqP H2) in H *; rewrite H1.\n+case H3: (ord k1 k2)=> /=.\n+-\n+by rewrite H1 eq_refl /= last_ins' // L3 //; apply: ord_path H.\n+by rewrite eq_refl /= IH //; apply: path_sorted H.\n+  case H3: (ord k1 k') => /=; first by rewrite H1 H2.\n+  case H4: (k1 == k') => /=; first by rewrite H1.\n+by rewrite H2 IH //; apply: path_sorted H. Qed.\n+\n+Lemma ins_ins k1 k2 v1 v2 (s : fmap) :\n+  ins k1 v1 (ins k2 v2 s) =\n+  if k1 == k2 then ins k1 v1 s\n+  else ins k2 v2 (ins k1 v1 s).\n Proof.\n rewrite /ins; case: s => s H; case H1: (k1 == k2); rewrite fmapE /=.\n-- rewrite (eqP H1) {H1}.\n-  elim: s H k2 v1 v2=>[|[k3 v3] s IH] /= H k2 v1 v2; \n-    first by rewrite irr eq_refl.\n-  case: (totalP k2 k3)=>H1 /=; rewrite ?irr ?eq_refl //.\n-  case: (totalP k2 k3) H1=>H2 _ //.\n-  by rewrite IH //; apply: path_sorted H.\n-elim: s H k1 k2 H1 v1 v2=>[|[k3 v3] s IH] H k1 k2 H1 v1 v2 /=.\n-- rewrite H1 eq_sym H1.\n-  by case: (totalP k1 k2) H1=>H2 H1.\n-case: (totalP k2 k3)=>H2 /=.\n-- case: (totalP k1 k2) (H1)=>H3 _ //=; last first.\n-  - by case: (totalP k1 k3)=>//= H4; rewrite ?H2 ?H3.\n-  case: (totalP k1 k3)=>H4 /=.\n-  - case: (totalP k2 k1) H3=>//= H3.\n-    by case: (totalP k2 k3) H2=>//=.\n-  - rewrite (eqP H4) in H3. \n-    by case: (totalP k2 k3) H2 H3.\n+-\n+  rewrite (eqP H1) {H1}.\n+  elim: s H k2 v1 v2 => [|[k3 v3] s IH] /= H k2 v1 v2; first by rewrite irr eq_refl.\n+  case: (totalP k2 k3) => H1 /=; rewrite ?irr ?eq_refl //.\n+  case: (totalP k2 k3) H1 => H2 _ //. by rewrite IH //; apply: path_sorted H.\n+  elim: s H k1 k2 H1 v1 v2 => [|[k3 v3] s IH] H k1 k2 H1 v1 v2 /=.\n+-\n+rewrite H1 eq_sym H1.\n+by case: (totalP k1 k2) H1 => H2 H1.\n+  case: (totalP k2 k3) => H2 /=.\n+-\n+  case: (totalP k1 k2) (H1) => H3 _ //=; last first.\n+-\n+  by case: (totalP k1 k3)=> //= H4; rewrite ?H2 ?H3.\n+case: (totalP k1 k3) => H4 /=.\n+-\n+case: (totalP k2 k1) H3 => //= H3.\n+  by case: (totalP k2 k3) H2 => //=.\n+-\n+  rewrite (eqP H4) in H3.\n+  by case: (totalP k2 k3) H2 H3.\n   by case: (totalP k1 k3) (trans H3 H2) H4.\n-- rewrite -(eqP H2) {H2} (H1).\n-  case: (totalP k1 k2) (H1)=>//= H2 _; rewrite ?irr ?eq_refl //.\n-  rewrite eq_sym H1.\n-  by case: (totalP k2 k1) H1 H2.\n-case: (totalP k1 k3)=>H3 /=.  \n-- rewrite eq_sym H1.\n-  case: (totalP k2 k1) H1 (trans H3 H2)=>//.\n-  by case: (totalP k2 k3) H2=>//=.\n-- rewrite (eqP H3).\n-  by case: (totalP k2 k3) H2.\n-case: (totalP k2 k3)=>H4 /=.\n+-\n+rewrite -(eqP H2) {H2}(H1).\n+  case: (totalP k1 k2) (H1) => //= H2 _; rewrite ?irr ?eq_refl //.\n+rewrite eq_sym H1. by case: (totalP k2 k1) H1 H2.\n+case: (totalP k1 k3) => H3 /=.\n+-\n+rewrite eq_sym H1.\n+  case: (totalP k2 k1) H1 (trans H3 H2)=> //.\n+  by case: (totalP k2 k3) H2 => //=.\n+-\n+rewrite (eqP H3).\n+by case: (totalP k2 k3) H2.\n+  case: (totalP k2 k3) => H4 /=.\n - by move: (trans H4 H2); rewrite irr.\n-- by rewrite (eqP H4) irr in H2.\n-by rewrite IH //; apply: path_sorted H.\n-Qed. \n+-\n+  by rewrite (eqP H4) irr in H2. by rewrite IH //; apply: path_sorted H. Qed.\n \n-Lemma rem_empty k : rem k nil = nil. \n+Lemma rem_empty k : rem k nil = nil.\n Proof. by rewrite fmapE. Qed.\n \n-Lemma rem_rem k1 k2 (s : fmap) : \n-        rem k1 (rem k2 s) = if k1 == k2 then rem k1 s else rem k2 (rem k1 s).\n+Lemma rem_rem k1 k2 (s : fmap) :\n+  rem k1 (rem k2 s) = if k1 == k2 then rem k1 s else rem k2 (rem k1 s).\n Proof.\n rewrite /rem; case: s => s H /=.\n-case H1: (k1 == k2); rewrite fmapE /= -!filter_predI; apply: eq_filter=>x /=.\n-- by rewrite (eqP H1) andbb.\n-by rewrite andbC.\n-Qed.\n+case H1: (k1 == k2); rewrite fmapE /= -!filter_predI; apply: eq_filter => x /=.\n+-\n+  by rewrite (eqP H1) andbb. by rewrite andbC. Qed.\n \n-Lemma rem_ins k1 k2 v (s : fmap) : \n-        rem k1 (ins k2 v s) = \n-        if k1 == k2 then rem k1 s else ins k2 v (rem k1 s).\n+Lemma rem_ins k1 k2 v (s : fmap) :\n+  rem k1 (ins k2 v s) = if k1 == k2 then rem k1 s else ins k2 v (rem k1 s).\n Proof.\n rewrite /rem; case: s => s H /=; case H1: (k1 == k2); rewrite /= fmapE /=.\n-- rewrite (eqP H1) {H1}.\n-  elim: s k2 H=>[|[k3 v3] s IH] k2 /= H; rewrite ?eq_refl 1?eq_sym //.\n-  case: (totalP k3 k2)=>H1 /=; rewrite ?eq_refl //=; \n-  case: (totalP k3 k2) H1=>//= H1 _.\n-  by rewrite IH //; apply: path_sorted H.\n-elim: s k1 k2 H1 H=>[|[k3 v3] s IH] k1 k2 H1 /= H; first by rewrite eq_sym H1.\n-case: (totalP k2 k3)=>H2 /=.\n-- rewrite eq_sym H1 /=.\n-  case: (totalP k3 k1)=>H3 /=; case: (totalP k2 k3) (H2)=>//=.\n+-\n+  rewrite (eqP H1) {H1}.\n+  elim: s k2 H => [|[k3 v3] s IH] k2 /= H; rewrite ?eq_refl 1?eq_sym //.\n+case: (totalP k3 k2) => H1 /=; rewrite ?eq_refl //=; case: (totalP k3 k2) H1 => //= H1 _. by rewrite IH //; apply: path_sorted H.\n+  elim: s k1 k2 H1 H => [|[k3 v3] s IH] k1 k2 H1 /= H; first by rewrite eq_sym H1.\n+  case: (totalP k2 k3) => H2 /=.\n+-\n+rewrite eq_sym H1 /=.\n+  case: (totalP k3 k1) => H3 /=; case: (totalP k2 k3)(H2) => //=.\n   rewrite -(eqP H3) in H1 *.\n-  rewrite -IH //; last by apply: path_sorted H. \n-  rewrite last_ins' /= 1?eq_sym ?H1 //.\n-  by apply: ord_path H.\n-- by move: H1; rewrite (eqP H2) /= eq_sym => -> /=; rewrite irr eq_refl.\n-case: (totalP k3 k1)=>H3 /=.\n-- case: (totalP k2 k3) H2=>//= H2 _.\n-  by rewrite IH //; apply: path_sorted H.\n-- rewrite -(eqP H3) in H1 *.\n-  by rewrite IH //; apply: path_sorted H.\n-case: (totalP k2 k3) H2=>//= H2 _.\n-by rewrite IH //; apply: path_sorted H.\n-Qed.\n-\n-Lemma rem_supp k (s : fmap) : \n-        k \\notin supp s -> rem k s = s.\n+  rewrite -IH //; last by apply: path_sorted H.\n+  rewrite last_ins' /= 1?eq_sym ?H1 //. by apply: ord_path H.\n+-\n+by move: H1; rewrite (eqP H2) /= eq_sym => -> /=; rewrite irr eq_refl.\n+case: (totalP k3 k1) => H3 /=.\n+-\n+  case: (totalP k2 k3) H2 => //= H2 _. by rewrite IH //; apply: path_sorted H.\n+-\n+  rewrite -(eqP H3) in H1 *. by rewrite IH //; apply: path_sorted H.\n+  case: (totalP k2 k3) H2 => //= H2 _. by rewrite IH //; apply: path_sorted H. Qed.\n+\n+Lemma rem_supp k (s : fmap) : k \\notin supp s -> rem k s = s.\n Proof.\n case: s => s H1; rewrite /supp !fmapE /= => H2.\n-elim: s H1 H2=>[|[k1 v1] s1 IH] //=; move/path_sorted=>H1.\n-rewrite inE negb_or; case/andP=>H2; move/(IH H1)=>H3.\n-by rewrite eq_sym H2 H3.\n-Qed.\n+elim: s H1 H2 => [|[k1 v1] s1 IH] //=; move/path_sorted=> H1.\n+  rewrite inE negb_or; case/andP=> H2; move/(IH H1)=> H3.\n+by rewrite eq_sym H2 H3. Qed.\n \n-Lemma fnd_supp k (s : fmap) : \n-        k \\notin supp s -> fnd k s = None.\n+Lemma fnd_supp k (s : fmap) : k \\notin supp s -> fnd k s = None.\n Proof. by case: suppP. Qed.\n \n-Lemma fnd_supp_in k (s : fmap) : \n-        k \\in supp s -> exists v, fnd k s = Some v.\n-Proof. by case: suppP=>[v|]; [exists v|]. Qed.\n-\n-Lemma cancel_ins k v (s1 s2 : fmap) : \n-       k \\notin (supp s1) -> k \\notin (supp s2) -> \n-         ins k v s1 = ins k v s2 -> s1 = s2.\n-Proof.\n-move: s1 s2=>[s1 p1][s2 p2]; rewrite !fmapE /supp /= {p1 p2}.\n-elim: s1 k v s2=>[k v s2| [k1 v1] s1 IH1 k v s2] /=.\n-- case: s2=>[| [k2 v2] s2] //= _.\n-  rewrite inE negb_or; case/andP=>H1 _; case: ifP=>// _.   \n-  by rewrite (negbTE H1); case=>E; rewrite E eq_refl in H1.\n-rewrite inE negb_or; case/andP=>H1 H2 H3. \n-case: ifP=>H4; case: s2 H3=>[| [k2 v2] s2] //=.\n-- rewrite inE negb_or; case/andP=>H5 H6. \n-  case: ifP=>H7; first by case=>->->->.\n-  by rewrite (negbTE H5); case=>E; rewrite E eq_refl in H5.\n-- by rewrite (negbTE H1)=>_; case=>E; rewrite E eq_refl in H1.\n-rewrite inE negb_or (negbTE H1); case/andP=>H5 H6.\n-rewrite (negbTE H5); case: ifP=>H7 /=.\n-- by case=>E; rewrite E eq_refl in H1.\n-by case=>->-> H; congr (_ :: _); apply: IH1 H.\n-Qed.\n+Lemma fnd_supp_in k (s : fmap) : k \\in supp s -> exists v, fnd k s = Some v.\n+Proof. by case: suppP=> [v|]; [exists v|]. Qed.\n+\n+Lemma cancel_ins k v (s1 s2 : fmap) :\n+   k \\notin (supp s1) -> k \\notin (supp s2) -> ins k v s1 = ins k v s2 -> s1 = s2.\n+Proof.\n+move: s1 s2 => [s1 p1] [s2 p2]; rewrite !fmapE /supp /= {p1 p2}.\n+elim: s1 k v s2 => [k v s2 |[k1 v1] s1 IH1 k v s2] /=.\n+-\n+case: s2 => [|[k2 v2] s2] //= _.\n+rewrite inE negb_or; case/andP=> H1 _; case: ifP => // _.\n+by rewrite (negbTE H1); case=> E; rewrite E eq_refl in H1.\n+rewrite inE negb_or; case/andP=> H1 H2 H3.\n+  case: ifP=> H4; case: s2 H3=> [|[k2 v2] s2] //=.\n+-\n+rewrite inE negb_or; case/andP=> H5 H6.\n+  case: ifP=> H7; first by case=> ->-> ->.\n+by rewrite (negbTE H5); case=> E; rewrite E eq_refl in H5.\n+-\n+  by rewrite (negbTE H1)=> _; case=> E; rewrite E eq_refl in H1.\n+rewrite inE negb_or (negbTE H1); case/andP=> H5 H6.\n+rewrite (negbTE H5); case: ifP => H7 /=.\n+- by case=> E; rewrite E eq_refl in H1.\n+by case=> -> -> H; congr (_ :: _); apply: IH1 H. Qed.\n \n End Laws.\n \n-Section Append. \n+Section Append.\n+\n Variable (K : ordType) (V : Type).\n-Notation fmap := (finMap K V).  \n+Notation fmap := (finMap K V).\n Notation nil := (nil K V).\n \n-Lemma seqof_ins k v (s : fmap) : \n-        path ord k (supp s) -> seq_of (ins k v s) = (k, v) :: seq_of s.\n-Proof. by case: s; elim=>[|[k1 v1] s IH] //= _; case/andP=>->. Qed.\n+Lemma seqof_ins k v (s : fmap) :\n+  path ord k (supp s) ->\n+  seq_of (ins k v s) = (k, v) :: seq_of s.\n+Proof.\n+by case: s; elim=> [|[k1 v1] s IH] //= _; case/andP=> ->. Qed.\n \n-Lemma path_supp_ins k1 k v (s : fmap) : \n-        ord k1 k -> path ord k1 (supp s) -> path ord k1 (supp (ins k v s)).\n+Lemma path_supp_ins k1 k v (s : fmap) :\n+  ord k1 k -> path ord k1 (supp s) -> path ord k1 (supp (ins k v s)).\n Proof.\n-case: s=>s p.\n-elim: s p k1 k v=>[| [k2 v2] s IH] //= p k1 k v H2; first by rewrite H2.\n-case/andP=>H3 H4.\n+case: s => s p.\n+elim: s p k1 k v => [|[k2 v2] s IH] //= p k1 k v H2; first by rewrite H2.\n+case/andP=> H3 H4.\n have H5: path ord k1 (map key s) by apply: ord_path H4.\n-rewrite /supp /=; case: (totalP k k2)=>H /=.\n-- by rewrite H2 H H4.\n-- by rewrite H2 (eqP H) H4.\n+rewrite /supp /=; case: (totalP k k2) => H /=.\n+-\n+by rewrite H2 H H4.\n+-\n+by rewrite H2 (eqP H) H4.\n rewrite H3 /=.\n-have H6: sorted ord (map key s) by apply: path_sorted H5. \n-by move: (IH H6 k2 k v H H4); case: s {IH p H4 H5} H6.\n-Qed.\n+have H6: sorted ord (map key s) by apply: path_sorted H5.\n+by move: (IH H6 k2 k v H H4); case: s {IH p H4 H5} H6. Qed.\n \n-Lemma path_supp_ins_inv k1 k v (s : fmap) :\n-        path ord k (supp s) -> path ord k1 (supp (ins k v s)) -> \n-        ord k1 k && path ord k1 (supp s).\n+Lemma path_supp_ins_inv k1 k v (s : fmap) : path ord k (supp s) -> path ord k1 (supp (ins k v s)) ->\n+  ord k1 k && path ord k1 (supp s).\n Proof.\n-case: s=>s p; rewrite /supp /= => H1; rewrite last_ins' //=.\n-by case/andP=>H2 H3; rewrite H2; apply: ord_path H3.\n-Qed.\n+case: s => s p; rewrite /supp /= => H1; rewrite last_ins' //=.\n+by case/andP=> H2 H3; rewrite H2; apply: ord_path H3. Qed.\n \n (* forward induction principle *)\n-Lemma fmap_ind' (P : fmap -> Prop) : \n-        P nil -> (forall k v s, path ord k (supp s) -> P s -> P (ins k v s)) -> \n-        forall s, P s.\n+Lemma fmap_ind' (P : fmap -> Prop) :\n+  P nil -> (forall k v s, path ord k (supp s) -> P s -> P (ins k v s)) ->\n+  forall s, P s.\n Proof.\n-move=>H1 H2; case; elim=>[|[k v] s IH] /= H.\n-- by rewrite (_ : FinMap _ = nil); last by rewrite fmapE.\n-have S: sorted ord (map key s) by apply: path_sorted H.  \n-rewrite (_ : FinMap _ = ins k v (FinMap S)); last by rewrite fmapE /= last_ins'.\n-by apply: H2.\n-Qed.\n+move=> H1 H2; case; elim=> [|[k v] s IH] /= H.\n+-\n+  by rewrite (_ : FinMap _ = nil); last by rewrite fmapE.\n+have S: sorted ord (map key s) by apply: path_sorted H.\n+  rewrite (_ : FinMap _ = ins k v (FinMap S)); last by rewrite fmapE /= last_ins'. by apply: H2. Qed.\n \n (* backward induction principle *)\n-Lemma fmap_ind'' (P : fmap -> Prop) : \n-        P nil -> (forall k v s, (forall x, x \\in supp s -> ord x k) -> \n-                    P s -> P (ins k v s)) ->\n-        forall s, P s.\n+Lemma fmap_ind'' (P : fmap -> Prop) :\n+    P nil -> (forall k v s, (forall x, x \\in supp s -> ord x k) ->\n+  P s -> P (ins k v s)) -> forall s, P s.\n Proof.\n-move=>H1 H2; case; elim/last_ind=>[|s [k v] IH] /= H. \n-- by rewrite (_ : FinMap _ = nil); last by rewrite fmapE.\n+move=> H1 H2; case; elim/last_ind=> [|s [k v] IH] /= H.\n+-\n+  by rewrite (_ : FinMap _ = nil); last by rewrite fmapE.\n have Sb: subseq (map key s) (map key (rcons s (k, v))).\n-- by elim: s {IH H}=>[|x s IH] //=; rewrite eq_refl. \n-have S : sorted ord (map key s).\n+-\n+by elim: s {IH H} => [|x s IH] //=; rewrite eq_refl.\n+have S: sorted ord (map key s).\n - by apply: subseq_sorted Sb H; apply: ordtype.trans.\n-have T : forall x : K, x \\in map key s -> ord x k.\n-- elim: {IH Sb S} s H=>[|[k1 v1] s IH] //= L x.\n-  rewrite inE; case/orP; last by apply: IH; apply: path_sorted L.\n-  move/eqP=>->; elim: s {IH} L=>[|[x1 w1] s IH] /=; first by rewrite andbT. \n-  by case/andP=>O /(ord_path O) /IH.  \n-rewrite (_ : FinMap _ = ins k v (FinMap S)). \n-- by apply: H2 (IH _)=>x /T.\n-by rewrite fmapE /= first_ins'.\n-Qed.\n-\n+have T: forall x : K, x \\in map key s -> ord x k.\n+-\n+  elim: {IH Sb S}s H => [|[k1 v1] s IH] //= L x.\n+rewrite inE; case/orP; last by apply: IH; apply: path_sorted L.\n+  move/eqP=> ->; elim: s {IH}L => [|[x1 w1] s IH] /=; first by rewrite andbT.\n+  by case/andP=> O/(ord_path O)/IH.\n+  rewrite (_ : FinMap _ = ins k v (FinMap S)).\n+-\n+  by apply: H2 (IH _) => x/T. by rewrite fmapE /= first_ins'. Qed.\n \n Fixpoint fcat' (s1 : fmap) (s2 : seq (K * V)) {struct s2} : fmap :=\n-  if s2 is (k, v)::t then fcat' (ins k v s1) t else s1.\n+  if s2 is (k, v) :: t then fcat' (ins k v s1) t else s1.\n \n Definition fcat s1 s2 := fcat' s1 (seq_of s2).\n \n-Lemma fcat_ins' k v s1 s2 : \n-        k \\notin (map key s2) -> fcat' (ins k v s1) s2 = ins k v (fcat' s1 s2). \n+Lemma fcat_ins' k v s1 s2 :\n+  k \\notin (map key s2) -> fcat' (ins k v s1) s2 = ins k v (fcat' s1 s2).\n Proof.\n-move=>H; elim: s2 k v s1 H=>[|[k2 v2] s2 IH] k1 v1 s1 //=.\n-rewrite inE negb_or; case/andP=>H1 H2.\n-by rewrite -IH // ins_ins eq_sym (negbTE H1).\n-Qed.\n+move=> H; elim: s2 k v s1 H => [|[k2 v2] s2 IH] k1 v1 s1 //=.\n+rewrite inE negb_or; case/andP=> H1 H2.\n+  by rewrite -IH // ins_ins eq_sym (negbTE H1). Qed.\n \n Lemma fcat_nil' s : fcat' nil (seq_of s) = s.\n Proof.\n-elim/fmap_ind': s=>[|k v s L IH] //=.\n-by rewrite seqof_ins //= (_ : FinMap _ = ins k v nil) // \n-     fcat_ins' ?notin_path // IH.\n-Qed.\n+elim/fmap_ind': s => [|k v s L IH] //=.\n+  by rewrite seqof_ins //= (_ : FinMap _ = ins k v nil) // fcat_ins' ?notin_path // IH. Qed.\n+\n+Lemma fcat0s s : fcat nil s = s.\n+Proof. by apply: fcat_nil'. Qed.\n \n-Lemma fcat0s s : fcat nil s = s. Proof. by apply: fcat_nil'. Qed.\n-Lemma fcats0 s : fcat s nil = s. Proof. by []. Qed.\n+Lemma fcats0 s : fcat s nil = s.\n+Proof. by []. Qed.\n \n-Lemma fcat_inss k v s1 s2 : \n-        k \\notin supp s2 -> fcat (ins k v s1) s2 = ins k v (fcat s1 s2).\n-Proof. by case: s2=>s2 p2 H /=; apply: fcat_ins'. Qed.\n+Lemma fcat_inss k v s1 s2 :\n+  k \\notin supp s2 -> fcat (ins k v s1) s2 = ins k v (fcat s1 s2).\n+Proof. by case: s2 => s2 p2 H /=; apply: fcat_ins'. Qed.\n \n-Lemma fcat_sins k v s1 s2 : \n-        fcat s1 (ins k v s2) = ins k v (fcat s1 s2).\n+Lemma fcat_sins k v s1 s2 :\n+  fcat s1 (ins k v s2) = ins k v (fcat s1 s2).\n Proof.\n-elim/fmap_ind': s2 k v s1=>[|k1 v1 s1 H1 IH k2 v2 s2] //.\n-case: (totalP k2 k1)=>//= H2.\n-- have H: path ord k2 (supp (ins k1 v1 s1)).\n-  - by apply: (path_supp_ins _ H2); apply: ord_path H1.\n-  by rewrite {1}/fcat seqof_ins //= fcat_ins' ?notin_path.\n-- by rewrite IH ins_ins H2 IH ins_ins H2.\n+elim/fmap_ind': s2 k v s1 => [|k1 v1 s1 H1 IH k2 v2 s2] //.\n+case: (totalP k2 k1) => //= H2.\n+-\n+have H: path ord k2 (supp (ins k1 v1 s1)).\n+-\n+by apply: (path_supp_ins _ H2); apply: ord_path H1.\n+by rewrite {1}/fcat seqof_ins //= fcat_ins' ?notin_path.\n+-\n+by rewrite IH ins_ins H2 IH ins_ins H2.\n have H: path ord k1 (supp (ins k2 v2 s1)) by apply: (path_supp_ins _ H2).\n rewrite ins_ins.\n case: (totalP k2 k1) H2 => // H2 _.\n-rewrite {1}/fcat seqof_ins //= fcat_ins' ?notin_path // IH ?notin_path //. \n+rewrite {1}/fcat seqof_ins //= fcat_ins' ?notin_path // IH ?notin_path //.\n rewrite ins_ins; case: (totalP k2 k1) H2 => // H2 _; congr (ins _ _ _).\n-by rewrite -/(fcat s2 (ins k2 v2 s1)) IH.\n-Qed. \n+by rewrite -/(fcat s2 (ins k2 v2 s1)) IH. Qed.\n \n-Lemma fcat_rems k s1 s2 : \n-        k \\notin supp s2 -> fcat (rem k s1) s2 = rem k (fcat s1 s2).\n+Lemma fcat_rems k s1 s2 : k \\notin supp s2 -> fcat (rem k s1) s2 = rem k (fcat s1 s2).\n Proof.\n-elim/fmap_ind': s2 k s1=>[|k2 v2 s2 H IH] k1 v1.\n+elim/fmap_ind': s2 k s1 => [|k2 v2 s2 H IH] k1 v1.\n - by rewrite !fcats0.\n-rewrite supp_ins inE /= negb_or; case/andP=>H1 H2.\n-by rewrite fcat_sins IH // ins_rem eq_sym (negbTE H1) -fcat_sins.\n-Qed.\n-\n-Lemma fcat_srem k s1 s2 : \n-        k \\notin supp s1 -> fcat s1 (rem k s2) = rem k (fcat s1 s2).\n-Proof.\n-elim/fmap_ind': s2 k s1=>[|k2 v2 s2 H IH] k1 s1.\n-- rewrite rem_empty fcats0.\n-  elim/fmap_ind': s1=>[|k3 v3 s3 H1 IH]; first by rewrite rem_empty.\n-  rewrite supp_ins inE /= negb_or.\n-  case/andP=>H2; move/IH=>E; rewrite {1}E . \n-  by rewrite ins_rem eq_sym (negbTE H2).\n-move=>H1; rewrite fcat_sins rem_ins; case: ifP=>E.\n-- by rewrite rem_ins E IH.\n-by rewrite rem_ins E -IH // -fcat_sins.\n-Qed.\n-\n-Lemma fnd_fcat k s1 s2 :  \n-        fnd k (fcat s1 s2) = \n-        if k \\in supp s2 then fnd k s2 else fnd k s1.\n-Proof.\n-elim/fmap_ind': s2 k s1=>[|k2 v2 s2 H IH] k1 s1.\n+rewrite supp_ins inE /= negb_or; case/andP=> H1 H2.\n+  by rewrite fcat_sins IH // ins_rem eq_sym (negbTE H1) -fcat_sins. Qed.\n+\n+Lemma fcat_srem k s1 s2 :\n+  k \\notin supp s1 -> fcat s1 (rem k s2) = rem k (fcat s1 s2).\n+Proof.\n+elim/fmap_ind': s2 k s1 => [|k2 v2 s2 H IH] k1 s1.\n+-\n+rewrite rem_empty fcats0.\n+elim/fmap_ind': s1 => [|k3 v3 s3 H1 IH]; first by rewrite rem_empty.\n+rewrite supp_ins inE /= negb_or.\n+case/andP=> H2; move/IH=> E; rewrite {1}E.\n+by rewrite ins_rem eq_sym (negbTE H2).\n+move=> H1; rewrite fcat_sins rem_ins; case: ifP=> E.\n+-\n+by rewrite rem_ins E IH.\n+  by rewrite rem_ins E -IH // -fcat_sins. Qed.\n+\n+Lemma fnd_fcat k s1 s2 :\n+  fnd k (fcat s1 s2) = if k \\in supp s2 then fnd k s2 else fnd k s1.\n+Proof.\n+elim/fmap_ind': s2 k s1 => [|k2 v2 s2 H IH] k1 s1.\n - by rewrite fcats0.\n rewrite supp_ins inE /=; case: ifP; last first.\n-- move/negbT; rewrite negb_or; case/andP=>H1 H2.\n-  by rewrite fcat_sins fnd_ins (negbTE H1) IH (negbTE H2).\n-case/orP; first by move/eqP=><-; rewrite fcat_sins !fnd_ins eq_refl.\n-move=>H1; rewrite fcat_sins !fnd_ins.\n-by case: ifP=>//; rewrite IH H1.\n-Qed.\n-\n-Lemma supp_fcat s1 s2 : supp (fcat s1 s2) =i [predU supp s1 & supp s2].\n-Proof.\n-elim/fmap_ind': s2 s1=>[|k v s L IH] s1.\n-- by rewrite supp_nil fcats0 => x; rewrite inE /= orbF.\n+-\n+move/negbT; rewrite negb_or; case/andP=> H1 H2.\n+by rewrite fcat_sins fnd_ins (negbTE H1) IH (negbTE H2).\n+case/orP; first by move/eqP=> <-; rewrite fcat_sins !fnd_ins eq_refl.\n+move=> H1; rewrite fcat_sins !fnd_ins.\n+  by case: ifP => //; rewrite IH H1. Qed.\n+\n+Lemma supp_fcat s1 s2 :\n+  supp (fcat s1 s2) =i [predU supp s1 & supp s2].\n+Proof.\n+elim/fmap_ind': s2 s1 => [|k v s L IH] s1.\n+-\n+by rewrite supp_nil fcats0 => x; rewrite inE /= orbF.\n rewrite fcat_sins ?notin_path // => x.\n-rewrite supp_ins !inE /=. \n-case E: (x == k)=>/=.\n-- by rewrite supp_ins inE /= E orbT.\n-by rewrite IH supp_ins inE /= inE /= E. \n-Qed.\n+rewrite supp_ins !inE /=.\n+case E: (x == k)=> /=.\n+-\n+by rewrite supp_ins inE /= E orbT.\n+  by rewrite IH supp_ins inE /= inE /= E. Qed.\n \n End Append.\n \n (* an induction principle for pairs of finite maps with equal support *)\n \n Section FMapInd.\n+\n Variables (K : ordType) (V : Type).\n Notation fmap := (finMap K V).\n Notation nil := (@nil K V).\n \n Lemma supp_eq_ins (s1 s2 : fmap) k1 k2 v1 v2 :\n-        path ord k1 (supp s1) -> path ord k2 (supp s2) ->\n-          supp (ins k1 v1 s1) =i supp (ins k2 v2 s2) -> \n-        k1 = k2 /\\ supp s1 =i supp s2.\n+    path ord k1 (supp s1) -> path ord k2 (supp s2) ->","path":"finmap/finmap.v","position":1045,"original_position":1045,"commit_id":"2556e23cc4336d41984c759e4f457003ea0ef4d9","original_commit_id":"2556e23cc4336d41984c759e4f457003ea0ef4d9","user":{"login":"anton-trunov","id":2316541,"node_id":"MDQ6VXNlcjIzMTY1NDE=","avatar_url":"https://avatars0.githubusercontent.com/u/2316541?v=4","gravatar_id":"","url":"https://api.github.com/users/anton-trunov","html_url":"https://github.com/anton-trunov","followers_url":"https://api.github.com/users/anton-trunov/followers","following_url":"https://api.github.com/users/anton-trunov/following{/other_user}","gists_url":"https://api.github.com/users/anton-trunov/gists{/gist_id}","starred_url":"https://api.github.com/users/anton-trunov/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/anton-trunov/subscriptions","organizations_url":"https://api.github.com/users/anton-trunov/orgs","repos_url":"https://api.github.com/users/anton-trunov/repos","events_url":"https://api.github.com/users/anton-trunov/events{/privacy}","received_events_url":"https://api.github.com/users/anton-trunov/received_events","type":"User","site_admin":false},"body":"This line should be aligned with the next one.","created_at":"2019-08-22T07:53:24Z","updated_at":"2019-08-22T07:53:25Z","html_url":"https://github.com/imdea-software/fcsl-pcm/pull/9#discussion_r316540812","pull_request_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/9","author_association":"COLLABORATOR","_links":{"self":{"href":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/comments/316540812"},"html":{"href":"https://github.com/imdea-software/fcsl-pcm/pull/9#discussion_r316540812"},"pull_request":{"href":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/9"}}},"pull_request":{"url":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/9","id":309649218,"node_id":"MDExOlB1bGxSZXF1ZXN0MzA5NjQ5MjE4","html_url":"https://github.com/imdea-software/fcsl-pcm/pull/9","diff_url":"https://github.com/imdea-software/fcsl-pcm/pull/9.diff","patch_url":"https://github.com/imdea-software/fcsl-pcm/pull/9.patch","issue_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/issues/9","number":9,"state":"open","locked":false,"title":"Roosterize formatting suggestions","user":{"login":"palmskog","id":397424,"node_id":"MDQ6VXNlcjM5NzQyNA==","avatar_url":"https://avatars2.githubusercontent.com/u/397424?v=4","gravatar_id":"","url":"https://api.github.com/users/palmskog","html_url":"https://github.com/palmskog","followers_url":"https://api.github.com/users/palmskog/followers","following_url":"https://api.github.com/users/palmskog/following{/other_user}","gists_url":"https://api.github.com/users/palmskog/gists{/gist_id}","starred_url":"https://api.github.com/users/palmskog/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/palmskog/subscriptions","organizations_url":"https://api.github.com/users/palmskog/orgs","repos_url":"https://api.github.com/users/palmskog/repos","events_url":"https://api.github.com/users/palmskog/events{/privacy}","received_events_url":"https://api.github.com/users/palmskog/received_events","type":"User","site_admin":false},"body":"@anton-trunov here is the PR with our formatting suggestions for the whole project. As discussed, we don't expect you to merge this, but hope you can do a review describing what you think about the proposed changes. We are interested in general comments (\"patterns\") and some specific examples with respect to:\r\n\r\n1. good suggestions\r\n2. bad suggestions, \r\n3. new or interesting insights given by the suggestions\r\n\r\nNote that this was generated based on training data from mathcomp, fourcolor, odd-order, and finmap, so the style implicit in those projects is what is used. We hope you can use the GitHub review mechanism to pinpoint some examples.\r\n\r\nThank you!","created_at":"2019-08-21T19:18:35Z","updated_at":"2019-08-22T07:53:25Z","closed_at":null,"merged_at":null,"merge_commit_sha":"df2a64ed3f063d9a568070e5444b357e5912c318","assignee":null,"assignees":[],"requested_reviewers":[],"requested_teams":[],"labels":[],"milestone":null,"commits_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/9/commits","review_comments_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/9/comments","review_comment_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/comments{/number}","comments_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/issues/9/comments","statuses_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/statuses/2556e23cc4336d41984c759e4f457003ea0ef4d9","head":{"label":"palmskog:roosterize-formatting","ref":"roosterize-formatting","sha":"2556e23cc4336d41984c759e4f457003ea0ef4d9","user":{"login":"palmskog","id":397424,"node_id":"MDQ6VXNlcjM5NzQyNA==","avatar_url":"https://avatars2.githubusercontent.com/u/397424?v=4","gravatar_id":"","url":"https://api.github.com/users/palmskog","html_url":"https://github.com/palmskog","followers_url":"https://api.github.com/users/palmskog/followers","following_url":"https://api.github.com/users/palmskog/following{/other_user}","gists_url":"https://api.github.com/users/palmskog/gists{/gist_id}","starred_url":"https://api.github.com/users/palmskog/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/palmskog/subscriptions","organizations_url":"https://api.github.com/users/palmskog/orgs","repos_url":"https://api.github.com/users/palmskog/repos","events_url":"https://api.github.com/users/palmskog/events{/privacy}","received_events_url":"https://api.github.com/users/palmskog/received_events","type":"User","site_admin":false},"repo":{"id":168840454,"node_id":"MDEwOlJlcG9zaXRvcnkxNjg4NDA0NTQ=","name":"fcsl-pcm","full_name":"palmskog/fcsl-pcm","private":false,"owner":{"login":"palmskog","id":397424,"node_id":"MDQ6VXNlcjM5NzQyNA==","avatar_url":"https://avatars2.githubusercontent.com/u/397424?v=4","gravatar_id":"","url":"https://api.github.com/users/palmskog","html_url":"https://github.com/palmskog","followers_url":"https://api.github.com/users/palmskog/followers","following_url":"https://api.github.com/users/palmskog/following{/other_user}","gists_url":"https://api.github.com/users/palmskog/gists{/gist_id}","starred_url":"https://api.github.com/users/palmskog/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/palmskog/subscriptions","organizations_url":"https://api.github.com/users/palmskog/orgs","repos_url":"https://api.github.com/users/palmskog/repos","events_url":"https://api.github.com/users/palmskog/events{/privacy}","received_events_url":"https://api.github.com/users/palmskog/received_events","type":"User","site_admin":false},"html_url":"https://github.com/palmskog/fcsl-pcm","description":"Partial Commutative Monoids","fork":true,"url":"https://api.github.com/repos/palmskog/fcsl-pcm","forks_url":"https://api.github.com/repos/palmskog/fcsl-pcm/forks","keys_url":"https://api.github.com/repos/palmskog/fcsl-pcm/keys{/key_id}","collaborators_url":"https://api.github.com/repos/palmskog/fcsl-pcm/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/palmskog/fcsl-pcm/teams","hooks_url":"https://api.github.com/repos/palmskog/fcsl-pcm/hooks","issue_events_url":"https://api.github.com/repos/palmskog/fcsl-pcm/issues/events{/number}","events_url":"https://api.github.com/repos/palmskog/fcsl-pcm/events","assignees_url":"https://api.github.com/repos/palmskog/fcsl-pcm/assignees{/user}","branches_url":"https://api.github.com/repos/palmskog/fcsl-pcm/branches{/branch}","tags_url":"https://api.github.com/repos/palmskog/fcsl-pcm/tags","blobs_url":"https://api.github.com/repos/palmskog/fcsl-pcm/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/palmskog/fcsl-pcm/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/palmskog/fcsl-pcm/git/refs{/sha}","trees_url":"https://api.github.com/repos/palmskog/fcsl-pcm/git/trees{/sha}","statuses_url":"https://api.github.com/repos/palmskog/fcsl-pcm/statuses/{sha}","languages_url":"https://api.github.com/repos/palmskog/fcsl-pcm/languages","stargazers_url":"https://api.github.com/repos/palmskog/fcsl-pcm/stargazers","contributors_url":"https://api.github.com/repos/palmskog/fcsl-pcm/contributors","subscribers_url":"https://api.github.com/repos/palmskog/fcsl-pcm/subscribers","subscription_url":"https://api.github.com/repos/palmskog/fcsl-pcm/subscription","commits_url":"https://api.github.com/repos/palmskog/fcsl-pcm/commits{/sha}","git_commits_url":"https://api.github.com/repos/palmskog/fcsl-pcm/git/commits{/sha}","comments_url":"https://api.github.com/repos/palmskog/fcsl-pcm/comments{/number}","issue_comment_url":"https://api.github.com/repos/palmskog/fcsl-pcm/issues/comments{/number}","contents_url":"https://api.github.com/repos/palmskog/fcsl-pcm/contents/{+path}","compare_url":"https://api.github.com/repos/palmskog/fcsl-pcm/compare/{base}...{head}","merges_url":"https://api.github.com/repos/palmskog/fcsl-pcm/merges","archive_url":"https://api.github.com/repos/palmskog/fcsl-pcm/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/palmskog/fcsl-pcm/downloads","issues_url":"https://api.github.com/repos/palmskog/fcsl-pcm/issues{/number}","pulls_url":"https://api.github.com/repos/palmskog/fcsl-pcm/pulls{/number}","milestones_url":"https://api.github.com/repos/palmskog/fcsl-pcm/milestones{/number}","notifications_url":"https://api.github.com/repos/palmskog/fcsl-pcm/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/palmskog/fcsl-pcm/labels{/name}","releases_url":"https://api.github.com/repos/palmskog/fcsl-pcm/releases{/id}","deployments_url":"https://api.github.com/repos/palmskog/fcsl-pcm/deployments","created_at":"2019-02-02T14:33:20Z","updated_at":"2019-08-21T19:23:15Z","pushed_at":"2019-08-22T00:48:54Z","git_url":"git://github.com/palmskog/fcsl-pcm.git","ssh_url":"git@github.com:palmskog/fcsl-pcm.git","clone_url":"https://github.com/palmskog/fcsl-pcm.git","svn_url":"https://github.com/palmskog/fcsl-pcm","homepage":null,"size":162,"stargazers_count":0,"watchers_count":0,"language":"Coq","has_issues":false,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":0,"mirror_url":null,"archived":false,"disabled":false,"open_issues_count":0,"license":{"key":"apache-2.0","name":"Apache License 2.0","spdx_id":"Apache-2.0","url":"https://api.github.com/licenses/apache-2.0","node_id":"MDc6TGljZW5zZTI="},"forks":0,"open_issues":0,"watchers":0,"default_branch":"master"}},"base":{"label":"imdea-software:master","ref":"master","sha":"581d17078eb2e813cda3db42070b8d0c67beba53","user":{"login":"imdea-software","id":6480782,"node_id":"MDEyOk9yZ2FuaXphdGlvbjY0ODA3ODI=","avatar_url":"https://avatars1.githubusercontent.com/u/6480782?v=4","gravatar_id":"","url":"https://api.github.com/users/imdea-software","html_url":"https://github.com/imdea-software","followers_url":"https://api.github.com/users/imdea-software/followers","following_url":"https://api.github.com/users/imdea-software/following{/other_user}","gists_url":"https://api.github.com/users/imdea-software/gists{/gist_id}","starred_url":"https://api.github.com/users/imdea-software/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/imdea-software/subscriptions","organizations_url":"https://api.github.com/users/imdea-software/orgs","repos_url":"https://api.github.com/users/imdea-software/repos","events_url":"https://api.github.com/users/imdea-software/events{/privacy}","received_events_url":"https://api.github.com/users/imdea-software/received_events","type":"Organization","site_admin":false},"repo":{"id":130369797,"node_id":"MDEwOlJlcG9zaXRvcnkxMzAzNjk3OTc=","name":"fcsl-pcm","full_name":"imdea-software/fcsl-pcm","private":false,"owner":{"login":"imdea-software","id":6480782,"node_id":"MDEyOk9yZ2FuaXphdGlvbjY0ODA3ODI=","avatar_url":"https://avatars1.githubusercontent.com/u/6480782?v=4","gravatar_id":"","url":"https://api.github.com/users/imdea-software","html_url":"https://github.com/imdea-software","followers_url":"https://api.github.com/users/imdea-software/followers","following_url":"https://api.github.com/users/imdea-software/following{/other_user}","gists_url":"https://api.github.com/users/imdea-software/gists{/gist_id}","starred_url":"https://api.github.com/users/imdea-software/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/imdea-software/subscriptions","organizations_url":"https://api.github.com/users/imdea-software/orgs","repos_url":"https://api.github.com/users/imdea-software/repos","events_url":"https://api.github.com/users/imdea-software/events{/privacy}","received_events_url":"https://api.github.com/users/imdea-software/received_events","type":"Organization","site_admin":false},"html_url":"https://github.com/imdea-software/fcsl-pcm","description":"Partial Commutative Monoids","fork":false,"url":"https://api.github.com/repos/imdea-software/fcsl-pcm","forks_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/forks","keys_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/keys{/key_id}","collaborators_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/teams","hooks_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/hooks","issue_events_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/issues/events{/number}","events_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/events","assignees_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/assignees{/user}","branches_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/branches{/branch}","tags_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/tags","blobs_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/git/refs{/sha}","trees_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/git/trees{/sha}","statuses_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/statuses/{sha}","languages_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/languages","stargazers_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/stargazers","contributors_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/contributors","subscribers_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/subscribers","subscription_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/subscription","commits_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/commits{/sha}","git_commits_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/git/commits{/sha}","comments_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/comments{/number}","issue_comment_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/issues/comments{/number}","contents_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/contents/{+path}","compare_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/compare/{base}...{head}","merges_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/merges","archive_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/downloads","issues_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/issues{/number}","pulls_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls{/number}","milestones_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/milestones{/number}","notifications_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/labels{/name}","releases_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/releases{/id}","deployments_url":"https://api.github.com/repos/imdea-software/fcsl-pcm/deployments","created_at":"2018-04-20T14:00:35Z","updated_at":"2019-07-03T09:47:10Z","pushed_at":"2019-08-22T00:48:55Z","git_url":"git://github.com/imdea-software/fcsl-pcm.git","ssh_url":"git@github.com:imdea-software/fcsl-pcm.git","clone_url":"https://github.com/imdea-software/fcsl-pcm.git","svn_url":"https://github.com/imdea-software/fcsl-pcm","homepage":null,"size":126,"stargazers_count":11,"watchers_count":11,"language":"Coq","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":2,"mirror_url":null,"archived":false,"disabled":false,"open_issues_count":3,"license":{"key":"apache-2.0","name":"Apache License 2.0","spdx_id":"Apache-2.0","url":"https://api.github.com/licenses/apache-2.0","node_id":"MDc6TGljZW5zZTI="},"forks":2,"open_issues":3,"watchers":11,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/9"},"html":{"href":"https://github.com/imdea-software/fcsl-pcm/pull/9"},"issue":{"href":"https://api.github.com/repos/imdea-software/fcsl-pcm/issues/9"},"comments":{"href":"https://api.github.com/repos/imdea-software/fcsl-pcm/issues/9/comments"},"review_comments":{"href":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/9/comments"},"review_comment":{"href":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/imdea-software/fcsl-pcm/pulls/9/commits"},"statuses":{"href":"https://api.github.com/repos/imdea-software/fcsl-pcm/statuses/2556e23cc4336d41984c759e4f457003ea0ef4d9"}},"author_association":"CONTRIBUTOR"}}
{"actor":{"display_login":"anton-trunov"}}