update for fcsl-pcm

examples/bubblesort.v

@@ -167,7 +167,7 @@ Proof.
 case: k=>//= k; rewrite ltnS=>Hk.
 suff E: {in drop k.+1 (enum 'I_n.+1), f =1 (pffun (pswnx i) f)}.
 - by rewrite /= !codomE -2!map_drop /=; move/eq_in_map: E.
-move=>/= y /index_gtn; rewrite index_last_uniq; last by apply: enum_uniq.
+move=>/= y /index_geq; rewrite index_last_uniq; last by apply: enum_uniq.
 rewrite /pswnx ffunE index_enum_ord=>Hy.
 have {Hk}Hy: i.+1 < y.
 - rewrite -ltn_predRL; apply: (leq_trans Hk).

examples/congmath.v

@@ -4,7 +4,7 @@
 
 From Coq Require Import Recdef ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype choice ssrnat seq bigop fintype finfun.
-From pcm Require Import options prelude ordtype finmap pred.
+From pcm Require Import options prelude ordtype finmap pred seqext.
 From htt Require Import interlude.
 
 Ltac add_morphism_tactic := SetoidTactics.add_morphism_tactic.

htt/interlude.v

@@ -145,164 +145,3 @@ by rewrite (allrel_trans (@trans A) Hl Hr).
 Qed.
 
 End SeqOrd.
-
-Section FindLast.
-
-Variables (T : Type).
-Implicit Types (x : T) (p : pred T) (s : seq T).
-
-(* find the last occurence in a single pass *)
-Definition find_last_aux oi0 p s :=
-  foldl (fun '(o,i) x => (if p x then Some i else o, i.+1)) oi0 s.
-
-Lemma find_last_auxE oi0 p s :
-        find_last_aux oi0 p s =
-        let k := seq.find p (rev s) in
-        (if k == size s then oi0.1
-           else Some (oi0.2 + (size s - k).-1), oi0.2 + size s).
-Proof.
-rewrite /find_last_aux; elim: s oi0=>/= [|x s IH] [o0 i0] /=; first by rewrite addn0.
-rewrite IH /= rev_cons -cats1 find_cat /= has_find.
-move: (find_size p (rev s)); rewrite size_rev; case: ltngtP=>// H _.
-- case: eqP=>[E|_]; first by rewrite E ltnNge leqnSn in H.
-  apply: injective_projections=>/=; [congr Some | rewrite addSnnS]=>//.
-  by rewrite !predn_sub /= -predn_sub addSnnS prednK // subn_gt0.
-case: ifP=>_; rewrite addSnnS; last by rewrite addn1 eqxx.
-by rewrite addn0 eqn_leq leqnSn /= ltnn subSnn addn0.
-Qed.
-
-Definition find_last p s :=
-  let '(o, i) := find_last_aux (None, 0) p s in odflt i o.
-
-(* finding last is finding first in reversed list and flipping indices *)
-Corollary find_lastE p s :
-            find_last p s =
-            if has p s then (size s - seq.find p (rev s)).-1
-                       else size s.
-Proof.
-rewrite /find_last find_last_auxE /= !add0n -has_rev; case/boolP: (has p (rev s)).
-- by rewrite has_find size_rev; case: ltngtP.
-by move/hasNfind=>->; rewrite size_rev eqxx.
-Qed.
-
-Lemma find_last_size p s : find_last p s <= size s.
-Proof.
-rewrite find_lastE; case: ifP=>// _.
-by rewrite -subnS; apply: leq_subr.
-Qed.
-
-Lemma has_find_last p s : has p s = (find_last p s < size s).
-Proof.
-symmetry; rewrite find_lastE; case: ifP=>H /=; last by rewrite ltnn.
-by rewrite -subnS /= ltn_subrL /=; case: s H.
-Qed.
-
-Lemma hasNfind_last p s : ~~ has p s -> find_last p s = size s.
-Proof. by rewrite has_find_last; case: ltngtP (find_last_size p s). Qed.
-
-Lemma nth_find_last x0 p s : has p s -> p (nth x0 s (find_last p s)).
-Proof.
-rewrite find_lastE=>/[dup] E ->; rewrite -has_rev in E.
-rewrite -subnS -nth_rev; last by rewrite -size_rev -has_find.
-by apply: nth_find.
-Qed.
-
-Lemma has_drop p s i : has p s -> has p (drop i.+1 s) = (i < find_last p s).
-Proof.
-rewrite find_lastE=>/[dup] E ->; rewrite -has_rev in E.
-rewrite -(size_rev s); move/(has_take (size s - i).-1): E.
-rewrite take_rev -subnS size_rev.
-case/boolP: (i < size s)=>[Hi|].
-- rewrite subnA // subnn add0n has_rev => ->.
-  by rewrite -subnS ltn_subRL addnC -addSnnS -ltn_subRL.
-rewrite -ltnNge ltnS => Hi _.
-rewrite drop_oversize /=; last by apply: (leq_trans Hi).
-symmetry; apply/negbTE; rewrite -ltnNge ltnS.
-by apply/leq_trans/Hi; rewrite -subnS; exact: leq_subr.
-Qed.
-
-Lemma find_gtn p s i : has p (drop i.+1 s) -> i < find_last p s.
-Proof.
-case/boolP: (has p s)=>Hp; first by rewrite (has_drop _ Hp).
-suff: ~~ has p (drop i.+1 s) by move/negbTE=>->.
-move: Hp; apply: contra; rewrite -{2}(cat_take_drop i.+1 s) has_cat=>->.
-by rewrite orbT.
-Qed.
-
-Variant split_find_last_nth_spec p : seq T -> seq T -> seq T -> T -> Type :=
-  FindLastNth x s1 s2 of p x & ~~ has p s2 :
-    split_find_last_nth_spec p (rcons s1 x ++ s2) s1 s2 x.
-
-Lemma split_find_last_nth x0 p s (i := find_last p s) :
-        has p s ->
-        split_find_last_nth_spec p s (take i s) (drop i.+1 s) (nth x0 s i).
-Proof.
-move=> p_s; rewrite -[X in split_find_last_nth_spec _ X](cat_take_drop i s).
-rewrite (drop_nth x0 _); last by rewrite -has_find_last.
-rewrite -cat_rcons; constructor; first by apply: nth_find_last.
-by rewrite has_drop // ltnn.
-Qed.
-
-Variant split_find_last_spec p : seq T -> seq T -> seq T -> Type :=
-  FindLastSplit x s1 s2 of p x & ~~ has p s2 :
-    split_find_last_spec p (rcons s1 x ++ s2) s1 s2.
-
-Lemma split_find_last p s (i := find_last p s) :
-        has p s ->
-        split_find_last_spec p s (take i s) (drop i.+1 s).
-Proof.
-by case: s => // x ? in i * =>?; case: split_find_last_nth=>//; constructor.
-Qed.
-
-End FindLast.
-
-Section FindLastEq.
-
-Variables (T : eqType).
-Implicit Type p : seq T.
-
-Definition index_last (x : T) := find_last (pred1 x).
-
-Lemma memNindex_last x s : x \notin s -> index_last x s = size s.
-Proof. by rewrite -has_pred1=>/hasNfind_last. Qed.
-
-Lemma index_last_cons x y t : index_last x (y::t) =
-        if x \in t then (index_last x t).+1
-          else if y == x then 0 else (size t).+1.
-Proof.
-rewrite /index_last !find_lastE /= rev_cons -cats1 find_cat /= has_rev has_pred1.
-case/boolP: (x \in t)=>H; last first.
-- rewrite size_rev orbF; case/boolP: (y == x)=>//= _.
-  by rewrite addn0 subSnn.
-by rewrite orbT predn_sub /= prednK // subn_gt0 -size_rev -has_find has_rev has_pred1.
-Qed.
-
-Lemma index_gtn x s i : x \in drop i.+1 s -> i < index_last x s.
-Proof. by rewrite -has_pred1; apply: find_gtn. Qed.
-
-Lemma index_last_uniq x s : uniq s -> index_last x s = index x s.
-Proof.
-move=>H; case/boolP: (x \in s)=>Hx; last first.
-- by rewrite (memNindex_last Hx) (memNindex Hx).
-elim: s x H Hx=>//= h t IH x.
-rewrite index_last_cons.
-case/andP=>Hh Ht; rewrite inE eq_sym; case/orP.
-- by move/eqP=>{x}<-; rewrite (negbTE Hh) eqxx.
-move=>Hx; rewrite Hx; case: eqP=>[E|_]; last by congr S; apply: IH.
-by rewrite E Hx in Hh.
-Qed.
-
-Variant splitLast x : seq T -> seq T -> seq T -> Type :=
-  SplitLast p1 p2 of x \notin p2 : splitLast x (rcons p1 x ++ p2) p1 p2.
-
-Lemma splitLastP s x (i := index_last x s) :
-        x \in s ->
-        splitLast x s (take i s) (drop i.+1 s).
-Proof.
-case: s => // y s in i * => H.
-case: split_find_last_nth=>//; first by rewrite has_pred1.
-move=>_ s1 s2 /= /eqP->; rewrite has_pred1 => H2.
-by constructor.
-Qed.
-
-End FindLastEq.