chip.check_seq_hierarchical
From mathcomp
Require Import all_ssreflect.
From chip
Require Import extra connect closure check check_seq change hierarchical hierarchical_sub hierarchical_sub_pt hierarchical_sub_correct hierarchical_sub_pt_correct tarjan_acyclic.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section CheckedSeqHierarchical.
Variable (A_top : eqType) (A_bot : eqType).
Variable (U' : finType) (V' : finType).
Variable (f'_top : U' -> A_top) (f'_bot : V' -> A_bot).
Variable (P_top : pred U') (P_bot : pred V').
Local Notation U := (sig_finType P_top).
Local Notation V := (sig_finType P_bot).
Variable (f_top : U -> A_top) (f_bot : V -> A_bot).
Variable g_top_rev : U -> seq U.
Variable g_bot_rev : V -> seq V.
Variable p : U -> seq V.
Variable p' : U' -> seq V'.
Variable (checkable'_bot : pred V').
Variable clos_top : (U -> seq U) -> seq U -> seq U.
Hypothesis clos_topP : forall successors (s : seq U) (x : U),
reflect
(exists2 v, v \in s & connect (grel successors) v x)
(x \in clos_top successors s).
Variable clos_bot : (V -> seq V) -> seq V -> seq V.
Hypothesis clos_botP : forall successors (s : seq V) (x : V),
reflect
(exists2 v, v \in s & connect (grel successors) v x)
(x \in clos_bot successors s).
(* defs *)
Definition seq_modifiedU := [seq u <- enum U | f_top u != f'_top (val u)].
Definition seq_impactedU := clos_top g_top_rev seq_modifiedU.
Definition seq_freshU' := [seq u <- enum U' | ~~ P_top u].
Definition seq_pmodified_V := flatten [seq (p u) | u <- seq_modifiedU].
Definition seq_pimpacted_V := flatten [seq (p u) | u <- seq_impactedU].
Definition seq_pfreshV' :=
flatten [seq (p' u) | u <- seq_freshU'] ++ flatten [seq (p' (val u)) | u <- seq_modifiedU].
Definition P_V_seq_sub v := v \in seq_pimpacted_V.
Definition g_bot_rev_sub (v : V) := [seq v <- g_bot_rev v | P_V_seq_sub v].
Definition seq_modifiedV_sub := [seq v <- seq_pmodified_V | f_bot v != f'_bot (val v)].
Definition seq_impactedV_sub := clos_bot g_bot_rev_sub seq_modifiedV_sub.
Definition seq_impactedVV'_sub := [seq val v | v <- seq_impactedV_sub].
Definition seq_freshV' := [seq v <- enum V' | ~~ P_bot v].
Definition seq_freshV'_sub := [seq v <- seq_pfreshV' | ~~ P_bot v].
Definition seq_impacted_fresh_sub := seq_impactedVV'_sub ++ seq_freshV'.
Definition seq_checkable_impacted_fresh_sub :=
[seq v <- seq_impacted_fresh_sub | checkable'_bot v].
Definition seq_impacted_fresh_sub_pt := seq_impactedVV'_sub ++ seq_freshV'_sub.
Definition seq_checkable_impacted_fresh_sub_pt :=
[seq v <- seq_impacted_fresh_sub_pt | checkable'_bot v].
(* proofs *)
Variable g_top : rel U.
Hypothesis g_top_grev : [rel x y | g_top y x] =2 grel g_top_rev.
Lemma seq_modifiedU_eq :
modifiedV f'_top f_top =i seq_modifiedU.
Proof.
by move => x; rewrite inE mem_filter mem_enum andb_idr.
Qed.
Lemma seq_impactedU_eq :
impacted g_top^-1 (modifiedV f'_top f_top) =i seq_impactedU.
Proof.
move => x.
apply/impactedVP.
case: ifP.
- move/clos_topP => [v Hv] Hc.
move: Hv.
rewrite -seq_modifiedU_eq => Hv.
exists v => //.
move/connectP: Hc => [p0 Hp] Hl.
apply/connectP.
exists p0 => //.
elim: p0 v Hp {Hv Hl} => //.
move => v p0 IH v0.
rewrite /=.
move/andP => [Hv Hp].
apply/andP.
split; last by apply: IH.
move: Hv.
have Hb := (g_top_grev v0 v).
rewrite /= in Hb.
by rewrite Hb.
- move/negP => Hs.
move => [y Hy] Hc.
case: Hs.
apply/clos_topP.
move: Hy.
rewrite seq_modifiedU_eq => Hy.
exists y => //.
move/connectP: Hc => [p0 Hp0] Hl.
apply/connectP.
exists p0 => //.
elim: p0 y Hp0 {Hl Hy} => //.
move => v p0 IH v0.
rewrite /=.
move/andP => [Hv Hp].
apply/andP.
split; last by apply: IH.
move: Hv.
have Hb := (g_top_grev v0 v).
rewrite /= in Hb.
by rewrite Hb.
Qed.
Lemma seq_freshU'_eq :
freshV' P_top =i seq_freshU'.
Proof.
by move => x; rewrite inE mem_filter mem_enum andb_idr.
Qed.
Variables (ps : U -> {set V}).
Hypothesis p_ps_eq : forall u : U, p u =i ps u.
Hypothesis ps_partition : partition (\bigcup_( u | u \in U ) [set ps u]) [set: V].
Lemma seq_pimpacted_V_eq :
pimpacted_sub_V f'_top g_top f_top ps =i seq_pimpacted_V.
Proof.
move => x.
apply/bigcupP.
case: ifP => Hm.
- move/flattenP: Hm => [us Hus] Hx.
move/mapP: Hus => [y Hy] Hyu.
exists y; last by rewrite -p_ps_eq -Hyu.
by rewrite seq_impactedU_eq.
- move/negP: Hm => Hm [u Hu] Hx.
case: Hm.
apply/flattenP.
exists (p u); last by rewrite p_ps_eq.
apply/mapP.
exists u => //.
by rewrite -seq_impactedU_eq.
Qed.
Lemma P_V_sub_V_seq_sub_eq :
P_V_sub f'_top g_top f_top ps =i P_V_seq_sub.
Proof.
move => x.
apply/idP/idP.
- by rewrite seq_pimpacted_V_eq.
- by rewrite seq_pimpacted_V_eq.
Qed.
Variables (ps' : U' -> {set V'}).
Hypothesis p'_ps'_eq : forall u : U', p' u =i ps' u.
Hypothesis ps'_partition : partition (\bigcup_( u | u \in U' ) [set ps' u]) [set: V'].
Lemma seq_pfreshV'_eq : pfreshV' f'_top f_top ps' =i seq_pfreshV'.
Proof.
move => x.
apply/idP/idP.
- case/setUP => Hp; rewrite mem_cat; apply/orP.
* left.
apply/flattenP.
move/bigcupP: Hp => [u' Hu'] Hx.
exists (p' u').
+ apply/mapP.
exists u' => //.
by rewrite -seq_freshU'_eq.
+ by rewrite p'_ps'_eq.
* right.
apply/flattenP.
move/bigcupP: Hp => [u Hu] Hx.
exists (p' (val u)); last by rewrite p'_ps'_eq.
apply/mapP.
exists u => //.
by rewrite -seq_modifiedU_eq.
- rewrite mem_cat; case/orP; move/flattenP => [vs Hvs] Hx.
* apply/setUP.
left.
apply/bigcupP.
move/mapP: Hvs => [u Hu] Huv.
exists u; first by rewrite seq_freshU'_eq.
by rewrite -p'_ps'_eq -Huv.
* move/mapP: Hvs => [u Hu] Huv.
apply/setUP.
right.
apply/bigcupP.
exists u; first by rewrite seq_modifiedU_eq.
by rewrite -p'_ps'_eq -Huv.
Qed.
Variable g_bot : rel V.
Hypothesis g_bot_grev : [rel x y | g_bot y x] =2 grel g_bot_rev.
Hypothesis f_top_bot_ps : forall (u : U),
f_top u = f'_top (val u) -> forall (v : V), v \in ps u -> f_bot v = f'_bot (val v).
Lemma seq_modifiedV_sub_eq : forall z,
(val z \in seq_modifiedV_sub) =
(z \in modifiedV_sub f'_top f'_bot g_top f_top f_bot ps).
Proof.
move => z.
apply/idP/idP.
- rewrite mem_filter.
move/andP => [Hz Ha].
rewrite inE.
move/flattenP: Ha => [x Hx] Hzx.
apply/andP; split => //.
apply/bigcupP.
move/mapP: Hx => [u Hu] Hxu.
exists u; last by rewrite -p_ps_eq -Hxu.
by rewrite seq_modifiedU_eq.
- move => Hz.
rewrite mem_filter.
apply/andP.
move: Hz.
rewrite inE.
move/andP => [Hz Hf].
split => //.
move/bigcupP: Hz => [u Hu] Huz.
apply/flattenP.
exists (p u); last by rewrite p_ps_eq.
apply/mapP.
exists u => //.
by rewrite -seq_modifiedU_eq.
Qed.
Lemma g_bot_rev_sub_eqq : forall x y : sig_finType (P_V_sub f'_top g_top f_top ps),
((grel g_bot_rev_sub) (val x) (val y)) = (g_bot (val y) (val x)).
Proof.
move => x y.
rewrite /=.
apply/idP/idP.
- rewrite mem_filter.
move/andP.
move => [Hp Hv].
have Hb := g_bot_grev (val x) (val y).
rewrite /= in Hb.
by rewrite -Hb in Hv.
- have Hb := g_bot_grev (val x) (val y).
rewrite /= in Hb.
rewrite Hb /=.
move => Hs.
rewrite mem_filter.
rewrite Hs.
apply/andP; split => //.
rewrite /P_V_seq_sub.
rewrite -P_V_sub_V_seq_sub_eq.
have H_sp := (insubP (sig_subFinType (P_V_sub f'_top g_top f_top ps)) (val y)).
by destruct H_sp; last by case/negP: i; apply valP.
Qed.
Lemma connect_rel_sub : forall (y z : sig_finType (P_V_sub f'_top g_top f_top ps)),
connect [rel x0 y0 | g_bot (val x0) (val y0)] y z ->
connect (grel g_bot_rev_sub) (val z) (val y).
Proof.
move => y z.
move/connectP => [pt Hpt] Hz.
apply connect_rev.
apply/connectP.
exists (map val pt); last by rewrite last_map Hz.
clear Hz.
elim: pt y Hpt => //.
move => a pt IH y.
rewrite /=.
move/andP => [Hg Hp].
apply/andP.
split; last by apply: IH.
by rewrite -g_bot_rev_sub_eqq in Hg.
Qed.
Lemma connect_g_bot_rev_sub_g_bot_rev : forall v y,
connect (grel g_bot_rev_sub) v y ->
connect g_bot^-1 v y.
Proof.
move => v y.
move/connectP => [pt Hpt] Hl.
apply/connectP.
exists pt => //.
elim: pt v Hpt {Hl} => //.
move => z pt IH v.
rewrite /=.
move/andP => [Hz Hp].
apply/andP.
rewrite mem_filter in Hz.
move/andP: Hz => [Hzp Hgb].
have Hg := g_bot_grev v z.
rewrite /= in Hg.
rewrite -Hg in Hgb.
split => //.
by apply: IH.
Qed.
Hypothesis g_bot_top_ps : forall (v v' : V) (u u' : U),
u <> u' -> g_bot v v' -> v \in ps u -> v' \in ps u' -> g_top u u'.
(* ps is injective *)
Hypothesis ps_neq : forall (u u' : U), u <> u' -> ps u <> ps u'.
Hypothesis ps'_neq : forall (u u' : U'), u <> u' -> ps' u <> ps' u'.
Hypothesis f_top_partition : forall (u : U),
f_top u = f'_top (val u) -> [set val v | v in ps u] = ps' (val u).
Lemma seq_impactedVV'_sub_eq :
impactedVV'_sub f'_top f'_bot g_top g_bot f_top f_bot ps =i seq_impactedVV'_sub.
Proof.
move => x.
apply/idP/idP.
- move/imsetP => [y Hy] Hyx.
apply/mapP.
exists (val y) => //.
move/impactedP: Hy => [z Hz] Hyz.
apply/clos_botP.
exists (val z); first by rewrite seq_modifiedV_sub_eq.
move: Hyz.
move/connect_rev => /=.
by apply connect_rel_sub.
- move/mapP => [y Hy] Hyx.
move/clos_botP: Hy => [v Hv] Hc.
apply/imsetP.
have H_sp := (insubP (sig_subFinType (P_V_sub f'_top g_top f_top ps)) v).
destruct H_sp; last first.
case/negP: i.
rewrite /P_V_sub.
move: Hv.
rewrite mem_filter.
move/andP => [Hf Hs].
have Hv: v \in modifiedV f'_bot f_bot by rewrite inE.
suff Hsuff: v \in pmodified_sub_V f'_top f_top ps.
move/bigcupP: Hsuff => [u Hu] Huv.
apply/bigcupP.
exists u => //.
apply/impactedP.
by exists u.
move: Hv.
by apply modifiedV_pmodified_sub_V.
rewrite -e in Hv.
rewrite seq_modifiedV_sub_eq in Hv.
apply connect_g_bot_rev_sub_g_bot_rev in Hc.
rewrite inE in Hv.
move/andP: Hv => [Hvp Hfb].
rewrite e in Hfb.
have Hyi: y \in impacted g_bot^-1 (modifiedV f'_bot f_bot).
apply/impactedP.
exists v => //.
by rewrite inE.
have H_sp := (insubP (sig_subFinType (P_V_sub f'_top g_top f_top ps)) y).
destruct H_sp.
rewrite -e0 in Hyi.
apply impactedV_impactedV_sub_eq in Hyi => //.
by exists u0; last by rewrite e0.
case/negP: i0.
rewrite /P_V_sub.
rewrite /pimpacted_sub_V /pimpacted_V.
apply/bigcupP.
have Hp := ps_partition.
move/andP: Hp => [Hcc Hp].
move/andP: Hp => [Htr H0].
move: Hcc.
rewrite /cover.
move/eqP => Hcc.
have Hyy: y \in \bigcup_(B in \bigcup_(u in U) [set ps u]) B by rewrite Hcc inE.
move/bigcupP: Hyy => [ys Hyy] Hys.
move/bigcupP: Hyy => [u0 Hu0] Huys.
exists u0; last by move: Huys; rewrite inE; move/eqP =><-.
rewrite inE in Huys.
move/eqP: Huys => Huys.
rewrite Huys in Hys.
apply/impactedP.
have Hvv: v \in \bigcup_(B in \bigcup_(u in U) [set ps u]) B by rewrite Hcc inE.
move/bigcupP: Hvv => [vs Hvv] Hvs.
move/bigcupP: Hvv => [u1 Hu1] Huvs.
rewrite inE in Huvs.
move/eqP: Huvs => Huvs.
rewrite Huvs in Hvs.
exists u1.
- rewrite inE.
apply/eqP => Hf.
case/negP: Hfb.
apply/eqP.
by have f_topb := f_top_bot_ps Hf Hvs.
- move: Hys Hvs Hc.
by apply connect_rev_v_u.
Qed.
Lemma seq_freshV'_sub_eq :
freshV'_sub f'_top P_bot f_top ps' =i seq_freshV'_sub.
Proof.
by move => x; apply/idP/idP; rewrite inE mem_filter -seq_pfreshV'_eq andbC.
Qed.
Lemma seq_impacted_fresh_sub_eq :
impactedV'_sub f'_top f'_bot g_top g_bot f_top f_bot ps =i seq_impacted_fresh_sub.
Proof.
move => x.
apply/idP/idP.
- rewrite mem_cat.
case/setUP => Hx.
* apply/orP; left.
by rewrite -seq_impactedVV'_sub_eq.
* apply/orP; right.
by rewrite -seq_freshV'_eq.
- rewrite mem_cat.
move/orP; case => Hx.
* apply/setUP.
left.
by rewrite seq_impactedVV'_sub_eq.
* apply/setUP.
right.
by rewrite seq_freshV'_eq.
Qed.
Lemma seq_impacted_fresh_sub_pt_eq :
impactedV'_sub_pt f'_top f'_bot g_top g_bot f_top f_bot ps ps' =i
seq_impacted_fresh_sub_pt.
Proof.
move => x.
apply/idP/idP.
- case/setUP => Hx.
* rewrite mem_cat.
apply/orP.
left.
by rewrite -seq_impactedVV'_sub_eq.
* rewrite mem_cat.
apply/orP.
right.
by rewrite -seq_freshV'_sub_eq.
- rewrite mem_cat.
case/orP => Hx.
* apply/setUP.
left.
by rewrite seq_impactedVV'_sub_eq.
* apply/setUP.
right.
by rewrite seq_freshV'_sub_eq.
Qed.
Lemma seq_impacted_fresh_sub_correct :
seq_impacted_fresh_sub =i impactedV' f'_bot f_bot g_bot.
Proof.
move => x.
apply/idP/idP.
- rewrite -seq_impacted_fresh_sub_eq.
by rewrite impactedV'_sub_eq //.
- rewrite -seq_impacted_fresh_sub_eq.
by rewrite impactedV'_sub_eq //.
Qed.
Lemma seq_impacted_fresh_sub_pt_correct :
seq_impacted_fresh_sub_pt =i impactedV' f'_bot f_bot g_bot.
Proof.
move => x.
apply/idP/idP.
- rewrite -seq_impacted_fresh_sub_pt_eq.
by rewrite impactedV'_sub_pt_eq //.
- rewrite -seq_impacted_fresh_sub_pt_eq.
by rewrite impactedV'_sub_pt_eq //.
Qed.
Lemma seq_checkable_impacted_fresh_sub_correct :
seq_checkable_impacted_fresh_sub =i
checkable_impactedV' f'_bot f_bot g_bot checkable'_bot.
Proof.
move => x.
rewrite mem_filter.
apply/idP/idP.
- move/andP => [Hc Hx].
rewrite inE.
apply/andP; split => //.
by rewrite -seq_impacted_fresh_sub_correct.
- rewrite inE.
move/andP => [Hc Hi].
apply/andP.
split => //.
by rewrite seq_impacted_fresh_sub_correct.
Qed.
Lemma seq_checkable_impacted_fresh_sub_pt_correct :
seq_checkable_impacted_fresh_sub_pt =i
checkable_impactedV' f'_bot f_bot g_bot checkable'_bot.
Proof.
move => x.
rewrite mem_filter.
apply/idP/idP.
- move/andP => [Hc Hx].
rewrite inE.
apply/andP; split => //.
by rewrite -seq_impacted_fresh_sub_pt_correct.
- rewrite inE.
move/andP => [Hc Hi].
apply/andP.
split => //.
by rewrite seq_impacted_fresh_sub_pt_correct.
Qed.
Hypothesis clos_top_uniq : forall successors (s : seq U),
uniq s -> uniq (clos_top successors s).
Hypothesis clos_bot_uniq : forall successors (s : seq V),
uniq s -> uniq (clos_bot successors s).
Hypothesis p_uniq : forall u, uniq (p u).
Hypothesis p'_uniq : forall u, uniq (p' u).
Lemma seq_modifiedU_uniq : uniq seq_modifiedU.
Proof.
exact: seq_modifiedV_uniq.
Qed.
Lemma seq_impactedU_uniq : uniq seq_impactedU.
Proof.
by apply/clos_top_uniq/seq_modifiedU_uniq.
Qed.
Lemma seq_pmodified_V_uniq : uniq seq_pmodified_V.
Proof.
apply uniq_flatten.
- elim => //.
move => v l IH.
move/mapP => [u Hu] Hp.
rewrite Hp.
exact: p_uniq.
- rewrite map_inj_in_uniq; first by apply seq_modifiedU_uniq.
move => x y Hx Hy Hp.
case Hxy: (x == y); first by move/eqP: Hxy.
move/eqP: Hxy => Hxy.
apply ps_neq in Hxy.
case: Hxy.
apply/setP.
move => v.
by rewrite -2!p_ps_eq Hp.
- move => l l'.
move/mapP => [u Hu] Hlu.
move/mapP => [u' Hu'] Hlu' Hneq.
rewrite Hlu Hlu'.
case Heq: (u == u').
move/eqP: Heq Hlu =>->.
move => Hlu.
case/eqP: Hneq.
by rewrite Hlu' Hlu.
move/eqP: Heq => Heq.
have Hp := ps_partition.
move/andP: Hp => [Hcc Hp].
move/andP: Hp => [Htr H0].
move/trivIsetP: Htr => Htr.
have Hpu: ps u \in \bigcup_(u in U) [set ps u].
apply/bigcupP.
exists u => //=.
by rewrite in_set1.
have Hpu': ps u' \in \bigcup_(u in U) [set ps u].
apply/bigcupP.
exists u' => //=.
by rewrite in_set1.
have Hneq': ps u != ps u'.
apply/negP/negP/eqP => Hpp.
contradict Hpp.
exact: ps_neq.
have Hpp := Htr _ _ Hpu Hpu' Hneq'.
rewrite disjoint_subset.
apply/subsetP.
move => x.
rewrite p_ps_eq => Hx.
rewrite inE.
apply/negP.
case => Hp.
have Hy: x \in p u' by [].
move: Hy.
rewrite p_ps_eq => Hy.
move: Hpp.
rewrite disjoint_subset.
move/subsetP => Hs.
move/Hs: Hx.
rewrite inE.
move/negP.
by case.
Qed.
Lemma seq_pimpacted_V_uniq : uniq seq_pimpacted_V.
Proof.
apply uniq_flatten.
- elim => //.
move => v l IH.
move/mapP => [u Hu] Hp.
rewrite Hp.
exact: p_uniq.
- rewrite map_inj_in_uniq; first by apply seq_impactedU_uniq.
move => x y Hx Hy Hp.
case Hxy: (x == y); first by move/eqP: Hxy.
move/eqP: Hxy => Hxy.
apply ps_neq in Hxy.
case: Hxy.
apply/setP.
move => v.
by rewrite -2!p_ps_eq Hp.
- move => l l'.
move/mapP => [u Hu] Hlu.
move/mapP => [u' Hu'] Hlu' Hneq.
rewrite Hlu Hlu'.
case Heq: (u == u').
move/eqP: Heq Hlu =>->.
move => Hlu.
case/eqP: Hneq.
by rewrite Hlu' Hlu.
move/eqP: Heq => Heq.
have Hp := ps_partition.
move/andP: Hp => [Hcc Hp].
move/andP: Hp => [Htr H0].
move/trivIsetP: Htr => Htr.
have Hpu: ps u \in \bigcup_(u in U) [set ps u].
apply/bigcupP.
exists u => //=.
by rewrite in_set1.
have Hpu': ps u' \in \bigcup_(u in U) [set ps u].
apply/bigcupP.
exists u' => //=.
by rewrite in_set1.
have Hneq': ps u != ps u'.
apply/negP/negP/eqP => Hpp.
contradict Hpp.
exact: ps_neq.
have Hpp := Htr _ _ Hpu Hpu' Hneq'.
rewrite disjoint_subset.
apply/subsetP.
move => x.
rewrite p_ps_eq => Hx.
rewrite inE.
apply/negP.
case => Hp.
have Hy: x \in p u' by [].
move: Hy.
rewrite p_ps_eq => Hy.
move: Hpp.
rewrite disjoint_subset.
move/subsetP => Hs.
move/Hs: Hx.
rewrite inE.
move/negP.
by case.
Qed.
Lemma seq_freshU'_uniq : uniq seq_freshU'.
Proof.
rewrite filter_uniq //.
exact: enum_uniq.
Qed.
Lemma seq_pfreshV'_uniq : uniq seq_pfreshV'.
Proof.
rewrite /seq_pfreshV'.
rewrite cat_uniq.
apply/andP.
split; last (apply/andP; split).
- apply uniq_flatten.
* move => s.
move/mapP => [u' Hu'] Hs.
rewrite Hs.
exact: p'_uniq.
* rewrite map_inj_in_uniq; first by apply seq_freshU'_uniq.
move => u u' Hu Hu' Hp.
case Huu: (u == u'); first by move/eqP: Huu.
move/eqP: Huu => Huu.
have Hpsn := ps'_neq Huu.
case: Hpsn.
apply/setP => x.
by rewrite -2!p'_ps'_eq Hp.
* move => vs vs'.
move/mapP => [u Hu] Hup.
move/mapP => [u' Hu'] Hu'p.
move/eqP => Hv.
have Hp := ps'_partition.
move/andP: Hp => [Hcc Hp].
move/andP: Hp => [Htr H0].
move/trivIsetP: Htr => Htr.
have Hpu: ps' u \in \bigcup_(u in U') [set ps' u].
apply/bigcupP.
exists u => //=.
by rewrite in_set1.
have Hpu': ps' u' \in \bigcup_(u in U') [set ps' u].
apply/bigcupP.
exists u' => //=.
by rewrite in_set1.
have Hneq': ps' u != ps' u'.
apply/negP/negP/eqP => Hpp.
contradict Hpp.
apply: ps'_neq.
move => Huu.
case: Hv.
by rewrite Hup Hu'p Huu.
have Hpp := Htr _ _ Hpu Hpu' Hneq'.
rewrite Hup Hu'p.
rewrite disjoint_subset.
apply/subsetP.
move => x.
rewrite p'_ps'_eq => Hx.
rewrite inE.
apply/negP.
case => Hp.
have Hy: x \in p' u' by [].
move: Hy.
rewrite p'_ps'_eq => Hy.
move: Hpp.
rewrite disjoint_subset.
move/subsetP => Hs.
move/Hs: Hx.
rewrite inE.
move/negP.
by case.
- apply/hasP => Hx.
move: Hx => [x Hx] Hxx.
move/flattenP: Hxx => [vs Hvs] Hxx.
move/flattenP: Hx => [vs' Hvs'] Hxx'.
move/mapP: Hvs => [u Hu] Hus.
move/mapP: Hvs' => [u' Hu'] Hus'.
move: Hxx Hxx'.
rewrite Hus Hus'.
move: Hu.
rewrite -seq_freshU'_eq inE => Hp Hx Hx'.
have Hxx: x \in ps' u by rewrite -p'_ps'_eq.
have Hxx': x \in ps' (val u') by rewrite -p'_ps'_eq.
suff Hsuff: u <> val u'.
have Hpp := ps'_partition.
move/andP: Hpp => [Hcc Hpp].
move/andP: Hpp => [Htr H0].
move/trivIsetP: Htr => Htr.
have Hpu: ps' u \in \bigcup_(u0 in U') [set ps' u0].
apply/bigcupP.
by exists u => //; last by rewrite inE.
have Hpu': ps' (val u') \in \bigcup_(u0 in U') [set ps' u0].
apply/bigcupP.
by exists (val u') => //; last by rewrite inE.
have Hneq': ps' u != ps' (val u').
apply/negP/negP/eqP => Hpp.
contradict Hpp.
exact: ps'_neq.
have Hpp := Htr _ _ Hpu Hpu' Hneq'.
move: Hpp.
rewrite disjoint_subset.
move/subsetP => Hpp.
have Hpx := Hpp x Hxx.
move: Hpx.
rewrite inE.
by case/negP.
move => Hu.
case/negP: Hp.
rewrite Hu.
by apply/valP.
- apply uniq_flatten.
* move => vs.
move/mapP => [x Hx] Hv.
rewrite Hv.
exact: p'_uniq.
* rewrite map_inj_in_uniq; first by apply seq_modifiedU_uniq.
move => u u' Hu Hu' Hp.
case Huu: (u == u'); first by move/eqP: Huu.
move/eqP: Huu => Huu.
have Hpsn := ps_neq Huu.
have Huu': val u <> val u' by move => Hv; apply val_inj in Hv.
have Hps'n := ps'_neq Huu'.
case: Hps'n.
apply/setP => x.
by rewrite -2!p'_ps'_eq Hp.
* move => vs vs'.
move/mapP => [u Hu] Hup.
move/mapP => [u' Hu'] Hu'p.
move/eqP => Hv.
have Hp := ps'_partition.
move/andP: Hp => [Hcc Hp].
move/andP: Hp => [Htr H0].
move/trivIsetP: Htr => Htr.
have Hpu: ps' (val u) \in \bigcup_(u0 in U') [set ps' u0].
apply/bigcupP.
exists (val u) => //=.
by rewrite in_set1.
have Hpu': ps' (val u') \in \bigcup_(u0 in U') [set ps' u0].
apply/bigcupP.
exists (val u') => //=.
by rewrite in_set1.
have Hneq': ps' (val u) != ps' (val u').
apply/negP/negP/eqP => Hpp.
contradict Hpp.
apply: ps'_neq.
move => Huu.
case: Hv.
by rewrite Hup Hu'p Huu.
have Hpp := Htr _ _ Hpu Hpu' Hneq'.
rewrite Hup Hu'p.
rewrite disjoint_subset.
apply/subsetP.
move => x.
rewrite p'_ps'_eq => Hx.
rewrite inE.
apply/negP.
case => Hp.
have Hy: x \in p' (val u') by [].
move: Hy.
rewrite p'_ps'_eq => Hy.
move: Hpp.
rewrite disjoint_subset.
move/subsetP => Hs.
move/Hs: Hx.
rewrite inE.
move/negP.
by case.
Qed.
Lemma seq_freshV'_sub_uniq : uniq seq_freshV'_sub.
Proof.
rewrite filter_uniq //.
exact: seq_pfreshV'_uniq.
Qed.
Lemma seq_modifiedV_sub_uniq : uniq seq_modifiedV_sub.
Proof.
rewrite filter_uniq //.
exact: seq_pmodified_V_uniq.
Qed.
Lemma seq_impactedV_sub_uniq : uniq seq_impactedV_sub.
Proof.
apply/clos_bot_uniq.
exact: seq_modifiedV_sub_uniq.
Qed.
Lemma seq_impactedVV'_sub_uniq : uniq seq_impactedVV'_sub.
Proof.
rewrite map_inj_in_uniq; first by apply seq_impactedV_sub_uniq.
move => x y Hx Hy.
by move/val_inj.
Qed.
Lemma seq_freshV'_uniq : uniq seq_freshV'.
Proof.
rewrite filter_uniq //.
exact: enum_uniq.
Qed.
Lemma seq_impacted_fresh_sub_uniq : uniq seq_impacted_fresh_sub.
Proof.
rewrite cat_uniq.
apply/andP; split.
- rewrite map_inj_uniq; last by apply val_inj.
apply clos_bot_uniq.
by apply seq_modifiedV_sub_uniq.
- apply/andP; split; last by rewrite filter_uniq // enum_uniq.
apply/negP.
case.
move/hasP.
move => /= [x Hx] Hm.
move: Hx Hm.
rewrite -seq_freshV'_eq.
rewrite -seq_impactedVV'_sub_eq impactedVV'_sub_eq // => Hx Hm.
move/negP: Hx; case; apply/negP.
move: Hm.
by apply impactedVV'_freshV'.
Qed.
Lemma seq_impacted_fresh_sub_pt_uniq : uniq seq_impacted_fresh_sub_pt.
Proof.
rewrite cat_uniq.
apply/andP; split.
- rewrite map_inj_uniq; last by apply val_inj.
apply clos_bot_uniq.
by apply seq_modifiedV_sub_uniq.
- apply/andP; split; last by apply seq_freshV'_sub_uniq.
apply/negP.
case.
move/hasP.
move => /= [x Hx] Hm.
move: Hx Hm.
rewrite -seq_freshV'_sub_eq.
erewrite freshV'_sub_eq; eauto.
rewrite -seq_impactedVV'_sub_eq impactedVV'_sub_eq // => Hx Hm.
move/negP: Hx; case; apply/negP.
move: Hm.
by apply impactedVV'_freshV'.
Qed.
Lemma seq_checkable_impacted_fresh_sub_uniq : uniq seq_checkable_impacted_fresh_sub.
Proof.
rewrite filter_uniq //.
exact: seq_impacted_fresh_sub_uniq.
Qed.
Lemma seq_checkable_impacted_fresh_sub_pt_uniq : uniq seq_checkable_impacted_fresh_sub_pt.
Proof.
rewrite filter_uniq //.
exact: seq_impacted_fresh_sub_pt_uniq.
Qed.
End CheckedSeqHierarchical.
Require Import all_ssreflect.
From chip
Require Import extra connect closure check check_seq change hierarchical hierarchical_sub hierarchical_sub_pt hierarchical_sub_correct hierarchical_sub_pt_correct tarjan_acyclic.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section CheckedSeqHierarchical.
Variable (A_top : eqType) (A_bot : eqType).
Variable (U' : finType) (V' : finType).
Variable (f'_top : U' -> A_top) (f'_bot : V' -> A_bot).
Variable (P_top : pred U') (P_bot : pred V').
Local Notation U := (sig_finType P_top).
Local Notation V := (sig_finType P_bot).
Variable (f_top : U -> A_top) (f_bot : V -> A_bot).
Variable g_top_rev : U -> seq U.
Variable g_bot_rev : V -> seq V.
Variable p : U -> seq V.
Variable p' : U' -> seq V'.
Variable (checkable'_bot : pred V').
Variable clos_top : (U -> seq U) -> seq U -> seq U.
Hypothesis clos_topP : forall successors (s : seq U) (x : U),
reflect
(exists2 v, v \in s & connect (grel successors) v x)
(x \in clos_top successors s).
Variable clos_bot : (V -> seq V) -> seq V -> seq V.
Hypothesis clos_botP : forall successors (s : seq V) (x : V),
reflect
(exists2 v, v \in s & connect (grel successors) v x)
(x \in clos_bot successors s).
(* defs *)
Definition seq_modifiedU := [seq u <- enum U | f_top u != f'_top (val u)].
Definition seq_impactedU := clos_top g_top_rev seq_modifiedU.
Definition seq_freshU' := [seq u <- enum U' | ~~ P_top u].
Definition seq_pmodified_V := flatten [seq (p u) | u <- seq_modifiedU].
Definition seq_pimpacted_V := flatten [seq (p u) | u <- seq_impactedU].
Definition seq_pfreshV' :=
flatten [seq (p' u) | u <- seq_freshU'] ++ flatten [seq (p' (val u)) | u <- seq_modifiedU].
Definition P_V_seq_sub v := v \in seq_pimpacted_V.
Definition g_bot_rev_sub (v : V) := [seq v <- g_bot_rev v | P_V_seq_sub v].
Definition seq_modifiedV_sub := [seq v <- seq_pmodified_V | f_bot v != f'_bot (val v)].
Definition seq_impactedV_sub := clos_bot g_bot_rev_sub seq_modifiedV_sub.
Definition seq_impactedVV'_sub := [seq val v | v <- seq_impactedV_sub].
Definition seq_freshV' := [seq v <- enum V' | ~~ P_bot v].
Definition seq_freshV'_sub := [seq v <- seq_pfreshV' | ~~ P_bot v].
Definition seq_impacted_fresh_sub := seq_impactedVV'_sub ++ seq_freshV'.
Definition seq_checkable_impacted_fresh_sub :=
[seq v <- seq_impacted_fresh_sub | checkable'_bot v].
Definition seq_impacted_fresh_sub_pt := seq_impactedVV'_sub ++ seq_freshV'_sub.
Definition seq_checkable_impacted_fresh_sub_pt :=
[seq v <- seq_impacted_fresh_sub_pt | checkable'_bot v].
(* proofs *)
Variable g_top : rel U.
Hypothesis g_top_grev : [rel x y | g_top y x] =2 grel g_top_rev.
Lemma seq_modifiedU_eq :
modifiedV f'_top f_top =i seq_modifiedU.
Proof.
by move => x; rewrite inE mem_filter mem_enum andb_idr.
Qed.
Lemma seq_impactedU_eq :
impacted g_top^-1 (modifiedV f'_top f_top) =i seq_impactedU.
Proof.
move => x.
apply/impactedVP.
case: ifP.
- move/clos_topP => [v Hv] Hc.
move: Hv.
rewrite -seq_modifiedU_eq => Hv.
exists v => //.
move/connectP: Hc => [p0 Hp] Hl.
apply/connectP.
exists p0 => //.
elim: p0 v Hp {Hv Hl} => //.
move => v p0 IH v0.
rewrite /=.
move/andP => [Hv Hp].
apply/andP.
split; last by apply: IH.
move: Hv.
have Hb := (g_top_grev v0 v).
rewrite /= in Hb.
by rewrite Hb.
- move/negP => Hs.
move => [y Hy] Hc.
case: Hs.
apply/clos_topP.
move: Hy.
rewrite seq_modifiedU_eq => Hy.
exists y => //.
move/connectP: Hc => [p0 Hp0] Hl.
apply/connectP.
exists p0 => //.
elim: p0 y Hp0 {Hl Hy} => //.
move => v p0 IH v0.
rewrite /=.
move/andP => [Hv Hp].
apply/andP.
split; last by apply: IH.
move: Hv.
have Hb := (g_top_grev v0 v).
rewrite /= in Hb.
by rewrite Hb.
Qed.
Lemma seq_freshU'_eq :
freshV' P_top =i seq_freshU'.
Proof.
by move => x; rewrite inE mem_filter mem_enum andb_idr.
Qed.
Variables (ps : U -> {set V}).
Hypothesis p_ps_eq : forall u : U, p u =i ps u.
Hypothesis ps_partition : partition (\bigcup_( u | u \in U ) [set ps u]) [set: V].
Lemma seq_pimpacted_V_eq :
pimpacted_sub_V f'_top g_top f_top ps =i seq_pimpacted_V.
Proof.
move => x.
apply/bigcupP.
case: ifP => Hm.
- move/flattenP: Hm => [us Hus] Hx.
move/mapP: Hus => [y Hy] Hyu.
exists y; last by rewrite -p_ps_eq -Hyu.
by rewrite seq_impactedU_eq.
- move/negP: Hm => Hm [u Hu] Hx.
case: Hm.
apply/flattenP.
exists (p u); last by rewrite p_ps_eq.
apply/mapP.
exists u => //.
by rewrite -seq_impactedU_eq.
Qed.
Lemma P_V_sub_V_seq_sub_eq :
P_V_sub f'_top g_top f_top ps =i P_V_seq_sub.
Proof.
move => x.
apply/idP/idP.
- by rewrite seq_pimpacted_V_eq.
- by rewrite seq_pimpacted_V_eq.
Qed.
Variables (ps' : U' -> {set V'}).
Hypothesis p'_ps'_eq : forall u : U', p' u =i ps' u.
Hypothesis ps'_partition : partition (\bigcup_( u | u \in U' ) [set ps' u]) [set: V'].
Lemma seq_pfreshV'_eq : pfreshV' f'_top f_top ps' =i seq_pfreshV'.
Proof.
move => x.
apply/idP/idP.
- case/setUP => Hp; rewrite mem_cat; apply/orP.
* left.
apply/flattenP.
move/bigcupP: Hp => [u' Hu'] Hx.
exists (p' u').
+ apply/mapP.
exists u' => //.
by rewrite -seq_freshU'_eq.
+ by rewrite p'_ps'_eq.
* right.
apply/flattenP.
move/bigcupP: Hp => [u Hu] Hx.
exists (p' (val u)); last by rewrite p'_ps'_eq.
apply/mapP.
exists u => //.
by rewrite -seq_modifiedU_eq.
- rewrite mem_cat; case/orP; move/flattenP => [vs Hvs] Hx.
* apply/setUP.
left.
apply/bigcupP.
move/mapP: Hvs => [u Hu] Huv.
exists u; first by rewrite seq_freshU'_eq.
by rewrite -p'_ps'_eq -Huv.
* move/mapP: Hvs => [u Hu] Huv.
apply/setUP.
right.
apply/bigcupP.
exists u; first by rewrite seq_modifiedU_eq.
by rewrite -p'_ps'_eq -Huv.
Qed.
Variable g_bot : rel V.
Hypothesis g_bot_grev : [rel x y | g_bot y x] =2 grel g_bot_rev.
Hypothesis f_top_bot_ps : forall (u : U),
f_top u = f'_top (val u) -> forall (v : V), v \in ps u -> f_bot v = f'_bot (val v).
Lemma seq_modifiedV_sub_eq : forall z,
(val z \in seq_modifiedV_sub) =
(z \in modifiedV_sub f'_top f'_bot g_top f_top f_bot ps).
Proof.
move => z.
apply/idP/idP.
- rewrite mem_filter.
move/andP => [Hz Ha].
rewrite inE.
move/flattenP: Ha => [x Hx] Hzx.
apply/andP; split => //.
apply/bigcupP.
move/mapP: Hx => [u Hu] Hxu.
exists u; last by rewrite -p_ps_eq -Hxu.
by rewrite seq_modifiedU_eq.
- move => Hz.
rewrite mem_filter.
apply/andP.
move: Hz.
rewrite inE.
move/andP => [Hz Hf].
split => //.
move/bigcupP: Hz => [u Hu] Huz.
apply/flattenP.
exists (p u); last by rewrite p_ps_eq.
apply/mapP.
exists u => //.
by rewrite -seq_modifiedU_eq.
Qed.
Lemma g_bot_rev_sub_eqq : forall x y : sig_finType (P_V_sub f'_top g_top f_top ps),
((grel g_bot_rev_sub) (val x) (val y)) = (g_bot (val y) (val x)).
Proof.
move => x y.
rewrite /=.
apply/idP/idP.
- rewrite mem_filter.
move/andP.
move => [Hp Hv].
have Hb := g_bot_grev (val x) (val y).
rewrite /= in Hb.
by rewrite -Hb in Hv.
- have Hb := g_bot_grev (val x) (val y).
rewrite /= in Hb.
rewrite Hb /=.
move => Hs.
rewrite mem_filter.
rewrite Hs.
apply/andP; split => //.
rewrite /P_V_seq_sub.
rewrite -P_V_sub_V_seq_sub_eq.
have H_sp := (insubP (sig_subFinType (P_V_sub f'_top g_top f_top ps)) (val y)).
by destruct H_sp; last by case/negP: i; apply valP.
Qed.
Lemma connect_rel_sub : forall (y z : sig_finType (P_V_sub f'_top g_top f_top ps)),
connect [rel x0 y0 | g_bot (val x0) (val y0)] y z ->
connect (grel g_bot_rev_sub) (val z) (val y).
Proof.
move => y z.
move/connectP => [pt Hpt] Hz.
apply connect_rev.
apply/connectP.
exists (map val pt); last by rewrite last_map Hz.
clear Hz.
elim: pt y Hpt => //.
move => a pt IH y.
rewrite /=.
move/andP => [Hg Hp].
apply/andP.
split; last by apply: IH.
by rewrite -g_bot_rev_sub_eqq in Hg.
Qed.
Lemma connect_g_bot_rev_sub_g_bot_rev : forall v y,
connect (grel g_bot_rev_sub) v y ->
connect g_bot^-1 v y.
Proof.
move => v y.
move/connectP => [pt Hpt] Hl.
apply/connectP.
exists pt => //.
elim: pt v Hpt {Hl} => //.
move => z pt IH v.
rewrite /=.
move/andP => [Hz Hp].
apply/andP.
rewrite mem_filter in Hz.
move/andP: Hz => [Hzp Hgb].
have Hg := g_bot_grev v z.
rewrite /= in Hg.
rewrite -Hg in Hgb.
split => //.
by apply: IH.
Qed.
Hypothesis g_bot_top_ps : forall (v v' : V) (u u' : U),
u <> u' -> g_bot v v' -> v \in ps u -> v' \in ps u' -> g_top u u'.
(* ps is injective *)
Hypothesis ps_neq : forall (u u' : U), u <> u' -> ps u <> ps u'.
Hypothesis ps'_neq : forall (u u' : U'), u <> u' -> ps' u <> ps' u'.
Hypothesis f_top_partition : forall (u : U),
f_top u = f'_top (val u) -> [set val v | v in ps u] = ps' (val u).
Lemma seq_impactedVV'_sub_eq :
impactedVV'_sub f'_top f'_bot g_top g_bot f_top f_bot ps =i seq_impactedVV'_sub.
Proof.
move => x.
apply/idP/idP.
- move/imsetP => [y Hy] Hyx.
apply/mapP.
exists (val y) => //.
move/impactedP: Hy => [z Hz] Hyz.
apply/clos_botP.
exists (val z); first by rewrite seq_modifiedV_sub_eq.
move: Hyz.
move/connect_rev => /=.
by apply connect_rel_sub.
- move/mapP => [y Hy] Hyx.
move/clos_botP: Hy => [v Hv] Hc.
apply/imsetP.
have H_sp := (insubP (sig_subFinType (P_V_sub f'_top g_top f_top ps)) v).
destruct H_sp; last first.
case/negP: i.
rewrite /P_V_sub.
move: Hv.
rewrite mem_filter.
move/andP => [Hf Hs].
have Hv: v \in modifiedV f'_bot f_bot by rewrite inE.
suff Hsuff: v \in pmodified_sub_V f'_top f_top ps.
move/bigcupP: Hsuff => [u Hu] Huv.
apply/bigcupP.
exists u => //.
apply/impactedP.
by exists u.
move: Hv.
by apply modifiedV_pmodified_sub_V.
rewrite -e in Hv.
rewrite seq_modifiedV_sub_eq in Hv.
apply connect_g_bot_rev_sub_g_bot_rev in Hc.
rewrite inE in Hv.
move/andP: Hv => [Hvp Hfb].
rewrite e in Hfb.
have Hyi: y \in impacted g_bot^-1 (modifiedV f'_bot f_bot).
apply/impactedP.
exists v => //.
by rewrite inE.
have H_sp := (insubP (sig_subFinType (P_V_sub f'_top g_top f_top ps)) y).
destruct H_sp.
rewrite -e0 in Hyi.
apply impactedV_impactedV_sub_eq in Hyi => //.
by exists u0; last by rewrite e0.
case/negP: i0.
rewrite /P_V_sub.
rewrite /pimpacted_sub_V /pimpacted_V.
apply/bigcupP.
have Hp := ps_partition.
move/andP: Hp => [Hcc Hp].
move/andP: Hp => [Htr H0].
move: Hcc.
rewrite /cover.
move/eqP => Hcc.
have Hyy: y \in \bigcup_(B in \bigcup_(u in U) [set ps u]) B by rewrite Hcc inE.
move/bigcupP: Hyy => [ys Hyy] Hys.
move/bigcupP: Hyy => [u0 Hu0] Huys.
exists u0; last by move: Huys; rewrite inE; move/eqP =><-.
rewrite inE in Huys.
move/eqP: Huys => Huys.
rewrite Huys in Hys.
apply/impactedP.
have Hvv: v \in \bigcup_(B in \bigcup_(u in U) [set ps u]) B by rewrite Hcc inE.
move/bigcupP: Hvv => [vs Hvv] Hvs.
move/bigcupP: Hvv => [u1 Hu1] Huvs.
rewrite inE in Huvs.
move/eqP: Huvs => Huvs.
rewrite Huvs in Hvs.
exists u1.
- rewrite inE.
apply/eqP => Hf.
case/negP: Hfb.
apply/eqP.
by have f_topb := f_top_bot_ps Hf Hvs.
- move: Hys Hvs Hc.
by apply connect_rev_v_u.
Qed.
Lemma seq_freshV'_sub_eq :
freshV'_sub f'_top P_bot f_top ps' =i seq_freshV'_sub.
Proof.
by move => x; apply/idP/idP; rewrite inE mem_filter -seq_pfreshV'_eq andbC.
Qed.
Lemma seq_impacted_fresh_sub_eq :
impactedV'_sub f'_top f'_bot g_top g_bot f_top f_bot ps =i seq_impacted_fresh_sub.
Proof.
move => x.
apply/idP/idP.
- rewrite mem_cat.
case/setUP => Hx.
* apply/orP; left.
by rewrite -seq_impactedVV'_sub_eq.
* apply/orP; right.
by rewrite -seq_freshV'_eq.
- rewrite mem_cat.
move/orP; case => Hx.
* apply/setUP.
left.
by rewrite seq_impactedVV'_sub_eq.
* apply/setUP.
right.
by rewrite seq_freshV'_eq.
Qed.
Lemma seq_impacted_fresh_sub_pt_eq :
impactedV'_sub_pt f'_top f'_bot g_top g_bot f_top f_bot ps ps' =i
seq_impacted_fresh_sub_pt.
Proof.
move => x.
apply/idP/idP.
- case/setUP => Hx.
* rewrite mem_cat.
apply/orP.
left.
by rewrite -seq_impactedVV'_sub_eq.
* rewrite mem_cat.
apply/orP.
right.
by rewrite -seq_freshV'_sub_eq.
- rewrite mem_cat.
case/orP => Hx.
* apply/setUP.
left.
by rewrite seq_impactedVV'_sub_eq.
* apply/setUP.
right.
by rewrite seq_freshV'_sub_eq.
Qed.
Lemma seq_impacted_fresh_sub_correct :
seq_impacted_fresh_sub =i impactedV' f'_bot f_bot g_bot.
Proof.
move => x.
apply/idP/idP.
- rewrite -seq_impacted_fresh_sub_eq.
by rewrite impactedV'_sub_eq //.
- rewrite -seq_impacted_fresh_sub_eq.
by rewrite impactedV'_sub_eq //.
Qed.
Lemma seq_impacted_fresh_sub_pt_correct :
seq_impacted_fresh_sub_pt =i impactedV' f'_bot f_bot g_bot.
Proof.
move => x.
apply/idP/idP.
- rewrite -seq_impacted_fresh_sub_pt_eq.
by rewrite impactedV'_sub_pt_eq //.
- rewrite -seq_impacted_fresh_sub_pt_eq.
by rewrite impactedV'_sub_pt_eq //.
Qed.
Lemma seq_checkable_impacted_fresh_sub_correct :
seq_checkable_impacted_fresh_sub =i
checkable_impactedV' f'_bot f_bot g_bot checkable'_bot.
Proof.
move => x.
rewrite mem_filter.
apply/idP/idP.
- move/andP => [Hc Hx].
rewrite inE.
apply/andP; split => //.
by rewrite -seq_impacted_fresh_sub_correct.
- rewrite inE.
move/andP => [Hc Hi].
apply/andP.
split => //.
by rewrite seq_impacted_fresh_sub_correct.
Qed.
Lemma seq_checkable_impacted_fresh_sub_pt_correct :
seq_checkable_impacted_fresh_sub_pt =i
checkable_impactedV' f'_bot f_bot g_bot checkable'_bot.
Proof.
move => x.
rewrite mem_filter.
apply/idP/idP.
- move/andP => [Hc Hx].
rewrite inE.
apply/andP; split => //.
by rewrite -seq_impacted_fresh_sub_pt_correct.
- rewrite inE.
move/andP => [Hc Hi].
apply/andP.
split => //.
by rewrite seq_impacted_fresh_sub_pt_correct.
Qed.
Hypothesis clos_top_uniq : forall successors (s : seq U),
uniq s -> uniq (clos_top successors s).
Hypothesis clos_bot_uniq : forall successors (s : seq V),
uniq s -> uniq (clos_bot successors s).
Hypothesis p_uniq : forall u, uniq (p u).
Hypothesis p'_uniq : forall u, uniq (p' u).
Lemma seq_modifiedU_uniq : uniq seq_modifiedU.
Proof.
exact: seq_modifiedV_uniq.
Qed.
Lemma seq_impactedU_uniq : uniq seq_impactedU.
Proof.
by apply/clos_top_uniq/seq_modifiedU_uniq.
Qed.
Lemma seq_pmodified_V_uniq : uniq seq_pmodified_V.
Proof.
apply uniq_flatten.
- elim => //.
move => v l IH.
move/mapP => [u Hu] Hp.
rewrite Hp.
exact: p_uniq.
- rewrite map_inj_in_uniq; first by apply seq_modifiedU_uniq.
move => x y Hx Hy Hp.
case Hxy: (x == y); first by move/eqP: Hxy.
move/eqP: Hxy => Hxy.
apply ps_neq in Hxy.
case: Hxy.
apply/setP.
move => v.
by rewrite -2!p_ps_eq Hp.
- move => l l'.
move/mapP => [u Hu] Hlu.
move/mapP => [u' Hu'] Hlu' Hneq.
rewrite Hlu Hlu'.
case Heq: (u == u').
move/eqP: Heq Hlu =>->.
move => Hlu.
case/eqP: Hneq.
by rewrite Hlu' Hlu.
move/eqP: Heq => Heq.
have Hp := ps_partition.
move/andP: Hp => [Hcc Hp].
move/andP: Hp => [Htr H0].
move/trivIsetP: Htr => Htr.
have Hpu: ps u \in \bigcup_(u in U) [set ps u].
apply/bigcupP.
exists u => //=.
by rewrite in_set1.
have Hpu': ps u' \in \bigcup_(u in U) [set ps u].
apply/bigcupP.
exists u' => //=.
by rewrite in_set1.
have Hneq': ps u != ps u'.
apply/negP/negP/eqP => Hpp.
contradict Hpp.
exact: ps_neq.
have Hpp := Htr _ _ Hpu Hpu' Hneq'.
rewrite disjoint_subset.
apply/subsetP.
move => x.
rewrite p_ps_eq => Hx.
rewrite inE.
apply/negP.
case => Hp.
have Hy: x \in p u' by [].
move: Hy.
rewrite p_ps_eq => Hy.
move: Hpp.
rewrite disjoint_subset.
move/subsetP => Hs.
move/Hs: Hx.
rewrite inE.
move/negP.
by case.
Qed.
Lemma seq_pimpacted_V_uniq : uniq seq_pimpacted_V.
Proof.
apply uniq_flatten.
- elim => //.
move => v l IH.
move/mapP => [u Hu] Hp.
rewrite Hp.
exact: p_uniq.
- rewrite map_inj_in_uniq; first by apply seq_impactedU_uniq.
move => x y Hx Hy Hp.
case Hxy: (x == y); first by move/eqP: Hxy.
move/eqP: Hxy => Hxy.
apply ps_neq in Hxy.
case: Hxy.
apply/setP.
move => v.
by rewrite -2!p_ps_eq Hp.
- move => l l'.
move/mapP => [u Hu] Hlu.
move/mapP => [u' Hu'] Hlu' Hneq.
rewrite Hlu Hlu'.
case Heq: (u == u').
move/eqP: Heq Hlu =>->.
move => Hlu.
case/eqP: Hneq.
by rewrite Hlu' Hlu.
move/eqP: Heq => Heq.
have Hp := ps_partition.
move/andP: Hp => [Hcc Hp].
move/andP: Hp => [Htr H0].
move/trivIsetP: Htr => Htr.
have Hpu: ps u \in \bigcup_(u in U) [set ps u].
apply/bigcupP.
exists u => //=.
by rewrite in_set1.
have Hpu': ps u' \in \bigcup_(u in U) [set ps u].
apply/bigcupP.
exists u' => //=.
by rewrite in_set1.
have Hneq': ps u != ps u'.
apply/negP/negP/eqP => Hpp.
contradict Hpp.
exact: ps_neq.
have Hpp := Htr _ _ Hpu Hpu' Hneq'.
rewrite disjoint_subset.
apply/subsetP.
move => x.
rewrite p_ps_eq => Hx.
rewrite inE.
apply/negP.
case => Hp.
have Hy: x \in p u' by [].
move: Hy.
rewrite p_ps_eq => Hy.
move: Hpp.
rewrite disjoint_subset.
move/subsetP => Hs.
move/Hs: Hx.
rewrite inE.
move/negP.
by case.
Qed.
Lemma seq_freshU'_uniq : uniq seq_freshU'.
Proof.
rewrite filter_uniq //.
exact: enum_uniq.
Qed.
Lemma seq_pfreshV'_uniq : uniq seq_pfreshV'.
Proof.
rewrite /seq_pfreshV'.
rewrite cat_uniq.
apply/andP.
split; last (apply/andP; split).
- apply uniq_flatten.
* move => s.
move/mapP => [u' Hu'] Hs.
rewrite Hs.
exact: p'_uniq.
* rewrite map_inj_in_uniq; first by apply seq_freshU'_uniq.
move => u u' Hu Hu' Hp.
case Huu: (u == u'); first by move/eqP: Huu.
move/eqP: Huu => Huu.
have Hpsn := ps'_neq Huu.
case: Hpsn.
apply/setP => x.
by rewrite -2!p'_ps'_eq Hp.
* move => vs vs'.
move/mapP => [u Hu] Hup.
move/mapP => [u' Hu'] Hu'p.
move/eqP => Hv.
have Hp := ps'_partition.
move/andP: Hp => [Hcc Hp].
move/andP: Hp => [Htr H0].
move/trivIsetP: Htr => Htr.
have Hpu: ps' u \in \bigcup_(u in U') [set ps' u].
apply/bigcupP.
exists u => //=.
by rewrite in_set1.
have Hpu': ps' u' \in \bigcup_(u in U') [set ps' u].
apply/bigcupP.
exists u' => //=.
by rewrite in_set1.
have Hneq': ps' u != ps' u'.
apply/negP/negP/eqP => Hpp.
contradict Hpp.
apply: ps'_neq.
move => Huu.
case: Hv.
by rewrite Hup Hu'p Huu.
have Hpp := Htr _ _ Hpu Hpu' Hneq'.
rewrite Hup Hu'p.
rewrite disjoint_subset.
apply/subsetP.
move => x.
rewrite p'_ps'_eq => Hx.
rewrite inE.
apply/negP.
case => Hp.
have Hy: x \in p' u' by [].
move: Hy.
rewrite p'_ps'_eq => Hy.
move: Hpp.
rewrite disjoint_subset.
move/subsetP => Hs.
move/Hs: Hx.
rewrite inE.
move/negP.
by case.
- apply/hasP => Hx.
move: Hx => [x Hx] Hxx.
move/flattenP: Hxx => [vs Hvs] Hxx.
move/flattenP: Hx => [vs' Hvs'] Hxx'.
move/mapP: Hvs => [u Hu] Hus.
move/mapP: Hvs' => [u' Hu'] Hus'.
move: Hxx Hxx'.
rewrite Hus Hus'.
move: Hu.
rewrite -seq_freshU'_eq inE => Hp Hx Hx'.
have Hxx: x \in ps' u by rewrite -p'_ps'_eq.
have Hxx': x \in ps' (val u') by rewrite -p'_ps'_eq.
suff Hsuff: u <> val u'.
have Hpp := ps'_partition.
move/andP: Hpp => [Hcc Hpp].
move/andP: Hpp => [Htr H0].
move/trivIsetP: Htr => Htr.
have Hpu: ps' u \in \bigcup_(u0 in U') [set ps' u0].
apply/bigcupP.
by exists u => //; last by rewrite inE.
have Hpu': ps' (val u') \in \bigcup_(u0 in U') [set ps' u0].
apply/bigcupP.
by exists (val u') => //; last by rewrite inE.
have Hneq': ps' u != ps' (val u').
apply/negP/negP/eqP => Hpp.
contradict Hpp.
exact: ps'_neq.
have Hpp := Htr _ _ Hpu Hpu' Hneq'.
move: Hpp.
rewrite disjoint_subset.
move/subsetP => Hpp.
have Hpx := Hpp x Hxx.
move: Hpx.
rewrite inE.
by case/negP.
move => Hu.
case/negP: Hp.
rewrite Hu.
by apply/valP.
- apply uniq_flatten.
* move => vs.
move/mapP => [x Hx] Hv.
rewrite Hv.
exact: p'_uniq.
* rewrite map_inj_in_uniq; first by apply seq_modifiedU_uniq.
move => u u' Hu Hu' Hp.
case Huu: (u == u'); first by move/eqP: Huu.
move/eqP: Huu => Huu.
have Hpsn := ps_neq Huu.
have Huu': val u <> val u' by move => Hv; apply val_inj in Hv.
have Hps'n := ps'_neq Huu'.
case: Hps'n.
apply/setP => x.
by rewrite -2!p'_ps'_eq Hp.
* move => vs vs'.
move/mapP => [u Hu] Hup.
move/mapP => [u' Hu'] Hu'p.
move/eqP => Hv.
have Hp := ps'_partition.
move/andP: Hp => [Hcc Hp].
move/andP: Hp => [Htr H0].
move/trivIsetP: Htr => Htr.
have Hpu: ps' (val u) \in \bigcup_(u0 in U') [set ps' u0].
apply/bigcupP.
exists (val u) => //=.
by rewrite in_set1.
have Hpu': ps' (val u') \in \bigcup_(u0 in U') [set ps' u0].
apply/bigcupP.
exists (val u') => //=.
by rewrite in_set1.
have Hneq': ps' (val u) != ps' (val u').
apply/negP/negP/eqP => Hpp.
contradict Hpp.
apply: ps'_neq.
move => Huu.
case: Hv.
by rewrite Hup Hu'p Huu.
have Hpp := Htr _ _ Hpu Hpu' Hneq'.
rewrite Hup Hu'p.
rewrite disjoint_subset.
apply/subsetP.
move => x.
rewrite p'_ps'_eq => Hx.
rewrite inE.
apply/negP.
case => Hp.
have Hy: x \in p' (val u') by [].
move: Hy.
rewrite p'_ps'_eq => Hy.
move: Hpp.
rewrite disjoint_subset.
move/subsetP => Hs.
move/Hs: Hx.
rewrite inE.
move/negP.
by case.
Qed.
Lemma seq_freshV'_sub_uniq : uniq seq_freshV'_sub.
Proof.
rewrite filter_uniq //.
exact: seq_pfreshV'_uniq.
Qed.
Lemma seq_modifiedV_sub_uniq : uniq seq_modifiedV_sub.
Proof.
rewrite filter_uniq //.
exact: seq_pmodified_V_uniq.
Qed.
Lemma seq_impactedV_sub_uniq : uniq seq_impactedV_sub.
Proof.
apply/clos_bot_uniq.
exact: seq_modifiedV_sub_uniq.
Qed.
Lemma seq_impactedVV'_sub_uniq : uniq seq_impactedVV'_sub.
Proof.
rewrite map_inj_in_uniq; first by apply seq_impactedV_sub_uniq.
move => x y Hx Hy.
by move/val_inj.
Qed.
Lemma seq_freshV'_uniq : uniq seq_freshV'.
Proof.
rewrite filter_uniq //.
exact: enum_uniq.
Qed.
Lemma seq_impacted_fresh_sub_uniq : uniq seq_impacted_fresh_sub.
Proof.
rewrite cat_uniq.
apply/andP; split.
- rewrite map_inj_uniq; last by apply val_inj.
apply clos_bot_uniq.
by apply seq_modifiedV_sub_uniq.
- apply/andP; split; last by rewrite filter_uniq // enum_uniq.
apply/negP.
case.
move/hasP.
move => /= [x Hx] Hm.
move: Hx Hm.
rewrite -seq_freshV'_eq.
rewrite -seq_impactedVV'_sub_eq impactedVV'_sub_eq // => Hx Hm.
move/negP: Hx; case; apply/negP.
move: Hm.
by apply impactedVV'_freshV'.
Qed.
Lemma seq_impacted_fresh_sub_pt_uniq : uniq seq_impacted_fresh_sub_pt.
Proof.
rewrite cat_uniq.
apply/andP; split.
- rewrite map_inj_uniq; last by apply val_inj.
apply clos_bot_uniq.
by apply seq_modifiedV_sub_uniq.
- apply/andP; split; last by apply seq_freshV'_sub_uniq.
apply/negP.
case.
move/hasP.
move => /= [x Hx] Hm.
move: Hx Hm.
rewrite -seq_freshV'_sub_eq.
erewrite freshV'_sub_eq; eauto.
rewrite -seq_impactedVV'_sub_eq impactedVV'_sub_eq // => Hx Hm.
move/negP: Hx; case; apply/negP.
move: Hm.
by apply impactedVV'_freshV'.
Qed.
Lemma seq_checkable_impacted_fresh_sub_uniq : uniq seq_checkable_impacted_fresh_sub.
Proof.
rewrite filter_uniq //.
exact: seq_impacted_fresh_sub_uniq.
Qed.
Lemma seq_checkable_impacted_fresh_sub_pt_uniq : uniq seq_checkable_impacted_fresh_sub_pt.
Proof.
rewrite filter_uniq //.
exact: seq_impacted_fresh_sub_pt_uniq.
Qed.
End CheckedSeqHierarchical.