Library reach
This file formlises the proof described in Section 4 of the Paper.
Require Import ssreflect.
Require Import ssrbool.
Require Import ssrfun.
Require Import eqtype.
Require Import seq.
Require Import fintype.
Require Import ssrnat.
Require Import eqrel.
Require Import finfun.
Require Import boollogic.
Require Import fingroup.
Require Import graphs.
Require Import general.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Section JAG.
Finite set of states
Parameter Q:finType.
Finite set of pebbles
Parameter P:finType.
Two pebbles to be placed on the start and end nodes
Parameters sP tP: P.
Inductive move:Type :=
| m_edge: P -> nat -> move
| m_jump: P -> P -> move.
Definition move_eqd (m1 m2: move): bool :=
match (m1, m2) with
| (m_edge z1 n1, m_edge z2 n2) => (z1 == z2) && (n1 == n2)
| (m_jump z1 z'1, m_jump z2 z'2) => (z1 == z2) && (z'1 == z'2)
| _ => false
end.
Lemma move_eqPx: reflect_eq move_eqd.
Proof.
rewrite /move_eqd.
case=>[z1 n1|z1 z1']; case=>[z2 n2|z2 z2']; apply: (iffP idP)=>//;
by (case/andP; do 2 move/eqP=>[->]) || (case=>[-> ->]; rewrite !eq_refl).
Qed.
Canonical Structure moveData := EqType move_eqPx.
Definition obs := ieqrelFin P.
Record jag : Type := JAG {
jag_state: Q -> obs -> Q;
jag_move: Q -> obs -> move
}.
End JAG.
Section OperationalSemantics.
Variable J:jag.
Record state_space: Type := mkState_space {
underlying:> finType;
make_move: underlying -> move -> underlying;
observe: underlying -> obs
}.
Notation "rho @ m" := (make_move rho m) (at level 60).
Variable S:state_space.
Definition conf: finType := {Q * S :as finType}.
Definition next(C : conf):=
( jag_state J C.1 (observe C.2)
, C.2 @ (jag_move J C.1 (observe C.2))).
End OperationalSemantics.
Section Abstraction.
Variable S: state_space.
Variable J: jag.
Record abstraction : Type := mkAbst {
abstract:> finType;
init: S -> abstract;
action0: abstract -> move -> abstract;
action1: abstract -> move -> obs -> abstract;
realises: abstract -> S -> bool;
predictable: abstract -> move -> S -> bool;
init_rel: forall rho:S, realises (init rho) rho;
action01: forall (xi:abstract) (rho: S) (m:move),
(realises xi rho) ->
(predictable xi m rho) ->
(action0 xi m == action1 xi m (observe (make_move rho m)));
action1_rel: forall (xi:abstract) (rho: S) (m:move),
(realises xi rho) ->
(realises (action1 xi m (observe (make_move rho m)))
(make_move rho m));
obs_rel: forall (xi:abstract) (rho rho': S),
(realises xi rho) -> (realises xi rho') ->
((observe rho) == (observe rho'))
}.
Notation "rho ||- delta" := (realises rho delta) (at level 80).
Variable X: abstraction.
Extended configurations
Definition econfP(E : {(conf S) * X :as finType}) :=
realises E.2 (E.1.2).
Definition econf: finType := sub_finType econfP.
Definition mk_econf(C:conf S) (xi:X) (R: realises xi C.2) :=
@EqSig {(conf S) * X :as finType} econfP (C, xi) R.
Implicit Arguments mk_econf [].
Definition econf_conf(E : econf) : conf S := (val E).1.
Definition piQ(E : econf) : Q := (econf_conf E).1.
Definition piS(E : econf) : S := (econf_conf E).2.
Definition piX(E : econf) : X := (val E).2.
Lemma real_econf: forall (E:econf), realises (piX E) (piS E).
Proof. by move=>[[[q rho] xi] real]. Qed.
Definition init_econf(C : conf S) : econf :=
mk_econf C (init X C.2) (init_rel X C.2).
Lemma econf_conf_init_econf: forall C, econf_conf (init_econf C) = C.
Proof. by case=>[q rho]. Qed.
Lemma econf_observe: forall E1 E2,
(piX E1) = (piX E2) -> observe (piS E1) = observe (piS E2).
Proof.
move=>E1 E2 eq; apply/eqP; apply: (obs_rel (valP E1));
rewrite /piX in eq; rewrite (eq); apply: (valP E2).
Qed.
Definition stepn(E : econf): bool :=
negb (predictable (piX E) (jag_move J (piQ E) (observe (piS E))) (piS E)).
Definition stepe(E : econf): econf.
Proof.
move=>[[C xi] EP].
set rho:=C.2.
set q':=jag_state J C.1 (observe rho).
set m :=jag_move J C.1 (observe rho).
apply: (@mk_econf (next J C) (action1 xi m (observe (make_move rho m)))).
apply: (action1_rel m EP).
Defined.
Lemma econf_subd_eqd: forall E1 E2:econf, (E1 == E2) = (val E1 == val E2).
Proof. done. Qed.
Lemma stepe_eqd: forall E1 E2,
(E1 == E2) = (piQ E1 == piQ E2) && (piS E1 == piS E2) && (piX E1 == piX E2).
Proof.
move=>E1 E2.
rewrite (econf_subd_eqd).
case E1 =>[[[q1 rho1] xi1] EP1].
case E2 =>[[[q2 rho2] xi2] EP2].
rewrite /piQ /piS /piX /=.
apply: iffB.
by case/eqP=>[-> -> ->]; rewrite !eq_refl.
by case/andP=> [eQS eX]; case (andP eQS) => [eQ eS];
rewrite (eqP eQ) (eqP eS) (eqP eX) eq_refl.
Qed.
Lemma stepe_Q: forall E,
(piQ (stepe E)) = jag_state J (piQ E) (observe (piS E)).
Proof. by move=>E; case: E=>[[q rho] xi]/=. Qed.
Lemma stepe_S: forall E,
(piS (stepe E)) = make_move (piS E) (jag_move J (piQ E) (observe (piS E))).
Proof. by move=>E; case: E=>[[q rho] xi]/=. Qed.
Lemma stepe_X1: forall E,
(piX (stepe E)) = action1 (piX E) (jag_move J (piQ E) (observe (piS E)))
(observe (piS (stepe E))).
Proof. by move=>E; case: E=>[[q rho] xi]/=. Qed.
Lemma stepe_X0: forall E, negb (stepn E) ->
(piX (stepe E)) = action0 (piX E) (jag_move J (piQ E) (observe (piS E))).
Proof.
by rewrite /stepn; move=>E p;
rewrite stepe_X1 /piX stepe_S;
rewrite (eqP (action01 (valP E) (negbE2 p))).
Qed.
Lemma stepe_econf: forall E, (econf_conf (stepe E)) = next J (econf_conf E).
Proof. by elim =>[[q rho] xi]/=. Qed.
Definition eqdQX( E1 E2 : econf) :=
(piQ E1 == piQ E2) && (piX E1 == piX E2).
Lemma eqdQX_stepe: forall E1 E2 : econf,
negb (stepn E1) -> negb (stepn E2)
-> (eqdQX E1 E2) -> (eqdQX (stepe E1) (stepe E2)).
Proof.
move=>E1 E2 N1 N2.
rewrite /eqdQX.
rewrite !stepe_Q.
move/andP=>[e1 e2].
by rewrite !stepe_X0 // (eqP e1) (eqP e2) (econf_observe (eqP e2)) !eq_refl andbT.
Qed.
Lemma eqdQX_stepe_gen: forall E1 E2,
(eqdQX E1 E2) -> (observe (piS (stepe E1))) = (observe (piS (stepe E2)))
-> (eqdQX (stepe E1) (stepe E2)).
Proof.
move=>E1 E2.
rewrite /eqdQX !stepe_Q !stepe_X1.
move/andP=>[e1 e2]. move=>e3.
by rewrite !e3 !(eqP e1) !(eqP e2) !(econf_observe (eqP e2)) !eq_refl.
Qed.
Computation sequences for normal and extended configurations
Fixpoint evolution_seq (k : nat) (C: conf S) {struct k} : seq (conf S):=
match k with
| 0 => seq0
| k'.+1 => Adds C (evolution_seq k' (next J C))
end.
Fixpoint eevolution_seq (k : nat) (E : econf) {struct k} : seq econf:=
match k with
| 0 => seq0
| k'.+1 => Adds E (eevolution_seq k' (stepe E))
end.
Lemma size_eevolution_seq: forall k E, size (eevolution_seq k E) = k.
Proof. by elim=>//[k IH E]//=; rewrite IH. Qed.
Lemma size_evolution_seq: forall k C, size (evolution_seq k C) = k.
Proof. by elim=>//[k IH C]//=; rewrite IH. Qed.
(evolution k C) is the configuration after k steps starting from C
Fixpoint evolution (k : nat) (C: conf S) {struct k}: conf S:=
match k with
| 0 => C
| k'.+1 => (next J (evolution k' C))
end.
(eevolution k E) is the extended configuration after k
steps starting from E
Fixpoint eevolution (k : nat) (E0: econf) {struct k}: econf:=
match k with
| 0 => E0
| k'.+1 => (stepe (eevolution k' E0))
end.
Lemma eevolution_step: forall m E, eevolution m (stepe E) = eevolution (m.+1) E.
Proof. by move=>m E; elim: m =>//=[m ->]. Qed.
Lemma step_eevolution: forall m E, stepe (eevolution m E) = eevolution m (stepe E).
Proof. by move=> m E; elim m=>//=[n ->]. Qed.
Lemma evolution_sum: forall m n C, evolution m (evolution n C) = evolution (m+n) C.
Proof. by elim=>[|m IH n C]//=; rewrite -IH. Qed.
Lemma eevolution_sum: forall m n E, eevolution m (eevolution n E) = eevolution (m+n) E.
Proof. by elim=>[|m IH n E]//=; rewrite -IH. Qed.
Lemma eevolution_sub: forall k l E,
(k < l) -> eevolution k E = sub E (eevolution_seq l E) k.
Proof.
have U: forall k j E, eevolution k E = sub E (eevolution_seq (k + j.+1) E) k.
by move=>k j E; elim: k {1 3}E=>[|k IH F]//=;
rewrite step_eevolution; apply (IH (stepe F)).
move=>k l E i.
have V:(l = k + (l - k - 1).+1).
by rewrite -ltn_0sub in i; rewrite subn1 (ltn_predK i) subnK //;
rewrite ltn_0sub in i; apply: ltnW.
by rewrite V; apply: U.
Qed.
Lemma econf_conf_eevolution: forall m E,
econf_conf (eevolution m E) = evolution m (econf_conf E).
Proof.
elim=>//=[m IH E].
rewrite -IH; clear IH.
by case: (eevolution m E)=>[[[q rho] xi] real].
Qed.
Lemma evol_eevol_seq: forall m E,
evolution_seq m (econf_conf E) = maps econf_conf (eevolution_seq m E).
Proof.
by elim=>//=[m IH C]; apply/eqP; rewrite eqseq_adds;
apply/andP; split; rewrite -?IH ?stepe_econf eq_refl.
Qed.
Lemma evol_eevol_seq_init: forall m C,
evolution_seq m C = maps econf_conf (eevolution_seq m (init_econf C)).
Proof.
move=>m C.
have H: C = econf_conf (init_econf C) by done.
by rewrite {1}H evol_eevol_seq.
Qed.
Lemma evolution_sub: forall k l E,
(k < l) -> evolution k E = sub E (evolution_seq l E) k.
Proof.
move=>k l C lt.
by rewrite -{1}(econf_conf_init_econf C) -econf_conf_eevolution
evol_eevol_seq_init (sub_maps (init_econf C))
?size_eevolution_seq -?eevolution_sub.
Qed.
Definition stepn_seq (k : nat) (E : econf): seq bool_eqType:=
maps (fun E => stepn E) (eevolution_seq k E).
Lemma size_stepn_seq: forall k E, size (stepn_seq k E) = k.
Proof. by move=>k E; rewrite /stepn_seq size_maps size_eevolution_seq. Qed.
End Abstraction.
This section contains the construction of a concrete abstraction for
a uniform graph. It corresponds to Lemma 10 in the paper.
Section ExistenceAbstraction.
Variable G:graph.
Implicit Arguments unit [f].
Definition env := finFun P (vertices G).
Definition state_space_G_action (rho: env) (m:move): env := nosimpl
match m with
| m_edge p i =>
fgraph_of_fun (fun p' => if p == p' then act _ (rho p) (edge_of_nat _ i) else rho p')
| m_jump p p' =>
fgraph_of_fun (fun r => if r == p then (rho p') else (rho r))
end.
Definition state_space_G_obs (rho: env): obs.
Proof.
move=>rho.
rewrite /obs.
apply: (ieqrel_of_eqrel).
apply (Eqrel (erel:=(fun p p' => rho p == rho p'))).
by move=>*; rewrite eq_refl.
by move=>*; rewrite eq_sym.
by move=>x y z; move/eqP=>H; move/eqP=> K; apply/eqP; rewrite H K.
Defined.
Definition state_space_G: state_space :=
mkState_space state_space_G_action state_space_G_obs.
Definition of the abstraction X
Definition X: Type := P -> P -> (option (edgegroup G)).
Definition initX(rho: env): X :=
fun x y => if rho x == rho y then Some unit else None.
Definition action0X(xi: X) (m:move): X :=
fun x y =>
match m with
| m_edge z i =>
let ei := edge_of_nat G i in
match (z == x, z == y) with
| (true, true) => Some unit
| (true,false) => map_option (fun d => mul (inv ei) d) (xi x y)
| (false,true) => map_option (fun d => mul d ei) (xi x y)
| (false,false)=> xi x y
end
| m_jump z zdest =>
match (z == x, z == y) with
| (true, true) => Some unit
| (true,false) => xi zdest y
| (false,true) => xi x zdest
| (false,false)=> xi x y
end
end.
Definition update(xi : X) (x y: P) : X :=
fun u v =>
match (xi u x, xi y v) with
| (Some dux, Some dyv) => Some (mul dux dyv)
| _ => match (xi u y, xi x v) with
| (Some duy, Some dxv) => Some (mul duy dxv)
| _ => xi u v
end
end.
Definition action1X(xi: X) (m:move) (o:obs): X :=
match m with
| m_edge z i =>
match pick (fun y => (xi z y == None)
&& (erel (eqrel_of_ieqrel o) z y)) with
| Some y => update (action0X xi m) z y
| None => action0X xi m
end
| m_jump z zdest => action0X xi m
end.
Definition refl_dom(xi:X):= forall x, is_some (xi x x).
Definition sym_dom(xi:X):= forall x y, is_some (xi x y) -> is_some (xi y x).
Definition trans_dom(xi:X):=
forall x y z, is_some (xi x y) -> is_some (xi y z) -> is_some (xi x z).
Definition realises1X(xi:X) : Prop :=
(forall x, is_some (xi x x))
/\ (forall x y, is_some (xi x y) -> is_some (xi y x))
/\ (forall x y z, is_some (xi x y) -> is_some (xi y z) -> is_some (xi x z)).
Definition realises2X(xi:X) (rho:state_space_G) : Prop :=
(forall x y, rho(x) == rho(y) -> xi x y = Some unit).
Definition realises3X(xi:X) (rho:state_space_G) : Prop :=
(forall x y d, xi x y = Some d -> (rho y) = act _ (rho x) d).
Definition realisesX(xi:X) (rho:state_space_G) : Prop :=
(realises1X xi) /\ (realises2X xi rho) /\
(realises3X xi rho).
Definition predictableX(xi:X) (m:move) (rho:state_space_G) : Prop :=
if m is m_edge z n then
forall x y, (make_move rho m) x = (make_move rho m) y
-> is_some (action0X xi m x y)
else True.
Lemma predictableX_edge_cond: forall xi z n rho,
realisesX xi rho ->
(fun z' => (xi z z' == None) && (erel (eqrel_of_ieqrel (observe (make_move rho (m_edge z n)))) z z')) =1 pred0 ->
predictableX xi (m_edge z n) rho.
Proof.
move=>xi z n rho [[R [S T]] [Z A]] H.
move=>x y.
rewrite /action0X /make_move /state_space_G /state_space_G_action !fgraph_fun_eq.
case zx: (z == x).
by case zy: (z == y)=>//;
case xixy: (xi x y)=>//E;
move/andP: (H y)=>Hy;
rewrite ?(eqP zx) ?(eqP zy) ?is_some_None ?xixy ?eq_refl
/observe {1}/state_space_G {1}/state_space_G_obs eqrel_ieqrel
[make_move]lock /= -lock
/make_move /state_space_G /state_space_G_action !fgraph_fun_eq
-?(eqP zy) -?(eqP zx) ?zy !eq_refl ?E ?eq_refl in Hy;
contradiction Hy.
case zy: (z == y)=>//.
case xixy: (xi x y)=>//E.
have K: negb (is_some (xi y x))
by apply/negP=>L; case: (S y x L); rewrite xixy.
by move/andP: (H x)=>Hx;
rewrite (eqP zy) is_some_None K
/observe {1}/state_space_G {1}/state_space_G_obs eqrel_ieqrel
[make_move]lock /= -lock
/make_move /state_space_G /state_space_G_action !fgraph_fun_eq
-(eqP zy) !eq_refl zx E eq_refl in Hx;
contradiction Hx.
by move=>E; rewrite (Z x y) ?E ?eq_refl.
Qed.
Lemma is_some_update: forall xi x y u v,
is_some ((update xi x y) u v) =
is_some (xi u v) ||
((is_some (xi u x) && is_some (xi y v))
|| (is_some (xi u y) && is_some (xi x v))).
Proof.
move=>xi x y u v; rewrite /update.
by case: (xi); case: (xi); case: (xi); case: (xi)=>//=; rewrite ?orbT ?orbF.
Qed.
Lemma update_eqrel: forall xi x y,
(realises1X xi) -> (realises1X (update xi x y)).
Proof.
move=>xi x y [R [S T]].
rewrite /realises1X.
split.
move=>u. rewrite is_some_update.
by apply/orP; left; apply:R .
split.
move=>u v. rewrite !is_some_update.
move/or3P=>[H1|H2|H3].
by rewrite S.
by move/andP: H2=>[H21 H22]; rewrite (S u x)=>//; rewrite (S y v)=>//;
rewrite andbT !orbT.
by move/andP: H3=>[H31 H32]; rewrite (S u y)=>//; rewrite (S x v)=>//;
rewrite andbT !orbT.
move=>u v w. rewrite !is_some_update.
move/or3P=>[H1|H2|H3].
move/or3P=>[K1|K2|K3].
by rewrite (T u v w).
by move/andP: K2=>[K21 K22]; rewrite (T u v x)=>//; rewrite K22 andTb!orbT.
by move/andP: K3=>[K31 K32]; rewrite (T u v y)=>//; rewrite K32 andTb!orbT.
move/or3P=>[K1|K2|K3].
by move/andP: H2=>[H21 H22]; rewrite (T y v w)=>//; rewrite H21 andTb!orbT.
by move/andP: H2=>[H21 H22]; move/andP: K2=>[K21 K22]; rewrite H21 K22 andTb!orbT.
by move/andP: H2=>[H21 H22]; move/andP: K3=>[K31 K32]; rewrite (T u x w)=>//; rewrite andTb!orTb.
move/or3P=>[K1|K2|K3].
by move/andP: H3=>[H31 H32]; rewrite (T x v w)=>//; rewrite H31 andTb!orbT.
by move/andP: H3=>[H31 H32]; move/andP: K2=>[K21 K22]; rewrite (T u y w)=>//; rewrite orTb.
by move/andP: H3=>[H31 H32]; move/andP: K3=>[K31 K32]; rewrite H31 K32 andTb!orbT.
Qed.
Lemma is_some_initX: forall rho x y,
is_some ((initX rho) x y) = ( rho x == rho y).
Proof. by move=>rho x y; rewrite /initX; case: (rho x == rho y). Qed.
Lemma initX_refl_dom: forall rho, refl_dom (initX rho).
Proof. by move=>rho x; rewrite is_some_initX eq_refl. Qed.
Lemma initX_sym_dom: forall rho, sym_dom (initX rho).
Proof. by move=>rho x y; rewrite !is_some_initX eq_sym. Qed.
Lemma initX_trans_dom: forall rho, trans_dom (initX rho).
Proof. by move=>rho x y z; rewrite !is_some_initX;
move=>E F; rewrite (eqP E) (eqP F) eq_refl.
Qed.
Lemma initXreal1: forall rho, realises1X (initX rho).
Proof. move=>rho; split.
apply initX_refl_dom. split. apply initX_sym_dom. apply initX_trans_dom.
Qed.
Lemma initXreal2 : forall rho, realises2X (initX rho) rho.
Proof. by move=>rho x y E; rewrite /initX E. Qed.
Lemma initXreal3: forall rho, realises3X (initX rho) rho.
Proof.
rewrite /initX.
move=>rho x y d.
case H: (rho x == rho y)=>//.
by case=>E; rewrite -E act_unitP (eqP H).
Qed.
Lemma act0real1X: forall xi rho m, (realisesX xi rho) ->
(realises1X (action0X xi m)).
Proof.
move=>xi rho m [[R [S T]] _].
case m.
move=>z n.
split.
by move=>x; case U: (z == x); rewrite /= U.
split.
move=>x y.
by case U: (z == y); case V: (z == x); rewrite /= U V;
try (rewrite !is_some_map); try (apply S).
move=>x y u.
case U:(z == y); case V:(z == x); case W:(z == u);
rewrite /= U V W; try (rewrite !is_some_map); try (apply T).
done.
by rewrite -(eqP U) -(eqP V).
by rewrite -(eqP U) -(eqP W).
by rewrite -(eqP V) -(eqP W).
move=>z n.
split.
by move=>x; case U: (z == x); rewrite /= U.
split.
move=>x y.
by case U: (z == y); case V: (z == x); rewrite /= U V;
try (rewrite !is_some_map); try (apply S).
move=>x y u.
by case U:(z == y); case V:(z == x); case W:(z == u);
rewrite /= U V W; try (rewrite !is_some_map); try (apply T).
Qed.
Lemma act0real2X: forall xi rho m,
(realisesX xi rho) -> (predictableX xi m rho)
-> (forall x y, (make_move rho m)(x) == (make_move rho m)(y)
-> (action0X xi m) x y = Some unit).
Proof.
move=>xi rho m [[R [S T]] [Z A]].
case m.
move=>z n pred x y.
rewrite /action0X /make_move /state_space_G /state_space_G_action !fgraph_fun_eq.
case U: (z == y); case V: (z == x)=>//.
move=>E.
rewrite -(eqP U).
have F: is_some (action0X xi (m_edge z n) x z).
by apply: pred;
rewrite /action0X /make_move /state_space_G /state_space_G_action
!fgraph_fun_eq V eq_refl (eqP E).
rewrite /= V eq_refl /= is_some_map in F.
case: (xi x z) (A x z) F =>[d A' _|_ F]//=.
have B: rho z = act _ (rho x) d by apply A'.
rewrite B act_mulP eq_sym in E.
have W: (mul (inv d) (mul d (edge_of_nat G n)) = inv d).
by rewrite (eqP (act_free (eqP E))) unitrP.
rewrite mulP invlP unitlP in W.
have W': (d = inv (edge_of_nat G n)) by rewrite W inv_inv.
rewrite W' W.
by rewrite inv_inv invrP.
move=>E.
have F: is_some (action0X xi (m_edge z n) x y).
apply pred; clear pred.
rewrite /make_move /state_space_G /state_space_G_action !fgraph_fun_eq U V.
exact (eqP E).
rewrite /= U V /= is_some_map in F.
case: (xi x y) (A x y) F =>[d A' _|_ F]//=.
have B: rho y = act _ (rho x) d by apply A'.
rewrite (eqP V) B in E.
have W: (edge_of_nat G n) = d.
by exact (eqP (act_free_eq (act_free (g:=G)) (eqP E))).
by rewrite -W invlP.
by apply Z.
move=>x y pred u v.
rewrite /make_move /state_space_G /state_space_G_action !fgraph_fun_eq.
rewrite (eq_sym u x) (eq_sym v x).
case U: (x == u); case V: (x == v)=> //=; rewrite U V => //=;
apply Z.
Qed.
Lemma act0real3X: forall xi rho m,
(realisesX xi rho) ->
(forall x y d, (action0X xi m) x y = Some d
-> ((make_move rho m) y) = act _ ((make_move rho m) x) d).
Proof.
move=>xi rho m [[R [S T]] [Z A]].
case m.
move=>z n x y.
rewrite /make_move /state_space_G /state_space_G_action !fgraph_fun_eq.
case U: (z == y); case V: (z == x); rewrite /= U V//=.
by move=>d; case =>[<-]; rewrite act_mulP unitrP.
move=>d E.
elim: (xi x y) E (A x y (mul d (inv (edge_of_nat G n)))) => [e E| E F]//=.
case: E=>[<-].
rewrite -mulP invrP unitrP (eqP U).
move=>F; rewrite F. by rewrite act_mulP. done.
move=>d E.
elim: (xi x y) E (A x y (mul (edge_of_nat G n) d)) => [e E| E F]//=.
case: E=>[<-].
move=>F; rewrite F //.
rewrite mulP invrP unitlP (eqP V).
by rewrite act_mulP mulP invrP unitlP.
by rewrite mulP invrP unitlP.
move=>d E.
by apply A.
move=>x y u v.
rewrite /make_move /state_space_G /state_space_G_action !fgraph_fun_eq.
rewrite (eq_sym u x) (eq_sym v x).
case U: (x == u); case V: (x == v)=> //=; rewrite U V => //=.
by move=>d E; case: E=>[<-]; rewrite act_unitP.
by move=>*; apply A.
by move=>*; apply A.
by move=>*; apply A.
Qed.
Lemma act0_edge_rest: forall xi z n rho, (realisesX xi rho) ->
(forall x y, (negb (z == x)) -> (negb (z == y))
-> (make_move rho (m_edge z n))(x) == (make_move rho (m_edge z n))(y)
-> (action0X xi (m_edge z n)) x y = Some unit).
Proof.
move=>xi z n rho [[R [S T]] [Z A]] x y.
rewrite /action0X /make_move /state_space_G /state_space_G_action !fgraph_fun_eq.
case U: (z == y); case V: (z == x)=>//.
move=>_ _ E.
by apply: Z.
Qed.
Lemma act1real1X: forall xi rho m, (realisesX xi rho) ->
(realises1X (action1X xi m (observe (make_move rho m)))).
Proof.
move=>xi rho m real.
rewrite /action1X.
case: m=>[z n|u v].
case: pickP=>//[z' z'm|].
by apply: update_eqrel; apply (@act0real1X xi rho (m_edge z n)).
by move=>_; apply (@act0real1X xi rho).
by apply (@act0real1X xi rho).
Qed.
Lemma act1real2X: forall xi rho m, (realisesX xi rho) ->
(forall x y, (make_move rho m)(x) == (make_move rho m)(y)
-> (action1X xi m (observe (make_move rho m))) x y = Some unit).
Proof.
move=>xi rho m real.
move real_:real=>[[R [S T]] [Z A]].
case m.
move=>z n x y E.
rewrite /action1X.
case: pickP=>//[z' z'm|].
rewrite /observe {1}/state_space_G {1}/state_space_G_obs eqrel_ieqrel
[make_move]lock /= -lock in z'm.
case U:(x == z); case V: (y == z').
rewrite /action0X /make_move /state_space_G /state_space_G_action
!fgraph_fun_eq in z'm E.
rewrite /update /action0X !(eqP U) !(eqP V) !eq_refl /=.
case W:(z == z').
by rewrite unitrP.
by rewrite Z ?unitrP ?eq_refl.
rewrite /action0X /make_move /state_space_G /state_space_G_action
!fgraph_fun_eq in z'm E.
rewrite /update /action0X !(eqP U) !eq_refl /=.
case W:(z == z').
by move/andP: z'm=>[zz'N _]; case: (R z'); rewrite -{1}(eqP W) (eqP zz'N).
case Y: (z == y).
case F: (xi z' y)=>[d|]//=.
by rewrite eq_refl W (eqP Y) (A _ _ _ F) act_mulP in z'm;
move/andP: z'm=>[_ z'm];
rewrite (eqP (@act_free G _ _ (eqP z'm))) unitrP.
by move/andP: z'm=>[z'm1 z'm2]; rewrite (eqP z'm1).
case F: (xi z' y)=>[d|]//=.
by rewrite (eq_sym z x) U Y in E;
rewrite eq_refl W (eqP E) (A _ _ _ F) in z'm;
move/andP: z'm=>[_ z'm];
rewrite (eqP (@act_free G _ _ (eqP z'm))) unitrP.
move/andP: z'm=>[z'm1 z'm2]; rewrite (eqP z'm1) /=.
rewrite (eq_sym z x) U Y in E.
rewrite eq_refl W (eqP E) eq_sym in z'm2.
by case: (Z _ _ z'm2); rewrite F.
rewrite /action0X /make_move /state_space_G /state_space_G_action
!fgraph_fun_eq in z'm E.
rewrite /update /action0X !eq_refl !(eq_sym z x) U /=.
case W:(xi x z)=>[d|]//=.
case Y:(z == z')=>/=.
by rewrite (eqP Y) (eq_sym z' y) V;
rewrite (eq_sym z x) U (eqP Y) (eq_sym z' y) V -(eqP Y) (A _ _ _ W)
act_mulP eq_sym in E;
rewrite (eqP (@act_free G _ _ (eqP E))) unitrP.
by rewrite (eqP V) Y;
move/andP: z'm=>[z'm1 z'm2];
rewrite (Z z' z' (eq_refl (rho z')));
rewrite (eq_sym z x) U (eqP V) Y in E;
rewrite eq_refl Y -(eqP E) (A _ _ _ W) act_mulP in z'm2;
rewrite (eqP (@act_free G _ _ (eqP z'm2))) unitrP.
case Y:(z == z')=>/=.
by move/andP: z'm=>[z'm1 z'm2];
rewrite (eqP Y) in z'm1; case: (@R z'); rewrite (eqP z'm1).
case F: (xi x z')=>[d|]//=.
by rewrite (eqP V) Y;
move/andP: z'm=>[z'm1 z'm2]; rewrite (eqP z'm1)=>//=;
rewrite (eq_sym z x) U (eqP V) Y (A _ _ _ F) eq_sym in E;
rewrite (eqP (@act_free G _ _ (eqP E))) in F.
by rewrite (eq_sym z x) U (eqP V) Y in E; case: (Z _ _ E); rewrite F.
rewrite /update.
case W: (action0X _ _ x z)=>[d|]//.
case Y: (action0X _ _ z' y)=>[d'|]//.
set rho':= make_move rho (m_edge z n) in E z'm.
have H: (rho' z) = act _ (rho' x) d
by rewrite /rho'; apply (@act0real3X xi rho)=>//.
have K: (rho' y) = act _ (rho' z') d'
by rewrite /rho'; apply (@act0real3X xi rho)=>//.
move/andP: z'm=>[_ z'm].
rewrite (eqP z'm) in H. rewrite H act_mulP (eqP E) in K.
symmetry in K.
by rewrite (eqP (@act_free G _ _ K)).
case B: (action0X _ _ x z')=>[d'|]//.
case C: (action0X _ _ z y)=>[d''|]//.
set rho':= make_move rho (m_edge z n) in E z'm.
have H: (rho' z') = act _ (rho' x) d'
by rewrite /rho'; apply (@act0real3X xi rho)=>//.
have K: (rho' y) = act _ (rho' z) d''
by rewrite /rho'; apply (@act0real3X xi rho)=>//.
move/andP: z'm=>[_ z'm].
rewrite (eqP z'm) H act_mulP (eqP E) in K.
symmetry in K.
by rewrite (eqP (@act_free G _ _ K)).
set rho':= make_move rho (m_edge z n) in E z'm.
case yz: (y == z).
rewrite -{2}(eqP yz) in W.
have H: (rho' y) = act _ (rho' x) d
by rewrite /rho'; apply (@act0real3X xi rho)=>//.
rewrite (eqP E) in H. symmetry in H.
by rewrite W (eqP (@act_free G _ _ H)).
by apply: (@act0_edge_rest xi z n rho);
rewrite ?(eq_sym z x) ?U ?(eq_sym z y) ?yz=>//.
set rho':= make_move rho (m_edge z n) in E z'm.
case yz: (y == z).
rewrite -{2}(eqP yz) in W.
have H: (rho' y) = act _ (rho' x) d
by rewrite /rho'; apply (@act0real3X xi rho)=>//.
rewrite (eqP E) in H. symmetry in H.
by rewrite W (eqP (@act_free G _ _ H)).
by apply: (@act0_edge_rest xi z n rho);
rewrite ?(eq_sym z x) ?U ?(eq_sym z y) ?yz=>//.
case B: (action0X _ _ x z')=>[d'|]//.
case C: (action0X _ _ z y)=>[d''|]//.
set rho':= make_move rho (m_edge z n) in E z'm.
have H: (rho' z') = act _ (rho' x) d'
by rewrite /rho'; apply (@act0real3X xi rho)=>//.
have K: (rho' y) = act _ (rho' z) d''
by rewrite /rho'; apply (@act0real3X xi rho)=>//.
move/andP: z'm=>[_ z'm].
rewrite (eqP z'm) H act_mulP (eqP E) in K.
symmetry in K.
by rewrite (eqP (@act_free G _ _ K)).
set rho':= make_move rho (m_edge z n) in E z'm.
case yz: (y == z).
rewrite (eqP yz) in C.
have H:is_some (action0X xi (m_edge z n) z z).
by move: (@act0real1X xi rho (m_edge z n) real) => [R' [_ _]];
apply R'=>//.
by rewrite C in H.
by apply: (@act0_edge_rest xi z n rho);
rewrite ?(eq_sym z x) ?U ?(eq_sym z y) ?yz=>//.
set rho':= make_move rho (m_edge z n) in E z'm.
case yz: (y == z).
move:W B.
rewrite /action0X (eq_sym z x) U -(eqP yz) V !eq_refl.
case Y: (xi x y)=>//=; first by done.
case L: (xi x z')=>//=; first by done.
rewrite /rho' /make_move /state_space_G /state_space_G_action
!fgraph_fun_eq (eq_sym z x) (eq_sym z y) U yz in E.
rewrite /rho' /make_move /state_space_G /state_space_G_action
!fgraph_fun_eq (eq_refl) -(eqP yz) V (eqP yz) in z'm.
move/andP:z'm=>[_ z'm].
rewrite (eqP z'm) in E.
by elim: (Z _ _ E); rewrite L.
by apply: (@act0_edge_rest xi z n rho);
rewrite ?(eq_sym z x) ?U ?(eq_sym z y) ?yz=>//.
by move=>u;
apply (act0real2X (m:=m_edge z n) real (predictableX_edge_cond real u)).
move=>x y u v.
rewrite /make_move /state_space_G /state_space_G_action !fgraph_fun_eq.
rewrite (eq_sym u x) (eq_sym v x).
case U: (x == u); case V: (x == v)=> //=; rewrite U V => //=;
apply Z.
Qed.
Lemma act1real3X: forall xi rho m,
(realisesX xi rho) ->
(realises3X (action1X xi m (observe (make_move rho m))) (make_move rho m)).
Proof.
move=>xi rho m real.
move real_:real=>[[R [S T]] [Z A]].
case m.
move=>z n x y d.
set rho':= make_move rho (m_edge z n).
rewrite /action1X.
case pickP=>[z' z'm|]//.
rewrite /observe {1}/state_space_G {1}/state_space_G_obs eqrel_ieqrel
[rho']lock /= -lock in z'm.
rewrite /update.
case xz: (action0X _ _ x z)=>[d'|].
case z'y: (action0X _ _ z' y)=>[d''|].
case=>E.
have Hzx: rho' z = act _ (rho' x) d'
by apply (act0real3X (m:=m_edge z n) real).
have Hyz': rho' y = act _ (rho' z') d''
by apply (act0real3X (m:=m_edge z n) real).
move/andP:z'm=>[_ z'm].
by rewrite Hyz' -(eqP z'm) Hzx act_mulP E.
case xz': (action0X _ _ x z')=>[d''|].
case zy: (action0X _ _ z y)=>[d'''|].
case=>E.
move/andP:z'm=>[_ z'm].
have Hyz: rho' y = act G (rho' z) d'''
by apply (act0real3X (m:=m_edge z n) real).
have Hzx: rho' z = act G (rho' x) d'
by apply (act0real3X (m:=m_edge z n) real).
have Hz'x: rho' z' = act G (rho' x) d''
by apply (act0real3X (m:=m_edge z n) real).
have F: d' = d''
by rewrite (eqP z'm) Hz'x in Hzx;
rewrite (eqP (act_free_eq (@act_free G) Hzx)).
by rewrite Hyz Hzx act_mulP F E.
move=>E.
have Hyx: rho' y = act G (rho' x) d
by apply (act0real3X (m:=m_edge z n) real).
by rewrite Hyx.
move=>E.
have Hyx: rho' y = act G (rho' x) d
by apply (act0real3X (m:=m_edge z n) real).
by rewrite Hyx.
case xz': (action0X _ _ x z')=>[d''|].
case zy: (action0X _ _ z y)=>[d'''|].
case=>E.
have Hz'x: rho' z' = act G (rho' x) d''
by apply (act0real3X (m:=m_edge z n) real).
have Hyz': rho' y = act G (rho' z) d'''
by apply (act0real3X (m:=m_edge z n) real).
move/andP:z'm=>[_ z'm].
by rewrite Hyz' (eqP z'm) Hz'x act_mulP E.
move=>E.
have Hyx: rho' y = act G (rho' x) d
by apply (act0real3X (m:=m_edge z n) real).
by rewrite Hyx.
move=>E.
have Hyx: rho' y = act G (rho' x) d
by apply (act0real3X (m:=m_edge z n) real).
by rewrite Hyx.
move=>_ E.
by apply (act0real3X (m:=m_edge z n) real).
move=>x y u v.
rewrite /action1X.
by apply (act0real3X).
Qed.
Lemma act1realX: forall xi rho m,
(realisesX xi rho) ->
(realisesX (action1X xi m (observe (make_move rho m))) (make_move rho m)).
Proof.
move=>xi rho m real.
split; first by apply: act1real1X.
split; first by apply: act1real2X.
by apply: act1real3X.
Qed.
Lemma act01X: forall xi rho m,
(realisesX xi rho) ->
(predictableX xi m rho) ->
(action0X xi m = action1X xi m (observe (make_move rho m))).
Proof.
move=>xi rho m real.
move real_:real=>[[R [S T]] [Z A]].
rewrite /action1X.
case m=>[z n|]=>//.
rewrite /predictableX.
set rho':= make_move rho (m_edge z n).
move=>pred.
case: pickP=>[z' z'm|]=>//.
move/andP:z'm=>[z'm1 z'm2].
rewrite /observe {1}/state_space_G {1}/state_space_G_obs eqrel_ieqrel
[rho']lock /= -lock in z'm2.
case zz': (z == z').
have H:is_some (xi z z') by rewrite (eqP zz') R.
by rewrite (eqP z'm1) in H.
have H:is_some (action0X xi (m_edge z n) z z') by apply:pred; rewrite (eqP z'm2).
by rewrite /action0X eq_refl zz' (eqP z'm1) in H.
Qed.
Lemma obs_relX: forall xi rho rho',
(realisesX xi rho) -> (realisesX xi rho') ->
((observe rho) == (observe rho')).
Proof.
move=>xi rho rho' [[_ [_ _]] [Z1 A1]] [[_ [_ _]] [Z2 A2]].
rewrite /observe /state_space_G /state_space_G_obs.
apply: ieqrel_of_eqrel_congr=>/=[x y].
apply: iffB=>[H|H].
by rewrite (A2 _ _ _ (Z1 _ _ H)) act_unitP eq_refl.
by rewrite (A1 _ _ _ (Z2 _ _ H)) act_unitP eq_refl.
Qed.
Next we study how the domain of the abstraction functions in X changes
during evolution
Definition separate_rel(r:rel P) (x:P) := fun u v =>
match (u == x, v == x) with
| (false, false) => r u v
| (true, true) => true
| _ => false
end.
Definition join_rel(r:rel P) (x y:P) :=
fun u v => (r u v) || ((r u x && r y v) || (r u y && r x v)).
Lemma is_some_act0X: forall xi m rho,
realisesX xi rho ->
forall x y, is_some (action0X xi m x y) =
if m is m_jump z z' then
(if z == z' then is_some (xi x y)
else (join_rel (separate_rel (fun x y =>is_some (xi x y)) z) z z') x y)
else is_some (xi x y).
Proof.
move=>xi m rho [[R [S T]] _] x y.
rewrite /action0X.
case:m =>[z n| z z'].
case U: (z == x);case V: (z == y)=>//.
by rewrite -(eqP U) -(eqP V) R.
by case: (xi x y).
by case: (xi x y).
case U: (z == x);case V: (z == y)=>//=.
by rewrite /join_rel /separate_rel -(eqP U) -(eqP V) eq_refl;
case W: (z == z')=>//; by rewrite R.
rewrite /join_rel /separate_rel -(eqP U) eq_refl (eq_sym y z) V.
case W: (z == z').
by rewrite (eqP W).
by rewrite (eq_sym z' z) W andTb orFb andFb orbF.
rewrite /join_rel /separate_rel -(eqP V) eq_refl (eq_sym x z) U.
case W: (z == z').
by rewrite (eqP W).
by rewrite (eq_sym z' z) W andbT orFb andFb orFb.
rewrite /join_rel /separate_rel eq_refl (eq_sym x z) U (eq_sym y z) V.
case W: (z == z')=>//.
by rewrite andFb andbF !orbF.
Qed.
Lemma is_some_act1X: forall xi m rho o,
realisesX xi rho ->
forall x y, is_some (action1X xi m o x y) =
match m with
| m_edge z n =>
match pick (fun z' => (xi z z' == None) && (erel (eqrel_of_ieqrel o) z z')) with
| Some z' => (join_rel (fun x y =>is_some (xi x y)) z z') x y
| None => is_some (xi x y)
end
| m_jump z z' =>
(if z == z' then is_some (xi x y)
else (join_rel (separate_rel (fun x y =>is_some (xi x y)) z) z z') x y)
end.
Proof.
move=> xi m rho o real x y.
rewrite /action1X.
case: m=>[z n | z z'].
case: (pickP)=>[z' z'm|].
by rewrite is_some_update !(is_some_act0X (m_edge z n) real).
by move=>_; rewrite !(is_some_act0X (m_edge z n) real).
by rewrite !(is_some_act0X (m_jump z z') real).
Qed.
Lemma is_some_act1_edge_npred: forall xi z n rho,
realisesX xi rho ->
~(predictableX xi (m_edge z n) rho) ->
exists z', (xi z z' == None) /\
forall x y,
is_some (action1X xi (m_edge z n) (observe (make_move rho (m_edge z n))) x y) =
(join_rel (fun x y =>is_some (xi x y)) z z') x y.
Proof.
move=>xi z n rho real npred.
set o:=observe (make_move rho (m_edge z n)).
set b:=fun z' => (xi z z' == None) && (erel (eqrel_of_ieqrel o) z z').
case U: (pick b)=>[z'|].
exists z'.
split.
case: (pickP) U=>[u um|]; first by case=>[<-]; move/andP: um=>[K _].
by move=>e; contradiction (npred (predictableX_edge_cond real e)).
move=>x y; rewrite (is_some_act1X (m_edge z n) o real).
fold b.
case: (pickP) U=>[u um|]; first by case=>[<-]; move/andP: um=>[K _].
by move=>e; contradiction (npred (predictableX_edge_cond real e)).
case: (pickP) U=>[u um|]//.
by move=>e; contradiction (npred (predictableX_edge_cond real e)).
Qed.
Lemma erel_observe_G: forall rho x y,
erel (observe (s:=state_space_G) rho) x y = (rho x == rho y).
Proof.
move=>rho x y.
by rewrite /observe {1}/state_space_G {1}/state_space_G_obs eqrel_ieqrel.
Qed.
Lemma join_rel_same: forall (r:rel P) x u v,
(forall x y z, r x y -> r y z -> r x z) ->
join_rel r x x u v = r u v.
Proof. move=>r x u v T. rewrite /join_rel. apply:iffB.
move/or3P=>[H1|H2|H3]//. by apply: (T u x v); move/andP:H2=>[H21 H22].
by apply: (T u x v); move/andP:H3=>[H31 H32].
move=>K; apply/or3P. by apply: Or31.
Qed.
Lemma is_some_init_finest: forall rho xi,
realisesX xi rho ->
(forall x y, is_some ((initX rho) x y) -> is_some (xi x y)).
Proof.
move=>rho xi [[R [S T]] [Z A]] x y.
rewrite /initX.
case U: (rho x == rho y)=>//H.
by rewrite (Z x y U).
Qed.
Lemma is_some_action1X_finer: forall rho m xi1 xi2,
realisesX xi1 rho -> realisesX xi2 rho ->
(forall x y, is_some (xi1 x y) -> is_some (xi2 x y)) ->
(forall x y, is_some (action1X xi1 m (observe (make_move rho m)) x y)
-> is_some (action1X xi2 m (observe (make_move rho m)) x y)).
Proof.
move=>rho m x1 x2 r1 r2 H x y.
rewrite (is_some_act1X m _ r1).
rewrite (is_some_act1X m _ r2).
move: r1=>[[R1 [S1 T1]] [Z1 A1]].
move: r2=>[[R2 [S2 T2]] [Z2 A2]].
case: m=>[z n|z z'].
case: pickP=>[z1 z1m|z1e].
case: pickP=>[z2 z2m|z2e].
rewrite !erel_observe_G in z1m z2m.
move/andP: z1m=>[z1m1 z1m2]; move/andP: z2m=>[z2m1 z2m2].
rewrite (eqP z1m2) in z2m2.
rewrite /make_move /state_space_G /state_space_G_action !fgraph_fun_eq in z2m2.
case U: (z == z1) z2m2=>z2m2.
case V: (z == z2) z2m2=>z2m2.
by rewrite -(eqP U) -(eqP V) !join_rel_same //; apply: H.
by rewrite -(eqP U) !join_rel_same // /join_rel=>K; apply/or3P; apply: Or31; apply: H.
case V: (z == z2) z2m2=>z2m2.
by rewrite (eqP V) in z2m1; move: (R2 z2); rewrite (eqP z2m1).
have T: is_some (x1 z1 z2) by rewrite (Z1 z1 z2 z2m2).
rewrite /join_rel.
move/or3P=>[K1|K2|K3].
by apply/or3P; apply: Or31; apply: H.
apply/or3P; apply: Or32. apply/andP; split. by apply:H; move/andP: K2=>[K21 K22].
apply:H; move/andP: K2=>[K21 K22]. by apply: (T1 _ z1 _); first by apply: S1.
apply/or3P; apply: Or33. apply/andP; split.
apply:H; move/andP: K3=>[K31 K32]. by apply: (T1 _ z1 _).
by apply:H; move/andP: K3=>[K31 K32].
rewrite !erel_observe_G in z1m.
move/andP: z1m=>[z1m1 z1m2].
move/nandP: (z2e z1)=>[z2e1|z2e2].
rewrite /make_move /state_space_G /state_space_G_action !fgraph_fun_eq in z1m2.
rewrite /join_rel.
have U: is_some (x2 z z1). case V: (x2 z z1)=>//. by rewrite V eq_refl in z2e1.
move/or3P=>[K1|K2|K3].
by apply: H.
move/andP: K2=>[K21 K22]. apply: (T2 _ z _ (H _ _ K21) _). apply: (T2 _ z1 _ U (H _ _ K22)).
move/andP: K3=>[K31 K32]. apply: (T2 _ z1 _ (H _ _ K31) _). apply: (T2 _ z _ (S2 _ _ U) (H _ _ K32)).
by rewrite erel_observe_G z1m2 in z2e2.
case: pickP=>[z2 z2m|z2e].
rewrite /join_rel. move=>K. by apply/or3P; apply Or31; apply H.
by move=>K; apply: H.
case U: (z == z').
by move=>K; apply: H.
rewrite /join_rel /separate_rel !eq_refl (eq_sym z' z) !U.
case V: (x == z).
case W: (y == z)=>//=.
rewrite !orbF. by move=>K; apply: H.
case W: (y == z)=>//=.
rewrite !andbT. by move=>K; apply: H.
rewrite !andbF !orbF. by move=>K; apply: H.
Qed.
To complete the definition of the abstraction, we must show that the underlying set
is finite and that all properties are decidable, i.e. can be modelled as functions
to bool. We therefore define an intensional version of the abstraction next.
Definition iX := finFun {P * P :as finType} (optionFin (edgegroup G)).
Definition iXX: X -> iX :=
fun xi => fgraph_of_fun (fun xy => xi xy.1 xy.2).
Definition XiX: iX -> X := fun ixi => fun x y => ixi (x, y).
Lemma XiX_iXX: forall xi, XiX (iXX xi) =2 xi.
Proof. by move=>xi x y; rewrite /XiX /iXX fgraph_fun_eq. Qed.
Lemma iXX_XiX: forall ixi, iXX (XiX ixi) == ixi.
Proof. by move=>ixi; apply: eq_finfun=>x; rewrite /XiX /iXX fgraph_fun_eq; case:x. Qed.
Lemma iXX_eq: forall xi1 xi2, xi1 =2 xi2 -> iXX xi1 == iXX xi2.
Proof. by move=>xi1 xi2 E; apply/eqP; apply: fgraph_of_fun_congr; by move=>[x y]. Qed.
Opaque iXX XiX.
Definition initiX(rho: env): iX := iXX (initX rho).
Definition action0iX(ixi: iX) (m:move): iX := iXX (action0X (XiX ixi) m).
Definition action1iX(ixi: iX) (m:move) (o:obs): iX := iXX (action1X (XiX ixi) m o).
Definition irefl_dom(xi:iX):= iforall(fun x=> is_some (XiX xi x x)).
Definition isym_dom(xi:iX):=
iforall2( fun x y=> (is_some (XiX xi x y)) ==> (is_some (XiX xi y x)) ).
Definition itrans_dom(xi:iX):=
iforall3( fun x y z => (is_some (XiX xi x y))
==> ((is_some (XiX xi y z)) ==> (is_some (XiX xi x z))) ).
Definition realises1iX(xi:iX) : bool :=
(irefl_dom xi) && (isym_dom xi) && (itrans_dom xi).
Definition realises2iX(xi:iX) (rho:state_space_G) : bool :=
iforall2( fun x y => (rho(x) == rho(y)) ==> (XiX xi x y == Some unit) ).
Definition realises3iX(xi:iX) (rho:state_space_G) : bool :=
iforall3( fun x y d => (XiX xi x y == Some d ) ==> ((rho y) == act G (rho x) d) ).
Definition realisesiX(xi:iX) (rho:state_space_G) : bool :=
(realises1iX xi) && (realises2iX xi rho) && (realises3iX xi rho).
Definition is_singleton(xi:iX) (x:P) : bool :=
iforall (fun y => (is_some (XiX xi x y)) ==> (x == y)).
Definition predictableiX(xi:iX) (m:move) (rho:state_space_G) : bool :=
match m with
| m_edge z n =>
iforall2( fun x y => ((make_move rho m) x == (make_move rho m) y)
==> (is_some (action0X (XiX xi) m x y)))
| m_jump z z' =>
(z == z') || (negb (is_singleton xi z))
end.
Lemma realises1iX_X: forall ixi, realises1iX ixi -> realises1X (XiX ixi).
Proof.
move=>ixi.
rewrite /realises1iX /realises1X.
move=>H; rewrite /irefl_dom /isym_dom /itrans_dom in H.
move/andP:H=>[H12 H3]; move/andP:H12=>[H1 H2].
split.
by apply: (iforallP H1).
split.
by move=>x y; apply/implyP; apply: (iforall2P H2).
by move=>x y z E; apply/implyP; move:E; apply/implyP;
apply: (iforall3P H3).
Qed.
Lemma realises1X_iX: forall xi, realises1X xi -> realises1iX (iXX xi).
move=>xix [H1 [H2 H3]].
apply/andP; split.
apply/andP; split.
by apply/iforallP; move=>x; rewrite /= !XiX_iXX H1.
by apply/iforallP; move=>[x y]; apply /implyP; rewrite !XiX_iXX; apply: H2.
by apply/iforallP; move=>[[x y] z]; rewrite !XiX_iXX; apply /implyP; move=>E;
apply/implyP; apply: H3.
Qed.
Lemma realises2iX_X: forall ixi rho,
realises2iX ixi rho -> realises2X (XiX ixi) rho.
Proof. by move=>ixi rho H x y E; rewrite (eqP (implyP (iforall2P H x y) E)).
Qed.
Lemma realises2X_iX: forall xi rho,
realises2X xi rho -> realises2iX (iXX xi) rho.
Proof.
by move=>xi rho H; apply/iforall2P=>x y; apply/implyP=>E; apply/eqP;
rewrite !XiX_iXX; apply: H.
Qed.
Lemma realises3iX_X: forall ixi rho,
realises3iX ixi rho -> realises3X (XiX ixi) rho.
Proof.
by move=>xi rho H x y d K; apply/eqP;
apply: (implyP (iforall3P H x y d)); apply/eqP.
Qed.
Lemma realises3X_iX: forall xi rho,
realises3X xi rho -> realises3iX (iXX xi) rho.
move=>xi rho H.
apply/eqP; apply: fgraph_of_fun_congr; move=>[[x y] d]; rewrite /= !XiX_iXX.
by apply/implyP=>[E]; apply/eqP; apply H; rewrite (eqP E).
Qed.
Lemma realisesiX_X: forall ixi rho, realisesiX ixi rho -> realisesX (XiX ixi) rho.
Proof.
move=>xi rho.
move/andP=>[H12 H3]; move/andP:H12=>[H1 H2].
split; first by apply realises1iX_X. split; first by apply realises2iX_X.
by apply realises3iX_X.
Qed.
Lemma realisesX_iX: forall xi rho, realisesX xi rho -> realisesiX (iXX xi) rho.
Proof.
move=>xi rho [H1 [H2 H3]].
apply/andP; split.
apply/andP; split.
by apply: realises1X_iX. by apply: realises2X_iX. by apply: realises3X_iX.
Qed.
Lemma predictableX_ix: forall ixi m rho,
predictableiX ixi m rho -> predictableX (XiX ixi) m rho.
Proof.
move=>ixi m rho.
case: m=>[z n| z z'].
move=> H x y.
move/eqP=>E. move:E. apply/implyP.
by apply (iforall2P H x y).
done.
Qed.
The abstraction claimed to exist in Lemma 10 of the paper:
Definition abstractionG : abstraction state_space_G.
apply (@mkAbst state_space_G iX initiX action0iX action1iX
realisesiX predictableiX).
move=>rho.
apply/andP; split.
apply/andP; split.
apply: realises1X_iX; apply initXreal1.
apply: realises2X_iX; apply initXreal2.
apply: realises3X_iX; apply initXreal3.
move=>xi rho m ri pi.
by apply: iXX_eq; rewrite -act01X; try apply: realisesiX_X;
try apply: predictableX_ix.
move=>xi rho m ri.
by apply: realisesX_iX; apply: act1realX; apply: realisesiX_X.
move=>xi rho rho' ri ri'.
by apply: (obs_relX (realisesiX_X ri) (realisesiX_X ri')).
Defined.
Having defined the abstraction, it remains to show that it has the
properties claimed in Lemma 10 of the paper.
We start by analysing the domain of the partial functions in the
abstraction.
Definition dom_abstr_rel (xi: abstractionG): rel P :=
fun x y => is_some (XiX xi x y).
Definition dom_abstr(E:econf abstractionG): ieqrel P.
move=>E.
apply: ieqrel_of_eqrel.
apply: (Eqrel (erel:= dom_abstr_rel (piX E)));
rewrite /piX;
elim: E=>[[/=C xi] real];
move/andP: real=>/=[r12 _]; move/andP: r12=>[r1 _];
move/andP: r1=>/=[reflsym trans]; move/andP: reflsym=>[refl sym].
by move: (iforallP refl).
by move=>x y; apply/implyP; apply: (iforall2P sym x y).
by move=>x y z H K; apply: (implyP (implyP (iforall3P trans x y z) H) K).
Defined.
Lemma erel_dom_abstr: forall E x y,
erel (dom_abstr E) x y = dom_abstr_rel (piX E) x y.
Proof. by move=>E x y; rewrite /dom_abstr eqrel_ieqrel /=. Qed.
The next Lemma is Lemma 10.1 in the paper.
Lemma init_factors: forall rho rho',
(observe rho == observe rho') -> (init abstractionG rho == init _ rho').
Proof.
move=>rho rho' oe.
rewrite /init /piX /= /initiX /initX /=.
apply iXX_eq=>x y.
have H: forall u v, erel (observe rho) u v = erel (observe rho') u v.
by move=>u v; rewrite (eqP oe).
move: (H x y).
rewrite /observe /state_space_G /state_space_G_obs !eqrel_ieqrel /=.
by move=>[->].
Qed.
Definition obs_abstG(E: econf abstractionG) := dom_abstr E.
The next Lemma is Lemma 10.2 in the paper.
Lemma econf_det_abstG: forall E E',
(econf_conf E == econf_conf E') -> (obs_abstG E == obs_abstG E') -> (E == E').
Proof.
move=>E E' Ce oe.
rewrite stepe_eqd.
have H: (piS E == piS E').
by rewrite /piS (eqP Ce) eq_refl.
apply/andP; split.
apply/andP; split=>//.
by rewrite /piQ (eqP Ce) eq_refl.
clear Ce.
rewrite /obs_abstG in oe.
rewrite -(eqP (iXX_XiX (piX E))) -(eqP (iXX_XiX (piX E'))).
apply: iXX_eq=>x y.
have D: erel (dom_abstr E) x y = erel (dom_abstr E') x y by rewrite (eqP oe).
clear oe.
rewrite !erel_dom_abstr /dom_abstr_rel in D.
move: (realisesiX_X (real_econf E)) =>[_ [_ A]].
move: (realisesiX_X (real_econf E')) =>[_ [_ A']].
rewrite (eqP H) in A; move: (A x y)=> Axy; move: (A' x y)=> A'xy; clear A A'.
case U: (XiX (piX E) x y)=>[d|];
case U': (XiX (piX E') x y)=>[d'|].
have V: (act G (piS E' x) d = act G (piS E' x) d')
by rewrite -(Axy d) // (A'xy d').
by rewrite (eqP (act_free_eq (act_free (g:=G)) V)).
by rewrite U U' in D.
by rewrite U U' in D.
by done.
Qed.
Finally, for Lemma 10.3 we now work towards the definition of the measure function.
Variable J:jag.
Lemma dom_abstr_act0: forall (E:econf abstractionG),
negb (stepn J E) ->
dom_abstr (stepe J E) =
if (jag_move J (piQ E) (observe (piS E))) is m_jump z z' then
(if z == z' then dom_abstr E
else join (separate (dom_abstr E) z) z z')
else dom_abstr E.
Proof.
move=>E nn.
apply/eqP; apply: eqrel_of_ieqrel_inj=>x y.
rewrite !erel_dom_abstr /dom_abstr_rel.
rewrite stepe_X0=>//.
rewrite /action0 /abstractionG /action0iX XiX_iXX.
case: (jag_move)=>[z n|z z'].
by rewrite !erel_dom_abstr /dom_abstr_rel;
rewrite (is_some_act0X _ (realisesiX_X (real_econf E))).
rewrite (is_some_act0X _ (realisesiX_X (real_econf E))).
case U: (z == z').
by rewrite !erel_dom_abstr /dom_abstr_rel.
by rewrite erel_join !erel_separate /join_rel /separate_rel
!erel_dom_abstr /dom_abstr_rel !eq_refl.
Qed.
Lemma XiX_action1: forall (xi:abstractionG) m o,
XiX (action1 xi m o) =2 action1X (XiX xi) m o.
Proof.
by move=>xi m o x y; rewrite /action1 /abstractionG /action1iX XiX_iXX.
Qed.
Lemma dom_abstr_act1: forall (E:econf abstractionG),
dom_abstr (stepe J E) =
match jag_move J (piQ E) (observe (piS E)) with
| m_edge z n =>
match pick (fun z' => (XiX (piX E) z z' == None)
&& (erel (eqrel_of_ieqrel (observe (piS (stepe J E)))) z z')) with
| Some z' => join (dom_abstr E) z z'
| None => dom_abstr E
end
| m_jump z z' =>
(if z == z' then dom_abstr E
else join (separate (dom_abstr E) z) z z')
end.
Proof.
move=>E.
apply/eqP; apply: eqrel_of_ieqrel_inj=>x y.
rewrite !erel_dom_abstr /dom_abstr_rel.
rewrite stepe_X1=>//.
rewrite XiX_action1.
case: (jag_move)=>[z n|z z'].
rewrite (is_some_act1X _ _ (realisesiX_X (real_econf E))).
case: pickP=>[u u_mem|nonmem].
by rewrite erel_join /join_rel !erel_dom_abstr /dom_abstr_rel.
by rewrite !erel_dom_abstr /dom_abstr_rel.
rewrite (is_some_act1X _ _ (realisesiX_X (real_econf E))).
case: (z == z').
by rewrite !erel_dom_abstr /dom_abstr_rel.
by rewrite erel_join !erel_separate /join_rel /separate_rel
!erel_dom_abstr /dom_abstr_rel.
Qed.
Lemma dom_abstr_act1_edge_npred: forall E z n,
stepn J E ->
jag_move J (piQ E) (observe (piS E)) = (m_edge z n) ->
exists z', negb (erel (dom_abstr E) z z')
&& (dom_abstr (stepe J E) == join (dom_abstr E) z z').
Proof.
move=>E z n nn e.
have npred: ~(predictableX (XiX (piX E)) (m_edge z n) (piS E)).
move=>c.
rewrite /stepn e /predictable /abstractionG /predictableiX in nn.
rewrite /predictableX in c.
elim: (iforallPn nn)=>[[x y] xm].
rewrite implybE in xm.
elim: (norP xm)=>[xm1 xm2].
by apply: (negP xm2 (c x y (eqP (negbE2 xm1)))).
elim: (is_some_act1_edge_npred (z:=z) (n:=n)
(realisesiX_X (real_econf E)) npred) => [z' [z'm1 z'm2]].
exists z'.
apply/andP.
split.
by rewrite erel_dom_abstr /dom_abstr_rel (eqP z'm1).
apply: eqrel_of_ieqrel_inj=>x y.
rewrite erel_join !erel_dom_abstr /dom_abstr_rel stepe_X1 stepe_S XiX_action1 e.
rewrite /join_rel in z'm2.
apply: z'm2.
Qed.
Lemma erel_dom_card_step_pred: forall (E:econf abstractionG),
negb (stepn J E) ->
card (quotient (dom_abstr E)) = card (quotient (dom_abstr (stepe J E))).
Proof.
move=>E nn.
rewrite (dom_abstr_act0 nn).
move:nn; rewrite /stepn.
case: (jag_move)=>//[z z'].
rewrite /predictable /abstractionG /predictableiX.
move/negbE2.
move/orP=>[nn|nn]; first by rewrite nn.
move/iforallPn:nn=>[u u_mem].
rewrite implybE in u_mem; move: (norP u_mem)=>[u_mem1 u_mem2].
case U: (z == z').
by done.
rewrite -(addnK 1 (card (quotient (dom_abstr E)))) addn1.
rewrite -(card_separate_quotient_eq (z:=z) (z':=u)).
rewrite -(card_quotient_join_lt (r:=separate (dom_abstr E) z) (u:=z) (v:=z')).
by rewrite -addn1 addnK.
by rewrite erel_separate eq_refl (eq_sym z' z) U.
by done.
by rewrite erel_dom_abstr /dom_abstr_rel; apply: (negbE2 u_mem1).
Qed.
Lemma erel_dom_card_step_npred: forall (E:econf abstractionG),
stepn J E ->
card (quotient (dom_abstr E)) = (card (quotient (dom_abstr (stepe J E)))).+1.
Proof.
move=>E.
rewrite (dom_abstr_act1) /stepn {1}/predictable {1}/abstractionG /predictableiX.
rewrite stepe_S.
case: (jag_move)=>[z n nn|z z' nn].
case: (pickP)=>[u um|e].
by move/andP:um => [um1 um2];
rewrite card_quotient_join_lt=>//;
rewrite erel_dom_abstr /dom_abstr_rel (eqP um1).
have npred: ~(predictableX (XiX (piX E)) (m_edge z n) (piS E)).
move=>c.
rewrite /predictableX in c.
elim: (iforallPn nn)=>[[x y] xm].
rewrite implybE in xm.
elim: (norP xm)=>[xm1 xm2].
by apply: (negP xm2 (c x y (eqP (negbE2 xm1)))).
by case: (npred (predictableX_edge_cond (z:=z) (n:=n)
(realisesiX_X (real_econf E)) e)).
case U: (z == z').
by move/norP: nn=>[nn _]; rewrite U in nn.
move/norP: nn=>[nn1 nn2]. move: (iforallP (negbE2 nn2))=>H.
rewrite card_quotient_join_lt.
have e: (dom_abstr E) == (separate (dom_abstr E) z).
apply: separate_singleton.
move=>x; rewrite erel_dom_abstr /dom_abstr_rel=>xm.
by apply: (implyP (H x) xm).
by rewrite -(eqP e).
by rewrite erel_separate eq_refl (eq_sym z' z) U.
Qed.
The measure function from Lemma 10.3 and its properties.
Definition measure_abstG(E : econf abstractionG) :=
card (quotient (dom_abstr E)).
Lemma measure_upper_abstG: forall E, measure_abstG E <= card P.
Proof. by move=>E; apply: card_quotient_upper. Qed.
Lemma measure_lower_abstG: forall E, 0 < measure_abstG E.
Proof. by move=>E; apply: card_quotient_lower; rewrite (cardD1 sP). Qed.
Lemma measure_step_abstG:
forall E, measure_abstG (stepe J E) = (measure_abstG E) - (stepn J E).
Proof.
move=>E.
rewrite /measure_abstG.
case U: (stepn J E).
by rewrite (erel_dom_card_step_npred (E:=E)) // subn1.
by rewrite (erel_dom_card_step_pred (E:=E)) ?subn0 ?U.
Qed.
Lemma measure_init_abstG: forall E m,
measure_abstG (eevolution J m E)
<= measure_abstG (eevolution J m (init_econf _ (econf_conf E))).
Proof.
move=>E m.
have H: forall m x y,
erel (dom_abstr (eevolution J m (init_econf _ (econf_conf E)))) x y
-> erel (dom_abstr (eevolution J m E)) x y.
elim=>[x y | m' IH x y].
elim: E=>[[[q rho] xi] Em].
rewrite !erel_dom_abstr /dom_abstr_rel /=.
rewrite /piX /init_econf /state_space_G /init /= /initiX XiX_iXX.
rewrite /econfP /= in Em.
move=>K. by apply (@is_some_init_finest rho (XiX xi) (realisesiX_X Em)).
rewrite [dom_abstr]lock [init_econf]lock /= -!lock.
move: (real_econf (eevolution J m' E)).
move: (real_econf (eevolution J m' (init_econf abstractionG (econf_conf E)))).
rewrite !erel_dom_abstr /dom_abstr_rel /=.
rewrite !stepe_X1 !stepe_S.
rewrite /action1 /state_space_G /= /action1iX !XiX_iXX.
rewrite /piS /piQ !econf_conf_eevolution !econf_conf_init_econf.
move=>r1 r2.
apply is_some_action1X_finer =>//.
by apply: realisesiX_X.
by apply: realisesiX_X.
move=>u v.
move: (IH u v).
by rewrite !erel_dom_abstr /dom_abstr_rel /=.
rewrite /measure_abstG.
apply: card_quotient_leq.
apply: H.
Qed.
End ExistenceAbstraction.
We can now give bounds on the number of nodes reachable by a JAG
in a free action graph.
This section corresponds to the development after Lemma 10 in
Section 4 of the paper.
Section Analysis.
We assume abstractly the properties of Lemma 10, for which we have
just constructed a concrete instance in the previous section.
Variable J: jag.
Variable G: graph.
Variable X: abstraction (state_space_G G).
Variable measure: econf X -> nat.
Variable measure_upper: forall E, measure E <= card P.
Variable measure_lower: forall E, 0 < measure E.
Variable measure_step: forall E, measure (stepe J E) = (measure E) - (stepn J E).
Variable measure_init: forall E m,
measure (eevolution J m E) <= measure (eevolution J m (init_econf X (econf_conf E))).
Variable init_factors: forall rho rho', (observe rho == observe rho') -> (init X rho == init X rho').
Variable obs_abst: econf X -> obs.
Variable econf_det: forall E E',
(econf_conf E == econf_conf E') -> (obs_abst E == obs_abst E') -> (E == E').
Definition 11 in the paper.
Definition coal(k n:nat) (E : econf X) :=
find (fun E'=> measure E' <= card P - n) (eevolution_seq J k E).
Definition coalE(k n:nat) (E : econf X) := eevolution J (coal k n E) E.
Lemma coal_triv_bound: forall k n E, coal k n E <= k.
Proof. by move=>k n E; rewrite /coal -{2}(size_eevolution_seq J k E) find_size. Qed.
Lemma coal_cardP: forall k E, coal k (card P) E = k.
Proof.
move=>k E.
case: (leqP k (coal k (card P) E))=>[le|gt].
by apply/eqP; rewrite eqn_leq; apply/andP; split=>//; apply: coal_triv_bound.
rewrite /coal -{2}(size_eevolution_seq J k E) -has_find in gt.
move/hasP: gt=>[x xm xp].
by rewrite subnn leqNgt measure_lower in xp.
Qed.
Lemma measure_eevolution_coal: forall k n E,
coal k n E < k ->
measure (eevolution J (coal k n E) E) <= card P - n.
Proof.
move=>k n E H.
rewrite (eevolution_sub J E H) /coal.
set a:=fun E'=> measure E' <= card P - n.
have U: a (sub E (eevolution_seq J k E) (find a (eevolution_seq J k E))).
apply: sub_find.
rewrite has_find size_eevolution_seq.
by rewrite /coal in H.
by rewrite {1}/a /= in U.
Qed.
Lemma before_measure: forall k n E l,
l < coal k n E ->
measure (eevolution J l E) > card P - n.
Proof.
move=>k n E l H.
have K: l < k by apply: (leq_trans H (coal_triv_bound k n E)).
rewrite ltnNge (eevolution_sub J E K) /coal.
set a:=fun E'=> measure E' <= card P - n.
have U: a (sub E (eevolution_seq J k E) l) = false.
by apply: before_find.
by rewrite {1}/a /= in U; apply: negbT.
Qed.
Lemma measure_leq: forall m E, measure (eevolution J m E) <= measure E.
Proof.
elim=>[E|m IH E]/=.
by apply: leqnn.
by rewrite measure_step; apply: (leq_trans _ (IH E)); apply: leq_subr.
Qed.
Lemma measure_loop: forall m E,
(0 < m) -> (eevolution J m E == E) -> forall n, (measure (eevolution J n E) == measure E).
Proof.
move=>m E l H n.
case: (ltnP (measure (eevolution J n E)) (measure E))=>[K|K].
case: m l H K => //[m l H K].
have U: measure (eevolution J ((m.+1)*n) E) < measure E.
by apply: (leq_trans _ K); rewrite ltnS /= mulSn addnC -eevolution_sum; apply measure_leq.
have V: eevolution J ((m.+1)*n) E == E.
clear U K; elim: n =>[|n IH].
by rewrite muln0 eq_refl.
by rewrite -[n.+1]addn1 muln_addr -eevolution_sum muln1 (eqP H) (eqP IH) eq_refl.
by rewrite (eqP V) ltnn in U.
by rewrite eqn_leq K measure_leq=>//.
Qed.
Lemma coal_stepn: forall k n E,
0 < coal k n E -> coal k n E < k
-> stepn J (eevolution J ((coal k n E)-1) E).
Proof.
move=>k n E ll lu.
case U: (stepn J (eevolution J (coal k n E - 1) E))=>//.
have H: measure (eevolution J (coal k n E - 1) E) = measure (eevolution J (coal k n E-1).+1 E).
by rewrite /= measure_step U subn0.
rewrite {2}subn1 (ltn_predK ll) in H.
have K: coal k n E - 1 < coal k n E by rewrite subn1 (ltn_predK ll) leqnn.
rewrite {2}/coal in K.
rewrite -(@before_find _ E _ _ _ K) -eevolution_sub ?H ?measure_eevolution_coal ?eq_refl =>//.
by rewrite subn1 (ltn_predK ll) ltnW.
Qed.
Lemma coal_bound: forall k E m n,
(forall m', m <= m' -> measure (eevolution J m' E) == measure (eevolution J m E))
-> coal k n E < k
-> coal k n E <= m.
Proof.
move=>k E m n H l.
case: (leqP (coal k n E) m)=>//=[K].
have H1: measure (eevolution J (coal k n E - 1) E) == measure (eevolution J m E).
by apply: H; rewrite subn1 -(leq_add2r 1) !addn1 (ltn_predK K).
have H2: measure (eevolution J (coal k n E - 1).+1 E) == measure (eevolution J m E).
by apply: H; rewrite subn1 (ltn_predK K) ltnW.
rewrite /= measure_step (coal_stepn (leq_trans (ltn0Sn m) K) l) in H2.
rewrite -(eqP H1) /nat_of_bool subn1 -eqSS (ltn_predK (measure_lower _)) in H2.
by elim: (measure (eevolution J (coal k n E - 1) E)) H2.
Qed.
Lemma coal0: forall k E, coal k 0 E = 0.
Proof. by case=>//k E; rewrite /coal /= subn0 measure_upper. Qed.
Lemma sub_n0: forall m n, m > 0 -> n <= n - m -> n = 0.
Proof.
move=>m n H K.
case: (leqP m n)=>[L|L].
rewrite -{1}(subnK L) -{2}[n-m]add0n in K.
have F: m <= 0 by rewrite -(leq_add2r (n-m)) K.
by move: (leq_trans H F).
have U: n <= m by apply: ltnW.
by rewrite -eqn_sub0 in U; rewrite (eqP U) leqn0 in K; rewrite (eqP K).
Qed.
Lemma coal_nbound: forall k n E, coal k n E < k -> n < card P.
Proof.
move=>k n E l.
have H: measure (eevolution J (coal k n E) E) <= card P - n by apply: measure_eevolution_coal.
have K: 0 < card P - n. by apply: (leq_trans _ H).
by rewrite -ltn_0sub.
Qed.
Lemma coal_defined: forall k n E,
coal k n.+1 E < k -> coal k n E < k.
Proof.
move=>k n E c.
case: (leqP k (coal k n E))=>//[l].
case: (leqP (coal k n.+1 E) 0)=>[z|nz].
rewrite leqn0 in z.
have H: measure (eevolution J (coal k n.+1 E) E) <= card P - n.+1.
by rewrite measure_eevolution_coal.
rewrite (eqP z) /= in H.
have K: measure E <= card P - n.
apply: (leq_trans H _).
by rewrite -addn1 -subn_sub leq_sub_add; apply: leq_addl.
have L: coal k n E = 0.
case: k c l z=>[|k c l z].
by rewrite ltn0.
by rewrite /coal /= K.
rewrite L in l.
by move: (leq_trans c l); rewrite ltn0.
have H: has (fun E'=> measure E' <= card P - n) (eevolution_seq J k E).
apply/(has_subP E).
exists (coal k n.+1 E - 1).
by rewrite size_eevolution_seq (leq_trans _ c) // ltnS leq_subr.
rewrite -eevolution_sub.
have K: measure (eevolution J ((coal k n.+1 E - 1).+1) E) ==
measure (eevolution J (coal k n.+1 E - 1) E) - stepn J (eevolution J (coal k n.+1 E - 1) E)=>/=.
by apply/eqP; apply: measure_step.
rewrite coal_stepn // in K.
rewrite subn1 (ltn_predK nz) in K=>//.
have L: measure (eevolution J ((coal k n.+1 E).-1) E) - true <= card P - n.+1.
by rewrite -(eqP K); apply: measure_eevolution_coal.
rewrite -(leq_add2l 1) !add1n -ltn_subS /nat_of_bool ?subnK in L=>//.
rewrite subn1; apply: (leq_trans _ L).
rewrite -[S (measure (eevolution J ((coal k n.+1 E).-1) E) - 1)]add1n.
by rewrite -leq_sub_add leqnn.
by apply: ltnW; apply: (coal_nbound c).
by rewrite ltnW // subn1 (ltn_predK nz).
rewrite has_find size_eevolution_seq in H.
by rewrite -(ltnn k) (leq_trans _ H) ?ltnS.
Qed.
Lemma coal_leq: forall k n E,
coal k n E <= coal k n.+1 E.
Proof.
move=>k n E .
case: (leqP k (coal k n E))=>[lecn|gtcn];
case: (leqP k (coal k n.+1 E))=>[lecSn|gtcSn].
have en: k == coal k n E by rewrite eqn_leq coal_triv_bound lecn.
have eSn: k == coal k n.+1 E by rewrite eqn_leq coal_triv_bound lecSn.
by rewrite -(eqP en) -(eqP eSn) leqnn.
have f: coal k n E < coal k n E by apply (leq_trans (coal_defined gtcSn) lecn).
by rewrite ltnn in f.
by apply: (leq_trans _ lecSn); apply: ltnW.
case: (leqP (coal k n E) (coal k n.+1 E))=>//[H].
have K: measure (eevolution J (coal k n.+1 E) E) <= card P - n.
apply: (@leq_trans (card P - n.+1)).
by apply measure_eevolution_coal.
by rewrite -addn1 -subn_sub leq_sub_add; apply: leq_addl.
have L: measure (eevolution J (coal k n.+1 E) E) > card P - n.
by apply (before_measure H).
rewrite -(ltnn (measure (eevolution J (coal k n.+1 E) E))).
by apply: (leq_trans _ L); rewrite ltnS.
Qed.
Lemma coal_measure_between: forall k n E m,
(coal k n E) <= m -> m < (coal k n.+1 E)
-> measure (eevolution J m E) = card P - n.
Proof.
move=>k n E m L1 L2.
have B: coal k n E < k.
apply: (@leq_trans (coal k n.+1 E)).
by apply: (leq_trans _ L2); rewrite ltnS.
by apply: coal_triv_bound.
have U: m = (coal k n E) + (m - coal k n E) by rewrite subnK.
have H1: measure (eevolution J m E) <= card P - n.
rewrite U addnC -eevolution_sum.
apply: (leq_trans _ (measure_eevolution_coal B)).
apply: measure_leq.
have H2: measure (eevolution J m E) > card P - n.+1.
by apply (before_measure L2).
case: (leqP (card P - n) 0)=>[leq|gt].
by rewrite leqn0 in leq; rewrite (eqP leq) leqn0 in H1; rewrite (eqP leq) (eqP H1).
by rewrite -[n.+1]addn1 -subn_sub -ltnS in H2;
rewrite -[(card P - n - 1).+1]add1n subnK // ?ltnS in H2;
apply/eqP; rewrite eqn_leq; apply/andP; split.
Qed.
Lemma coal_stepn_between: forall k n E m,
(coal k n E) <= m -> S m < (coal k n.+1 E)
-> negb (stepn J (eevolution J m E)).
Proof.
move=>k n E m le lt.
have M1: measure (eevolution J m E) = card P - n.
by apply (coal_measure_between le); apply ltnW.
have M2: measure (eevolution J m.+1 E) == card P - n.
by apply/eqP; apply (coal_measure_between (leq_trans le (leqnSn m))).
rewrite -M1 /= measure_step in M2.
rewrite -(@subnK (stepn J (eevolution J m E)) (measure (eevolution J m E))) in M2.
rewrite addKn -{1}[(measure _) - _]add0n eqn_addr in M2.
by case: (stepn) M2.
by case: (stepn); first by apply: measure_lower; apply: leq0n.
Qed.
Lemma coal_eqQX_before: forall k m n E1 E2,
(coal k n E1 = coal k n E2)
-> (eqdQX (coalE k n E1) (coalE k n E2))
-> (coal k n E1) <= m
-> m < (coal k n.+1 E1) -> m < (coal k n.+1 E2)
-> (eqdQX (eevolution J m E1) (eevolution J m E2)).
Proof.
move=>k m n E1 E2 ecoal eQX.
elim:m=>[le lmc1 lmc2| m IH le lmc1 lmc2]//=.
by rewrite leqn0 in le; rewrite /coalE -ecoal (eqP le) in eQX.
case: (leqP m.+1 (coal k n E1))=>[K|K].
have e: coal k n E1 == S m by rewrite eqn_leq; apply/andP; split.
by rewrite /coalE -ecoal (eqP e) in eQX.
rewrite ltnS in K.
apply: eqdQX_stepe.
apply (coal_stepn_between K)=>//.
rewrite ecoal in K; apply (coal_stepn_between K)=>//.
by apply: IH=>//; apply: ltnW.
Qed.
Lemma coal_eqQX: forall k n E1 E2,
(eqdQX (coalE k n E1) (coalE k n E2))
-> (coal k n E1 = coal k n E2)
-> (coal k n.+1 E1 = coal k n.+1 E2)
-> (observe (piS (coalE k n.+1 E1)) = observe (piS (coalE k n.+1 E2)))
-> (eqdQX (coalE k n.+1 E1) (coalE k n.+1 E2)).
Proof.
move=>k n E1 E2 eQX ecn ecSn ob.
case: (leqP k (coal k n E1)) =>[leq|gt].
have enk: coal k n E1 == k by rewrite eqn_leq coal_triv_bound leq.
have eSnk: coal k n.+1 E1 == k by rewrite eqn_leq coal_triv_bound (leq_trans leq (coal_leq _ _ _)).
rewrite /coalE -ecSn (eqP eSnk).
by rewrite /coalE -ecn (eqP enk) in eQX.
case U: ((coal k n.+1 E1) == (coal k n E1)).
by rewrite /coalE -ecSn (eqP U); rewrite /coalE -ecn in eQX.
rewrite /coalE ecSn.
case: (leqP (coal k n.+1 E2) 0)=>[H|H].
have K: coal k n E2 <= 0 by apply: leq_trans _ H; apply coal_leq.
rewrite !leqn0 in H K.
by rewrite !(eqP H); rewrite /coalE ecn (eqP K) in eQX.
rewrite -(ltn_predK H) /=.
apply: eqdQX_stepe_gen.
apply: (coal_eqQX_before ecn)=>//.
by rewrite -ltnS (ltn_predK H) ltn_neqAle -ecSn eq_sym U andTb; apply: coal_leq.
by rewrite ecSn -ltnS (ltn_predK H) ltnSn.
by rewrite -ltnS (ltn_predK H) ltnSn.
by rewrite /coalE ecSn -(ltn_predK H) /= in ob.
Qed.
Relation \sim_n in the paper:
Definition sim (k n : nat) (E1 E2 : econf X) : bool :=
iforall (fun i:(ordinal n.+1) =>
(coal k i E1 == coal k i E2)
&& (eqdQX (coalE k i E1) (coalE k i E2))).
Definition sim_rel(k n : nat) : eqrelType (econf X).
Proof.
move=>k n.
apply: (Eqrel (erel:=sim k n)).
by move=>E; apply/iforallP; move=>i/=; rewrite /eqdQX !eq_refl.
by move=>E1 E2 IH; apply/iforallP=>i;
move/andP: (iforallP IH i) =>/=[U1 U23]; move/andP: U23=>/=[U2 U3];
rewrite /eqdQX (eqP U1) (eqP U2) (eqP U3) !eq_refl.
by move=>E1 E2 E3 H K;
apply/iforallP=>i;
move/andP: (iforallP H i)=>[H1 H23]; move/andP: H23=>[H2 H3];
move/andP: (iforallP K i)=>[K1 K23]; move/andP: K23=>[K2 K3];
case: i H1 H2 H3 K1 K2 K3 => //= [i _ H1 H2 H3 K1 K2 K3];
rewrite /eqdQX (eqP H1) (eqP H2) (eqP H3) (eqP K1) (eqP K2) (eqP K3) !eq_refl.
Defined.
Lemma 13 in the paper
Lemma decomp_sim: forall k n E1 E2,
(sim k n E1 E2)
-> (coal k n.+1 E1 == coal k n.+1 E2)
-> (observe (piS (coalE k n.+1 E1)) = observe (piS (coalE k n.+1 E2)))
-> (sim k n.+1 E1 E2).
Proof.
move=>k n E1 E2 H E K; apply/iforallP; move=>[i i_mem] /=;
rewrite ltnS leq_eqVlt in i_mem.
case: (orP i_mem) =>[e|l].
apply/andP; rewrite (eqP e); split=>//=.
apply:coal_eqQX=>//.
by case: (andP (iforallP H (Ordinal (ltnSn n)))).
simpl in E.
case: (andP (iforallP H (Ordinal (ltnSn n))))=>/=[H1 _].
by rewrite (eqP H1).
by rewrite (eqP E).
by apply: (iforallP H (Ordinal l)).
Qed.
Relation \approx_n in the paper:
Definition equiv (k n: nat) : eqrelType (conf (state_space_G G)).
Proof.
move=>k n.
apply (Eqrel (erel:=fun (C1 C2:conf (state_space_G G)) => erel (sim_rel k n) (init_econf X C1) (init_econf X C2))).
by move=>*; apply: erel_refl.
by move=>*; apply: erel_sym.
by move=>x y z H K; apply: (erel_trans H K).
Defined.
The number R_n in the paper
Definition R (k n : nat) := card (quotient (equiv k n)).
Definition evolution_to_coal (k n : nat) (C : conf (state_space_G G)) :=
evolution_seq J (coal k n.+1 (init_econf X C)) C.
Definition setACP (k n : nat) (C : conf (state_space_G G)) : pred (conf (state_space_G G)) :=
(evolution_to_coal k n C).
Definition setAC (k n : nat) (C : conf (state_space_G G)) : finType := sub_finType (setACP k n C).
Definition union: forall (d:finType) (d':eqType) (f:d -> pred d'), pred d' :=
fun d d' f x => has (fun i => f i x) (enum d).
Definition max(d: finType) (f: d -> nat) : nat :=
foldr (fun x mx => if (f x) > mx then (f x) else mx) 0 (enum d).
The number A_n in the paper
Definition A (k n : nat) := max (fun C=> card (setACP k n C)).
Lemma card_AC_A: forall k n C, card (setAC k n C) <= A k n.
Proof.
move=>k n C; rewrite /A /setAC card_sub_fin.
apply (max_upper (fun C=>card (setACP k n C))).
Qed.
Lemma evolution_ACP: forall k n m C, m < coal k n.+1 (init_econf X C) -> setACP k n C (evolution J m C).
Proof.
by move=>k n m C lt;
rewrite /setACP /evolution_to_coal (evolution_sub _ _ _ lt) // mem_sub // size_evolution_seq.
Qed.
Lemma card_obs: (card obs) <= (exp (card P) (card P)).
Proof. rewrite -card_finFun /obs
/ieqrelFin cardA /= /ieqrel_enum size_maps -cardA card_sub_fin
/ieqrel_pred;apply: max_card.
Qed.
Lemma card_prod_fin: forall d1 d2:finType, card {d1 * d2 :as finType} = card d1 * card d2.
Proof. by move=>d1 d2; apply: card_prod. Qed.
Lemma coalSn_bound: forall k n C,
coal k n.+1 (init_econf _ C) < k
-> coal k n.+1 (init_econf _ C) <= (A k n)*(exp (card P) (card P)).
Proof.
move=>k n C H.
case: (ltnP ((A k n)*(exp (card P) (card P))) (coal k n.+1 (init_econf _ C)) )=>//[L].
set f: (ordinal (coal k n.+1 (init_econf X C))) -> {(setAC k n C) * obs :as finType} :=
fun i=> ( @EqSig _ (setACP k n C) (evolution J i C) (evolution_ACP (ltn_ord i))
, obs_abst (eevolution J i (init_econf X C))).
have crd1: card {(setAC k n C) * obs :as finType} <= A k n * exp (card P) (card P).
rewrite card_prod_fin.
apply: leq_mul; (apply: card_AC_A || apply card_obs).
have crd: card {(setAC k n C) * obs :as finType} < card (ordinal_finType (coal k n.+1 (init_econf X C))).
by rewrite card_ordinal; apply: (leq_trans _ L); apply: crd1.
elim: (pigeon f crd)=>[[i i_mem] [[j j_mem] W]]; clear crd1 crd L.
elim: (andP W)=>[W1 W2].
case: (eqP W2) =>[E1 E2].
have F: negb ((Ordinal i_mem) == (Ordinal j_mem) :> nat) by done.
rewrite /= in F; clear W W1 W2.
case: (leqP i j)=>[leq|gt].
rewrite leq_eqVlt in leq.
case: (orP leq)=>[eq|lt]; first by rewrite -(negbET F).
have sum: j = i + (j - i) by rewrite (subnK (ltnW lt)).
set E:=eevolution J i (init_econf X C).
have E12: eevolution J (j-i) E == E.
by apply: econf_det;
(rewrite /E eevolution_sum addnC -sum !econf_conf_eevolution econf_conf_init_econf E1 eq_refl
|| rewrite /E eevolution_sum addnC -sum E2 eq_refl).
have coalSn: coal k n.+1 (init_econf X C) <= i.
apply: coal_bound=>[m l|]=>//.
rewrite -(subnK l) addnC -eevolution_sum.
apply: (measure_loop _ E12) =>//.
by rewrite ltn_0sub.
rewrite -(ltnn (coal k n.+1 (init_econf X C))).
by apply: (leq_trans _ i_mem).
have sum: i = j + (i - j) by rewrite (subnK (ltnW gt)).
set E:=eevolution J j (init_econf X C).
have E12: eevolution J (i-j) E == E.
by apply: econf_det;
(rewrite /E eevolution_sum addnC -sum !econf_conf_eevolution econf_conf_init_econf E1 eq_refl
|| rewrite /E eevolution_sum addnC -sum E2 eq_refl).
have coalSn: coal k n.+1 (init_econf X C) <= j.
apply: coal_bound=>[m l|]=>//.
rewrite -(subnK l) addnC -eevolution_sum.
apply: (measure_loop _ E12) =>//.
by rewrite ltn_0sub.
rewrite -(ltnn (coal k n.+1 (init_econf X C))).
by apply: (leq_trans _ j_mem).
Qed.
Lemma coalSn_strictbound: forall k n C,
(if (coal k n.+1 (init_econf _ C)) < k then S (coal k n.+1 (init_econf _ C)) else 0)
< ((A k n)*(exp (card P) (card P))).+1.+1.
Proof.
move=>k n C.
case: (leqP k (coal k n.+1 (init_econf _ C)))=>//[H].
by rewrite !ltnS; apply: coalSn_bound.
Qed.
The next two lemmas are Lemma 14 in the paper
Lemma R0_bound: forall k, R k 0 <= (card Q) * (exp (card P) (card P)).
move=>k.
set f: (conf (state_space_G G)) -> {Q * obs :as finType} :=
fun C=> (C.1, observe C.2).
have leq: card {Q * obs :as finType} <= (card Q) * (exp (card P) (card P)).
by rewrite card_prod_fin; apply leq_mul; (apply leqnn || apply card_obs).
apply: (leq_trans _ leq).
apply: (card_quotient (f:=f))=>[C1 C2 e].
have E: f C1 == f C2 by rewrite e eq_refl. clear e.
rewrite /f in E.
case: C1 E =>[q1 rho1 E]; case: C2 E =>/=[q2 rho2 E]; case/andP: E=>/=[E1 E2].
apply/eqP; apply: fgraph_of_fun_congr. move=>[i i_mem] /=.
elim: i i_mem=>//=[_].
rewrite (eqP E1) /coalE !coal0; (try apply: measure_init).
by rewrite /eqdQX /init_econf /piQ /piX /= eq_refl andTb;
apply: init_factors.
Qed.
Lemma RSn_bound: forall k n, R k n.+1 <= (R k n) * ((A k n * exp (card P) (card P)).+2) * (exp (card P) (card P)).
move=>k n.
rewrite /R.
set f: (conf (state_space_G G)) -> {{(quotient (equiv k n)) * (ordinal (( A k n * exp (card P) (card P)).+2)) :as finType} * obs :as finType}:=
fun C => ((eqclass (equiv k n) C, Ordinal (coalSn_strictbound k n C))
, observe (piS (coalE k n.+1 (init_econf X C)))).
have crd: card {{(quotient (equiv k n)) * (ordinal (( A k n * exp (card P) (card P)).+2)) :as finType} * obs :as finType}
<= (R k n) * ((A k n * exp (card P) ((card P))).+2) * (exp (card P) (card P)).
rewrite !card_prod_fin /R card_ordinal;
apply leq_mul; (apply: leqnn || apply: card_obs).
apply: (leq_trans _ crd); clear crd.
apply (card_quotient (r:=equiv k n.+1) (f:=f)).
move=>C1 C2 ef.
have e1: erel (equiv k n) C1 C2.
have t: (f C1).1.1 == (f C2).1.1 by rewrite ef eq_refl.
rewrite /f /= in t.
by apply: (@eq_eqclass _ (equiv k n) _ _ t).
have e2: (if (coal k n.+1 (init_econf _ C1)) < k then S (coal k n.+1 (init_econf _ C1)) else 0)
= (if (coal k n.+1 (init_econf _ C2)) < k then S (coal k n.+1 (init_econf _ C2)) else 0).
have t: (f C1).1.2 = (f C2).1.2 :> nat by rewrite ef. by rewrite /f /= in t.
have e3: observe (piS (coalE k n.+1 (init_econf X C1))) = observe (piS (coalE k n.+1 (init_econf X C2))).
have t: (f C1).2 = (f C2).2 by rewrite ef. by rewrite /f /= in t.
clear f ef.
apply: decomp_sim=>//.
apply/eqP.
case: (leqP k (coal k n.+1 (init_econf X C1)))=>[l1|g1];
case: (leqP k (coal k n.+1 (init_econf X C2)))=>[l2|g2].
have k1: coal k n.+1 (init_econf X C1) == k by rewrite eqn_leq l1 andbT coal_triv_bound.
have k2: coal k n.+1 (init_econf X C2) == k by rewrite eqn_leq l2 andbT coal_triv_bound.
by rewrite (eqP k1) (eqP k2).
by rewrite leqNgt in l1; rewrite (negbET l1) g2 in e2.
by rewrite leqNgt in l2; rewrite (negbET l2) g1 in e2.
by rewrite g1 g2 in e2; case: e2.
Qed.
Definition make_moves(rho:state_space_G G)(alpha: seq moveData) : state_space_G G :=
foldr (fun m rho' => make_move rho' m) rho alpha.
Lemma make_moves_adds: forall rho m alpha,
make_moves rho (Adds m alpha) = make_move (make_moves rho alpha) m.
Proof. done. Qed.
Fixpoint iterate_make_moves(rho:state_space_G G)(ms: seq moveData)(k:nat) {struct k} : state_space_G G:=
match k with
| 0 => rho
| S k' => make_moves (iterate_make_moves rho ms k') ms
end.
Lemma make_moves_iterate_make_moves: forall rho alpha k,
make_moves (iterate_make_moves rho alpha k) alpha = (iterate_make_moves (make_moves rho alpha) alpha k).
Proof. by move=>rho alpha; elim=>//=[k ->]. Qed.
Lemma iterate_make_moves_sum: forall rho alpha (i j:nat),
iterate_make_moves (iterate_make_moves rho alpha i) alpha j = iterate_make_moves rho alpha (i + j).
Proof.
move=>rho alpha i j. elim: i=>//[i IH]. by rewrite addSn /= -IH -make_moves_iterate_make_moves.
Qed.
Lemma make_moves_act: forall alpha x, {dy : _ | forall rho, (make_moves rho alpha) x = act _ (rho dy.2) dy.1}.
move=>alpha.
elim: alpha=>[x|m alpha' IH x].
exists (unit (edgegroup G), x)=>rho. by rewrite /= act_unitP.
case: m=>[z n|z z'].
elim: (IH x) => [[d y] H].
case U: (z == x).
exists (mul d (edge_of_nat _ n), y)=>rho.
by rewrite make_moves_adds /make_move /state_space_G /state_space_G_action fgraph_fun_eq;
rewrite U (eqP U) H act_mulP.
exists (d, y)=>rho.
rewrite make_moves_adds /make_move /state_space_G /state_space_G_action fgraph_fun_eq.
by rewrite U H.
case U: (x == z).
elim: (IH z') => [[d y] H].
exists (d, y)=>rho.
rewrite make_moves_adds /make_move /state_space_G /state_space_G_action fgraph_fun_eq.
by rewrite U.
elim: (IH x) => [[d y] H].
exists (d, y)=>rho.
rewrite make_moves_adds /make_move /state_space_G /state_space_G_action fgraph_fun_eq.
by rewrite U.
Qed.
Lemma iterate_make_moves_act: forall alpha x i,
{ dy:_ | forall rho, iterate_make_moves rho alpha i x = act _ (rho dy.2) dy.1}.
Proof.
move=>alpha x i. move: x.
elim:i=>[x|i IH x].
exists (unit (edgegroup G), x)=>rho. by rewrite /= act_unitP.
elim: (IH x)=>[[d y] /=H].
elim: (make_moves_act alpha y)=>[[e z] /=K].
exists (mul e d, z) =>rho/=.
by rewrite make_moves_iterate_make_moves H K act_mulP.
Qed.
Lemma iterate_make_moves_act_twice: forall alpha x, exists y, exists i, exists j,
exists di, exists dj,
forall rho,
and4 (i < j) (j <= card P)
(iterate_make_moves rho alpha i x == act _ (rho y) di)
(iterate_make_moves rho alpha j x == act _ (rho y) dj).
Proof.
move=>alpha x.
set f: (ordinal (card P).+1) -> P :=
fun ord => (proj1_sig (iterate_make_moves_act alpha x ord)).2.
have c: card P < card (ordinal_finType (card P).+1).
by rewrite card_ordinal ltnS leqnn.
elim (pigeon f c)=>[[i imem] [[j jmem] /=H]]; move/andP: H=>[H1 H2].
rewrite eqE /= in H1; rewrite /f /= in H2.
move: (proj2_sig (iterate_make_moves_act alpha x i))=>/= K1.
move: (proj2_sig (iterate_make_moves_act alpha x j))=>/= K2.
exists ((proj1_sig (iterate_make_moves_act alpha x i)).2).
case: (leqP i j)=>[leq|gt].
have lt: i < j by rewrite ltn_neqAle leq H1.
exists i; exists j;
exists ((proj1_sig (iterate_make_moves_act alpha x i)).1);
exists ((proj1_sig (iterate_make_moves_act alpha x j)).1)=>rho.
split=>//.
by apply/eqP.
by pattern ((proj1_sig (iterate_make_moves_act alpha x i))).2; rewrite (eqP H2); apply/eqP.
exists j; exists i;
exists (proj1_sig (iterate_make_moves_act alpha x j)).1;
exists (proj1_sig (iterate_make_moves_act alpha x i)).1=>rho.
split=>//.
by pattern ((proj1_sig (iterate_make_moves_act alpha x i))).2; rewrite (eqP H2); apply/eqP.
by apply/eqP.
Qed.
Lemma iterate_make_moves_repeat_singlepebble: forall (rho:state_space_G G) alpha x,
exists k, exists d,
(0 < k) /\ (k <= card P) /\
forall n, (card P <= n) ->
(iterate_make_moves rho alpha (n+k) x == act _ (iterate_make_moves rho alpha n x) d).
Proof.
move=>rho alpha x.
elim: (iterate_make_moves_act_twice alpha x)=>[y [i [j [di [dj K]]]]].
exists (j-i); exists (mul (inv di) dj).
split; first by move:(K rho)=>[K1 _]; rewrite ltn_0sub.
split; first by move:(K rho)=>[_ K2 _ _]; apply: (leq_trans _ K2); apply: leq_subr.
move=>n H.
move: (K (iterate_make_moves rho alpha (n-i)))=>[K1 K2 K3 K4]; clear K.
have LEin: i <= n by apply: (leq_trans (ltnW K1) _); apply: (leq_trans K2 _).
rewrite !iterate_make_moves_sum in K3 K4.
rewrite addnC subnK // in K3.
rewrite -act_mulP (eqP K3) !act_mulP mulP invrP unitlP -(eqP K4).
have E: n-i+j = n+(j-i).
by rewrite -{2}(@subnK i n) // [i+(n-i)]addnC -addnA subnK //; apply: ltnW.
by rewrite E eq_refl.
Qed.
Lemma iterate_make_moves_repeat_allpebbles: forall (rho:state_space_G G) alpha x,
exists d,
forall n, card P <= n ->
(iterate_make_moves rho alpha (n+(fact (card P))) x
== act _ (iterate_make_moves rho alpha n x) d).
Proof.
move=>rho alpha x.
move: (iterate_make_moves_repeat_singlepebble rho alpha x)=>[k [d [H1 [H2 H3]]]].
have K: forall m, exists d, forall n, card P <= n ->
iterate_make_moves rho alpha (n + m*k) x == act _ (iterate_make_moves rho alpha n x) d.
elim=>[|m [d' IH]]/=.
by exists (unit (edgegroup G))=>n H; rewrite addn0 act_unitP eq_refl.
exists (mul d' d)=>n H.
have L: card P <= n + m*k by apply: (leq_trans H _); apply: leq_addr.
by rewrite mulSn [k+m*k]addnC addnA (eqP (H3 (n+m*k) L)) (eqP (IH n H)) act_mulP eq_refl.
move: (K (multiply (k+1) (card P-k) * multiply 1 (k-1)))=>[dx Kx].
exists dx=>n H.
by rewrite (fact_middle H1 H2) mulnC mulnA (eqP (Kx n H)) eq_refl.
Qed.
Lemma 15 in the paper
Lemma iterate_make_moves_repeat: forall (rho:state_space_G G) alpha,
(iterate_make_moves rho alpha (card P + eg_order G * fact (card P))
== iterate_make_moves rho alpha (card P)).
Proof.
move=>rho alpha.
apply: eq_finfun=>x.
move: (iterate_make_moves_repeat_allpebbles rho alpha x)=>[d K].
have L: forall m, iterate_make_moves rho alpha (card P + m*(fact (card P))) x
= act _ (iterate_make_moves rho alpha (card P) x) (iter m (mul d) (unit (edgegroup G))).
elim=>[|m IH]/=.
by rewrite addn0 act_unitP.
rewrite mulSn [fact _ +_]addnC addnA (eqP (K _ _)); last by apply: leq_addr.
rewrite IH act_mulP.
have H: forall n, mul (iter n (mul d) (unit (edgegroup G))) d
= mul d (iter n (mul d) (unit (edgegroup G))).
elim=>/=[|n IIH]; first by rewrite unitlP unitrP.
by rewrite -mulP IIH.
by rewrite H.
have M: (iterate_make_moves rho alpha (card P) x)
= act _ (iterate_make_moves rho alpha (card P) x) (iter (eg_order G) (mul d) (unit (edgegroup G))).
by rewrite (@eg_orderP G) act_unitP.
by rewrite M; apply: L.
Qed.
Lemma coal_init_econf: forall k n E, coal k n E <= coal k n (init_econf X (econf_conf E)).
Proof.
move=>k n E.
case: (leqP (coal k n E) (coal k n (init_econf X (econf_conf E))))=>//[H].
have K: measure (coalE k n (init_econf X (econf_conf E))) <= card P - n.
by apply: measure_eevolution_coal; apply: (leq_trans H _); apply: coal_triv_bound.
have L: card P - n <measure (eevolution J (coal k n (init_econf X (econf_conf E))) E).
by apply: (@before_measure k n).
have M: measure (coalE k n (init_econf X (econf_conf E))) <
measure (eevolution J (coal k n (init_econf X (econf_conf E))) E)
by apply: (leq_trans _ L).
by rewrite ltnNge /coalE measure_init in M.
Qed.
The next two lemmas are Lemma 12 in the paper
Lemma eqdQX_eevolution: forall k n E1 E2 m,
sim k n E1 E2 -> m < coal k n.+1 E1 -> m < coal k n.+1 E2 ->
eqdQX (eevolution J m E1) (eevolution J m E2).
Proof.
move=>k n E1 E2 m.
elim:n=>[s l1 l2|n IH s l1 l2].
move/andP: (iforallP s (Ordinal (ltn0Sn 0)))=>/=[s1 s2].
apply: (coal_eqQX_before (m:=m) (eqP s1))=>//.
by rewrite coal0 leq0n.
move/andP: (iforallP s (Ordinal (ltnSn n.+1)))=>/=[s1 s2].
case: (leqP (coal k n.+1 E1) m)=>[leq|gt].
by apply: (coal_eqQX_before (m:=m) (eqP s1))=>//.
apply: IH=>//.
by apply/iforallP=>i; move:i => [i im]; apply: (iforallP s (Ordinal (leqW im))).
by rewrite -(eqP s1).
Qed.
Definition eqdQobs(E1 E2 : econf X) :=
(piQ E1 == piQ E2) && (observe (piS E1) == observe (piS E2)).
Lemma eqdQobs_eevolution: forall k n E1 E2 m,
sim k n E1 E2 -> m < coal k n.+1 E1 -> m < coal k n.+1 E2 ->
eqdQobs (eevolution J m E1) (eevolution J m E2).
Proof.
move=>k n E1 E2 m H l1 l2.
move/andP:(eqdQX_eevolution H l1 l2)=>[L1 L2].
apply/andP; split=>//.
apply: (obs_rel (xi:=piX (eevolution J m E1))).
apply: real_econf.
rewrite (eqP L2); apply real_econf.
Qed.
Lemma eevolution_seq_cat: forall m n (E:econf X),
eevolution_seq J (m+n) E = cat (eevolution_seq J m E) (eevolution_seq J n (eevolution J m E)).
Proof. by move=>m n; elim:m=>//[m IH E]/=; rewrite IH eevolution_step. Qed.
Lemma coal_shift: forall k n E m, coal (m+k) n E <= m + coal k n (eevolution J m E).
Proof.
move=>k n E m.
rewrite /coal eevolution_seq_cat find_cat.
case: (has).
apply: (leq_trans (find_size _ _) _).
by rewrite size_eevolution_seq; apply: leq_addr.
by rewrite size_eevolution_seq; apply: leqnn.
Qed.
Lemma coal_mon1: forall k1 k2 n E, k1 <= k2 -> coal k1 n E <= coal k2 n E.
Proof.
move=>k1 k2 n E H.
rewrite /coal -(subnK H) eevolution_seq_cat find_cat.
case: (has).
by apply: leqnn.
by apply: (leq_trans (find_size _ _) _); apply: leq_addr.
Qed.
Lemma repeatQobs: forall k n E m,
erel (equiv k n) (econf_conf E) (econf_conf (eevolution J m E) )->
forall l, m + l < coal k n.+1 E-> eqdQobs (eevolution J l E) (eevolution J (m+l) E).
Proof.
move=>k n E m /=H.
move=>l K.
have l1: l < coal k n.+1 (init_econf X (econf_conf E)).
apply: (leq_trans _ (coal_init_econf k n.+1 _)).
rewrite -(leq_add2l m) addnS.
by apply: (leq_trans _ (leq_addl _ _)).
have l2: l < coal k n.+1 (init_econf X (econf_conf (eevolution J m E))).
case: (leqP m k)=>[leq|gt].
apply: (leq_trans _ (@coal_mon1 (k-m) _ _ _ _)).
rewrite -(leq_add2l m) addnS.
have l3: m + l < coal (m + (k-m)) n.+1 E by rewrite (subnK leq).
apply: (leq_trans l3 _).
apply: (leq_trans (@coal_shift (k-m) n.+1 E m) _).
rewrite (leq_add2l m).
apply: coal_init_econf.
by rewrite leq_sub_add; apply leq_addl.
have l3: k < k.
apply: (leq_trans gt _).
apply: (leq_trans (leq_addr l m) _).
apply: (leq_trans _ (coal_triv_bound k n.+1 E)).
by apply: ltnW.
by rewrite ltnn in l3.
rewrite addnC -eevolution_sum.
move: (eqdQobs_eevolution H l1 l2).
by rewrite /eqdQobs /piQ /piS !econf_conf_eevolution !econf_conf_init_econf.
Qed.
Lemma repeatQobs_mult: forall k n E m l r,
l*m + r < coal k n.+1 E ->
erel (equiv k n) (econf_conf E) (econf_conf (eevolution J m E) )->
eqdQobs (eevolution J r E) (eevolution J (l*m + r) E).
Proof.
move=>k n E m.
elim=>/=[r H K|l IH r H K]/=.
by rewrite add0n /eqdQobs !eq_refl.
have leq: l*m + r < coal k n.+1 E.
apply: (leq_trans _ H). rewrite ltnS leq_add2r mulSn. apply leq_addl.
rewrite -addnA in H.
move/andP:(repeatQobs K H)=>[H1 H2].
move/andP:(IH r leq K)=>[K1 K2].
rewrite !addnA in H1 H2 K1 K2.
by rewrite /eqdQobs -(eqP H1) -(eqP H2) -(eqP K1) -(eqP K2) !eq_refl.
Qed.
Definition make_moves_from(E : econf X) (n:nat) :=
rev (maps (fun E=>jag_move J (piQ E) (observe (piS E)))
(eevolution_seq J n E)).
Lemma make_moves_from_step: forall E n, make_moves (piS E) (make_moves_from E n.+1)
= make_moves (piS (stepe J E)) (make_moves_from (stepe J E) n).
Proof.
move=>E n.
rewrite /make_moves stepe_S.
by rewrite -!foldl_rev /make_moves_from !revK /=.
Qed.
Lemma eevolution_make_moves_from: forall E m,
piS (eevolution J m E) = make_moves (piS E) (make_moves_from E m).
Proof.
move=>E m.
elim: m E=>//[m IH E].
by rewrite make_moves_from_step -IH eevolution_step.
Qed.
Lemma eq_make_moves_from: forall n E1 E2,
(forall m, m < n -> (eqdQobs (eevolution J m E1) (eevolution J m E2))) ->
(make_moves_from E1 n) = (make_moves_from E2 n).
Proof.
elim=>//[n IH E1 E2 H].
rewrite /make_moves_from /= !rev_adds.
rewrite /make_moves_from /= in IH.
rewrite (IH (stepe J E1) (stepe J E2)).
move/andP:(H 0 (ltn0Sn n))=>/=[H1 H2].
by rewrite (eqP H1) (eqP H2).
move=>m L.
rewrite !eevolution_step.
apply: (H m.+1).
by rewrite ltnS.
Qed.
Lemma eq_make_moves_from_mult: forall k n E m l,
(l.+1)*m < coal k n.+1 E ->
erel (equiv k n) (econf_conf E) (econf_conf (eevolution J m E))->
make_moves_from E m = make_moves_from (eevolution J (l*m) E) m.
Proof.
move=>k n E m l H K.
case: l H K=>//[l H K].
apply: eq_make_moves_from=>[r rl].
rewrite eevolution_sum addnC.
apply: (@repeatQobs_mult k n E m l.+1 r) =>//.
by apply: (leq_trans _ H)=>/=;
rewrite ltnS -addnA leq_add2l addnC leq_add2r; apply ltnW.
Qed.
Lemma eevolution_make_moves_from_mult: forall k n E m l,
erel (equiv k n) (econf_conf E) (econf_conf (eevolution J l E) )->
m*l < coal k n.+1 E ->
piS (eevolution J (m*l) E) =
iterate_make_moves (piS E) (make_moves_from E l) m.
Proof.
move=>k n E m l H L.
elim:m H L=>[| m IH H L]//=.
rewrite -IH =>//.
rewrite (@eq_make_moves_from_mult k n E l m L H).
rewrite -eevolution_make_moves_from.
by rewrite -eevolution_sum.
apply: (leq_trans _ L)=>/=. rewrite ltnS mulSn. apply leq_addl.
Qed.
Lemma eevolution_repeat: forall k n (E: econf X) m,
(card P + eg_order G * fact (card P))*m < coal k n.+1 E ->
erel (equiv k n) (econf_conf E) (econf_conf (eevolution J m E) ) ->
econf_conf (eevolution J ((card P)*m) E)
= econf_conf (eevolution J ((card P + eg_order G * fact (card P))*m) E).
Proof.
move=>k n E m K H.
have K': card P * m < coal k n.+1 E
by rewrite muln_addl in K; apply: (leq_trans _ K);
rewrite ltnS; apply: leq_addr.
have eQ: piQ (eevolution J ((card P)*m) E)
= piQ (eevolution J ((card P + eg_order G * fact (card P))*m) E).
rewrite -[_*m] addn0 in K; rewrite -[_*m] addn0 in K'.
rewrite /piQ -[card P * m]addn0.
move/andP: (@repeatQobs_mult k n E m (card P) 0 K' H)=>/=[H1 _].
move/andP: (@repeatQobs_mult k n E m _ 0 K H)=>/=[H2 _].
rewrite /piQ !addn0 in H1 H2.
by rewrite addn0 -(eqP H1) -(eqP H2).
have eA: piS (eevolution J ((card P)*m) E)
= piS (eevolution J ((card P + eg_order G * fact (card P))*m) E).
rewrite !(eevolution_make_moves_from_mult H) //.
symmetry; apply/eqP.
by apply: iterate_make_moves_repeat.
by apply/pair_eqP; rewrite /pair_eq /=; apply/andP; split; apply/eqP.
Qed.
Lemma repeat_add: forall k (C:conf (state_space_G G)) m i j,
(evolution J k C = evolution J (k+m) C) ->
(evolution J (k+i*m+j) C = evolution J (k+j) C).
Proof.
move=>k C m i j H.
have H': forall j, (evolution J (k+j) C = evolution J (k+m+j) C).
elim=>//=[|l IH].
by rewrite !addn0.
by rewrite -addn1 !addnA addnC -evolution_sum IH evolution_sum addnC.
elim: i j =>//=[|i IH j].
by rewrite addn0.
by rewrite mulSn [m+i*m]addnC addnA -addnA IH addnA -H'.
Qed.
Lemma evolution_step: forall m (C:conf (state_space_G G)),
evolution J m (next J C) = evolution J m.+1 C.
Proof. by move=>m C; elim: m =>//=[m ->]. Qed.
Lemma evolution_seq_cat: forall m n (C:conf (state_space_G G)),
evolution_seq J (m+n) C = cat (evolution_seq J m C) (evolution_seq J n (evolution J m C)).
Proof. by move=>m n; elim:m=>//[m IH C]/=; rewrite IH evolution_step. Qed.
Lemma evolution_seq_repeat_subset: forall k (C:conf (state_space_G G)) m n,
(0 < m) ->
(evolution J k C = evolution J (k+m) C) ->
subset (evolution_seq J n C) (evolution_seq J (k+m) C).
Proof.
move=>k C m n mgt0 H.
apply/subsetP=>x K.
case: (leqP n (k+m))=>[leq|gt].
by rewrite -(subnK leq) evolution_seq_cat mem_cat; apply/orP; left.
rewrite -index_mem size_evolution_seq.
case: (leqP (k+m) (index x (evolution_seq J (k+m) C)))=>//[U].
have l0: k + m <= index x (evolution_seq J n C).
rewrite -(subnK (ltnW gt)) evolution_seq_cat index_cat.
case: (mem (evolution_seq J (k + m) C) x)=>//.
apply: (leq_trans U _). apply: (leq_trans (index_size _ _) _). apply: leq_addr.
have l1: k <= index x (evolution_seq J n C) by apply: (leq_trans _ l0); apply: leq_addr.
elim: (div_mod_exists (index x (evolution_seq J n C) - k) mgt0)=>[q [r e]]; move/andP: e =>[e1 e2].
rewrite -(eqn_addl k) (subnK) // addnA in e1.
have l3: k+r < index x (evolution_seq J (k+m) C).
by apply: (leq_trans _ U); rewrite addnC -addSn addnC leq_add2l.
have l4: k + r < k + m by rewrite addnC -addSn addnC leq_add2l.
move: (before_find C l3)=>L.
rewrite -index_mem size_evolution_seq in K.
rewrite -evolution_sub // -(@repeat_add k C m q r) // -(eqP e1) in L.
rewrite (evolution_sub J X C K) sub_index ?eq_refl // in L.
by rewrite -index_mem size_evolution_seq.
Qed.
Lemma 17 in the paper
Lemma An_bound: forall k n, A k n <= (1 + card P + eg_order G * fact (card P)) * R k n.
Proof.
move=>k n.
rewrite /A.
apply max_lower=>C.
rewrite /setACP /evolution_to_coal.
case: (leqP (((1 + card P + eg_order G * fact (card P)) * R k n).+1) (coal k n.+1 (init_econf X C)))=>[leq|gt].
set f: nat -> quotient (equiv k n) :=
fun i => eqclass _ (evolution J i C).
have cf: card (quotient (equiv k n)) < S (R k n) by rewrite /R; apply: ltnSn.
move: (pigeon_nat f cf)=>[i [j H]].
move/andP: H =>[H12 H3']. move/andP: H12 =>[H1 H2]. rewrite /f in H3'. move: (eq_eqclass H3')=>H3; clear H3'.
rewrite -(subnK (ltnW H1)) addnC -evolution_sum in H3.
move: (@eevolution_repeat k n (eevolution J i (init_econf X C)) (j-i))=>T.
rewrite !econf_conf_eevolution !econf_conf_init_econf in T.
have T0: (card P + eg_order G * fact (card P)) * (j-i) <= (card P + eg_order G * fact (card P)) * (R k n).
rewrite leq_mul2l. apply/orP; right. rewrite ltnS in H2. apply: (leq_trans _ H2).
rewrite leq_sub_add. apply: leq_addl.
have T1: (card P + eg_order G * fact (card P)) * (j-i) < coal k n.+1 (eevolution J i (init_econf X C)).
rewrite -(leq_add2l 1) !add1n in T0. apply: (leq_trans T0 _).
move: (coal_shift k n.+1 (init_econf X C) i)=>T2.
rewrite -leq_sub_add in T2.
apply: (leq_trans _ T2).
move: (@coal_mon1 k (i+k) n.+1 (init_econf X C) (leq_addl i k))=>T3.
apply: (leq_trans _ (leq_sub2r i T3)).
rewrite -addnA muln_addl mul1n in leq.
rewrite -(leq_add2l (R k n)) addnS.
apply: (leq_trans leq _).
rewrite -leq_sub_add.
apply: leq_sub2l.
rewrite ltnS in H2. apply: (leq_trans _ H2). by apply: ltnW.
move: (T T1 H3)=>K; clear T T1.
rewrite muln_addl in K.
have T2: 0 < eg_order G * fact (card P) * (j - i).
rewrite ltn_neqAle leq0n eq_sym !eqn_mul0 andbT.
apply/norP; split. apply/norP; split.
rewrite -leqn0 -ltnNge. apply (eg_order_positive G).
rewrite -leqn0 -ltnNge. apply: fact_positive.
rewrite -leqn0 -ltnNge. by rewrite -ltn_0sub in H1.
move: (subset_leq_card (evolution_seq_repeat_subset (coal k n.+1 (init_econf X C)-i) T2 K)) => L.
have T1: coal k n.+1 (init_econf X C) = i + (coal k n.+1 (init_econf X C) - i).
rewrite subnK //.
apply: (leq_trans _ leq). rewrite !muln_addl mul1n. apply: leqW.
do 2 apply: (leq_trans _ (leq_addr _ _)). rewrite ltnS in H2. apply: leq_trans _ H2. by apply: ltnW.
rewrite T1 evolution_seq_cat.
apply: (leq_trans (card_cat _ _) _).
rewrite -addnA muln_addl mul1n.
apply: leq_add.
apply: (leq_trans (card_size _ ) _). rewrite size_evolution_seq. rewrite ltnS in H2. apply: leq_trans _ H2. by apply: ltnW.
apply: leq_trans L _.
apply: leq_trans (card_size _) _.
by rewrite size_evolution_seq -muln_addl.
apply: leq_trans (card_size _) _.
rewrite size_evolution_seq.
by rewrite ltnS in gt.
Qed.
Now we come to the proof of the main result, Proposition 3
We exclude trivial cases:
Variable mgt1: 1 < eg_order G.
Variable cardQgt0: 0 < card Q.
Variable cardPgt1: 1 < card P.
Notation "x ** y" := (exp x y) (at level 30).
The next lemmas are straightforward (though tedious) arithmetic
calculations to establish upper bounds by induction. It should be
possible to shorthen the proofs.
Lemma size_bound_An: forall a x n q p c,
(1 < n) -> (1 <= q) -> (1 < p) ->
(x <= (n * q) ** c) ->
a <= (1 + p + n * (fact p))*x ->
a <= (n * q) ** (4 + p*p + c).
Proof.
move=>a x n q p c qgt1 nge1 ngt1 H K.
apply: (leq_trans K _).
have nqgt1: 1 < n * q.
rewrite -(muln1 2). apply leq_mul=>//.
have H1: n*(fact p) <= n * q * (p ** p).
rewrite -mulnA leq_mul2l.
apply/orP; right.
rewrite -(mul1n (fact p)).
apply: leq_mul =>//.
apply: fact_exp.
have H2: p <= n * q * (p ** p).
rewrite -{1}(mul1n p); apply leq_mul =>//.
by apply ltnW.
by apply leqnexp.
have H3: 1 <= n * q * (p ** p).
rewrite -(mul1n 1). apply leq_mul =>//.
by apply ltnW.
apply exp_positive.
by apply ltnW.
have H4: (1 + p + n * fact p) <= 3 * (n * q * (p ** p)).
rewrite -addnA mulSn mulSn mul1n.
apply: leq_add =>//.
apply: leq_add =>//.
have H5: (1 + p + n * fact p)*x <= 3 * (n * q * (p ** p))*x.
by rewrite leq_mul2r; apply/orP; right.
apply: (leq_trans H5 _).
have H6: 3 <= (n*q) ** 3 by apply leqnexp.
have H7: p**p <= (n*q) ** (p*p).
rewrite -exp_exp; apply: leq_exp2r.
by apply: leqnexp.
have H8: 3 * (n * q * (p ** p))*x <= ((n*q) ** 3) * (n*q) * ((n*q) ** (p*p) * x).
rewrite -!(mulnA 3) -!(mulnA ((n*q)**3)).
apply: leq_mul=>//.
rewrite -!mulnA.
apply: leq_mul=>//.
apply: leq_mul=>//.
apply: leq_mul=>//.
apply: (leq_trans H8 _).
rewrite -{2}(expn1 (n*q)) mulnA -!exp_plus addn1.
have H9: (n*q) ** (4 + p*p) *x <= (n*q) ** (4+ p*p + c).
rewrite (exp_plus _ (4+p*p)).
apply: leq_mul=>//.
apply: (leq_trans H9 _).
apply: leqnn.
Qed.
Lemma size_bound_R0: forall r n q p,
(1 < n) -> (1 <= q) -> (1 < p) ->
r <= q * p**p ->
r <= (n*q)**(6 + 3*p*p).
Proof.
move=>r n q p ngt1 qgt0 pgt1 H.
have nqgt1: 1 < n * q.
rewrite -(muln1 2). apply leq_mul=>//.
apply: leq_trans H _.
have H1: p**p <= (n*q) ** (p*p).
rewrite -exp_exp; apply: leq_exp2r.
by apply: leqnexp.
have H2: q <= (n*q) ** 1.
rewrite /= muln1.
rewrite -{1}(mul1n q).
apply: leq_mul.
by apply: ltnW.
by apply: leqnn.
have H3: q * (p ** p) <= (n*q) ** (1 + p*p).
by rewrite exp_plus; apply: leq_mul.
apply: (leq_trans H3 _).
apply: leq_exp2l=>//. apply: ltnW=>//.
apply: leq_add=>//.
rewrite -{1}(mul1n (p*p)) -mulnA.
apply: leq_mul=>//.
Qed.
Lemma size_bound_RSn: forall r a n q p c,
(1 < n) -> (1 <= q) -> (1 < p) ->
a <= (n*q)**(4 + p*p + c)->
r <= (n*q)**c * (2 + a * (p ** p))* (p**p) ->
r <= (n*q)**(6 + 3*p*p + 2*c).
Proof.
move=>r a n q p c ngt1 qge1 pgt1 H K.
have nqgt1: 1 < n * q.
rewrite -(muln1 2). apply leq_mul=>//.
apply: (leq_trans K _).
have H1: 2 <= (n*q)**(4 + p*p + c) * p**p.
rewrite -{1}(muln1 2).
apply: leq_mul; last by apply: exp_positive; apply: ltnW.
have H11: 2 <= (n*q) ** 1.
by rewrite /= -(muln1 2); apply: leq_mul.
apply: (leq_trans H11 _).
apply: leq_exp2l. by apply: ltnW.
have H12: 0 < 4 by auto.
apply: (leq_trans H12 _).
rewrite -addnA.
apply: leq_addr.
have H2: (2 + a * (p**p)) <= 2 * ((n*q)**(4 + p*p + c) * p**p).
have H22: (2 + a * (p**p)) <= (n*q)**(4 + p*p + c) * p**p + (n*q)**(4 + p*p + c) * p**p.
apply: leq_add =>//.
apply: leq_mul=>//.
apply: (leq_trans H22 _).
rewrite !mulSn mul0n addn0.
apply: leqnn.
have H3: (n*q)**c * (2 + a * (p**p)) * p**p <= ((n*q) ** c * (2 * ((n*q)**(4 + p*p + c) * p**p))) * p**p.
apply: leq_mul=>//.
apply: leq_mul=>//.
apply: leq_trans H3 _.
rewrite [2*_]mulnC -(mulnA _ _ 2) mulnA -exp_plus.
rewrite [_*2]mulnC mulnA -[_* p**p]mulnA -exp_plus.
have H4: 2 <= (n*q)**2 by apply: leqnexp.
have H5: (p**(p+p)) <= (n*q)**(2*p*p).
have H51: (p**(p+p) <= (n*q)**(p*(p+p))).
rewrite -exp_exp.
apply: leq_exp2r.
by apply: leqnexp.
apply: (leq_trans H51 _).
apply: leq_exp2l. by apply: ltnW.
rewrite !mulSn mul0n addn0 mulnC.
apply: leqnn.
rewrite [2*_]mulnC.
have H6: (n * q) ** (c + (4 + p * p + c)) * 2 * p ** (p + p)
<= (n * q) ** (c + (4 + p * p + c)) * (n*q)**2 * (n*q)**(2*p*p).
apply: leq_mul=>//.
apply: leq_mul=>//.
apply: (leq_trans H6 _).
rewrite -!exp_plus.
apply: leq_exp2l. by apply: ltnW.
clear H1 H2 H4 H5 H6.
rewrite !addnA.
rewrite [_+4]addnC [_+2]addnC !addnA.
have H1: 2+4=6 by auto. rewrite H1; clear H1.
rewrite [_+(p*p)]addnC [_+2*p*p]addnC !addnA.
have H1: 2*p*p + p*p = 3*(p*p).
by rewrite (mulSn 2) -mulnA addnC.
rewrite H1; clear H1.
rewrite [_+c]addnC [_+c]addnC !addnA.
have H1: c+ c = 2*c by rewrite !mulSn mul0n addn0.
rewrite H1; clear H1.
rewrite [6 + _]addnC -(addnA _ 6) [6 + _]addnC addnA [_+c*2]addnC.
rewrite -(mulnA 3 p p) !(mulSn _ (p*p)) !mul0n !addn0.
rewrite !addnA [c*2]mulnC.
apply: leqnn.
Qed.
Definition expbound(n p:nat) := (2**n.+1-1)*(6 + 3*p*p).
Lemma pred_mon: forall n m, m <= n -> m.-1 <= n.-1.
Proof. by move=>x y H; case: y H=>//=[y H]; case: x H=>//=. Qed.
Lemma expboundSn: forall n p, expbound n.+1 p = 6 + 3*p*p + 2*(expbound n p).
Proof.
move=>n p.
rewrite /expbound.
rewrite mulnA.
rewrite muln_subr muln1.
rewrite -{2}(mul1n (6+3*p*p)) -muln_addl.
rewrite add1n -{6}[2]addn1 -subn_sub !subn1.
have H: 0 < (2*2**n.+1).-1.
elim:n=>//[n IH].
have H: (2 * 2**(n.+1)).-1 <= (2 * 2**(n.+1).+1).-1.
apply: pred_mon; apply: leq_mul=>//; apply: leq_exp2l. by apply: ltnW.
apply leqnSn. by apply: leq_trans _ H.
by rewrite (ltn_predK H).
Qed.
Lemma expboundnn: forall n, 0 < n -> expbound n n <= (16 ** 4) ** n.
Proof.
move=>n npos.
rewrite /expbound.
have H1: 2** n.+1 -1 <= 2**n.+1.
rewrite subn1.
case (2** n.+1)=>//=[l].
have H2: 2 ** n.+1 <= 16**n.+1.
by rewrite leq_exp2r.
have H3: 6 <= 16 ** 1 by auto.
have H4: 3*n*n <= (2*n)*(2*n).
rewrite mulnA [_*2]mulnC mulnA.
apply: leq_mul; last by apply: leqnn.
apply: leq_mul=>//.
have H5: (2*n)*(2*n) <= 16**n.
have H51: (2*n)*(2*n) = (2*n)**2 by rewrite /= muln1.
rewrite H51.
have H52: (2*n)**2 <= (2**(2*n))**2.
by apply: leq_exp2r; apply: leqnexp.
apply: leq_trans H52 _.
rewrite exp_exp [_*2]mulnC mulnA -exp_exp.
apply: leqnn.
have H6: (2 ** n.+1 - 1) * (6 + 3 * n * n) <= 16**n.+1 * (16**1 + 16**n).
apply: leq_mul =>//.
apply: leq_trans H1 H2.
apply: leq_add=>//.
apply: leq_trans H4 H5.
apply: leq_trans H6 _.
rewrite muln_addr -!exp_plus.
have H7: 16 ** (n.+1 + 1) <= 16 ** (n.+1 + n).
apply: leq_exp2l. by apply: ltnW.
apply: leq_add=>//; apply: leqnn.
have H8: 16 ** (n.+1 + n) <= 16 ** (3*n).
apply: leq_exp2l. by apply: ltnW.
rewrite !mulSn mul0n addn0 addnA.
apply: leq_add=>//.
rewrite -addn1.
apply: leq_add=>//; apply: leqnn.
have H9: 16 ** (n.+1 + 1) + 16 ** (n.+1 + n) <= 2 * 16 ** (n.+1 + n).
rewrite !mulSn mul0n.
apply: leq_add=>//.
by rewrite addn0; apply: leqnn.
apply: leq_trans H9 _.
have H9: 2 * 16 ** (n.+1 + n) <= 2 * 16**(3*n).
by rewrite leq_mul2l; apply/orP; right.
apply: leq_trans H9 _.
have H9: 2 <= 16 ** 1 by auto.
have H10: 2 <= 16 ** n.
apply: leq_trans H9 _.
apply: leq_exp2l=>//.
have H11 : 16 ** (4*n) = 16 **n * 16 **(3*n).
rewrite -exp_plus.
by rewrite -{2}(muln1 n) [3*_]mulnC -muln_addr [4*n]mulnC.
have H12: 2 * 16 ** (3 * n) <= 16**(4*n).
rewrite H11.
apply: leq_mul=>//.
apply: leq_trans H12 _.
rewrite exp_exp.
apply: leqnn.
Qed.
Lemma Aexpbound: forall k n x,
R k n <= ((eg_order G) * (card Q)) ** x
-> A k n <= ((eg_order G) * (card Q)) ** (4 + (card P)*(card P) + x).
Proof.
move=>k n x H.
apply: (@size_bound_An (A k n) (R k n))=>//.
apply An_bound.
Qed.
Lemma Rexpbound: forall k n,
R k n <= ((eg_order G) * (card Q)) ** (expbound n (card P)).
Proof.
move=>k.
elim=>[|n IH].
rewrite /expbound [2**1 -1]/= [3]lock !mulSn !mul0n !addn0 -lock.
apply: (@size_bound_R0 (R k 0) _ (card Q))=>//.
apply: R0_bound.
rewrite expboundSn.
apply:(@size_bound_RSn (R k n.+1) (A k n) _ (card Q) (card P)).
apply:mgt1. apply:cardQgt0. apply:cardPgt1.
apply: Aexpbound =>//.
apply: leq_trans (RSn_bound k n) _.
apply: leq_mul; last by apply: leqnn.
apply: leq_mul; last by apply: leqnn.
apply: IH.
Qed.
Lemma RPP: forall k, R k (card P) <= ((eg_order G) * (card Q)) ** ((16 ** 4) ** (card P)).
Proof.
move=>k.
have mQgt1: 1 < (eg_order G) * (card Q).
rewrite -(muln1 2). apply leq_mul=>//.
apply: leq_trans (Rexpbound _ _) _.
apply: leq_exp2l=>//. by apply: ltnW.
apply: expboundnn.
apply: ltnW.
apply: cardPgt1.
Qed.
Lemma APP: forall k, A k (card P) <= ((eg_order G) * (card Q)) ** ((16 ** 8) ** (card P)).
Proof.
move=>k.
have mQgt1: 1 < (eg_order G) * (card Q).
rewrite -(muln1 2). apply leq_mul=>//.
apply: leq_trans (@Aexpbound k (card P) ((16 ** 4) ** (card P)) _) _.
apply: RPP.
apply: leq_exp2l=>//. by apply: ltnW.
have H0: 4 <= (16 **4)**1 by auto.
have H1: 4 <= (16 **4)**(card P).
apply: leq_trans H0 _.
apply: leq_exp2l=>//. apply: ltnW; apply: cardPgt1.
have H2: (card P) ** 2 <= (16 ** 2 ** (card P)) ** 2.
apply: leq_exp2r.
by apply: leqnexp.
have H3: (card P) ** 2 <= (16 ** 4) ** (card P).
apply: leq_trans H2 _.
rewrite exp_exp mulnC -exp_exp.
rewrite [((16**2)**2)]exp_exp.
apply: leqnn.
have H4: (card P) * (card P) = (card P) **2 by rewrite /= muln1.
have H5: 4 + (card P) * (card P) + (16**4)**(card P) <= (16**4)**(card P) + (16**4)**(card P) + (16**4)**(card P).
apply: leq_add=>//.
apply: leq_add=>//.
rewrite H4.
apply: leq_trans H3 _. apply: leqnn.
apply: leq_trans H5 _.
have H6: (16**4)**(card P) + (16**4)**(card P) + (16**4)**(card P) = 3 * (16**4)**(card P).
by rewrite [16]lock !mulSn mul0n addn0 -lock !addnA.
rewrite H6.
have H7: 3 * (16 ** 4) ** (card P) <= (16 ** 4) ** (card P) * (16 ** 4) ** (card P).
apply: leq_mul.
by apply: leq_trans _ H1.
by apply: leqnn.
apply: leq_trans H7 _.
rewrite -exp_plus.
have H8: card P + card P = 2 * (card P) by rewrite !mulSn mul0n addn0.
rewrite H8.
rewrite -exp_exp.
rewrite [(16**4)**2]exp_exp.
apply: leqnn.
Qed.
The main result, Proposition 3
Lemma main: forall k,
max (fun C:conf (state_space_G G)=> card (evolution_seq J k C))
<=
((eg_order G) * (card Q)) ** ((16 ** 8) ** (card P)).
Proof.
move=>k.
apply: leq_trans _ (APP k).
rewrite /A.
apply: max_lower=>C.
rewrite /setACP /evolution_to_coal.
have H: k = coal k (S (card P)) (init_econf X C).
apply/eqP; rewrite eqn_leq; apply/andP; split.
by apply: leq_trans _ (coal_leq _ _ _); rewrite coal_cardP; apply: leqnn.
by apply: coal_triv_bound.
rewrite {1}H.
by apply (max_upper (fun C0 : conf (state_space_G G) =>
card (evolution_seq J (coal k (S (card P)) (init_econf X C0)) C0))).
Qed.
End Analysis.