From 77438ed942c9d99530bd6b0275524ef3b5293646 Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Fri, 11 Nov 2022 04:01:06 +0100 Subject: [PATCH] update for fcsl-pcm --- examples/bubblesort.v | 2 +- examples/congmath.v | 2 +- htt/interlude.v | 161 ------------------------------------------ 3 files changed, 2 insertions(+), 163 deletions(-) diff --git a/examples/bubblesort.v b/examples/bubblesort.v index 0062a8d..34fc81f 100644 --- a/examples/bubblesort.v +++ b/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). diff --git a/examples/congmath.v b/examples/congmath.v index 70f3780..fde0566 100755 --- a/examples/congmath.v +++ b/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. diff --git a/htt/interlude.v b/htt/interlude.v index fb24939..e023e5b 100644 --- a/htt/interlude.v +++ b/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. \ No newline at end of file