Library main
Require Import ssreflect.
Require Import ssrbool.
Require Import ssrnat.
Require Import ssrfun.
Require Import eqtype.
Require Import seq.
Require Import fintype.
Require Import general.
Require Import graphs.
Require Import reach.
Section MainResult.
We assume a JAG
J and a uniform graph G.
Variable J: jag.
Variable G: graph.
We exclude trivial cases
Variable orderGgt1: 1 < eg_order G.
Variable cardQgt0: 0 < card Q.
Variable cardPgt1: 1 < card P.
Main result:
There exists a number
c such that the maximum number of
configurations that are reachable from any start configuration C
at most k steps is bounded by ((order G)*|Q|)^{c^{|P|}}
Theorem configs_bound: exists c, forall k,
max (fun C:conf (state_space_G G) => card (evolution_seq J k C))
<=
exp (eg_order G * card Q) (exp c (card P)).
Proof.
exists (exp 16 8)=>k.
apply (@main J G (@abstractionG G) (@measure_abstG G)
(@measure_upper_abstG G) (@measure_lower_abstG G) (@measure_step_abstG G J)
(@measure_init_abstG G J) (@init_factors G) (@obs_abstG G)
(@econf_det_abstG G) orderGgt1 cardQgt0 cardPgt1 k).
Qed.
This theorem shows that the number of counfigurations is bounded.
We have formulated Proposition 3 in the paper so that the number
of nodes that
J can visit in G is bounded by
((order G)*|Q|)^{c^{|P|}} for some constant c.
Of course, this is direct consequence of configs_bound.
We prove it formally next.
The nodes that are visited in a single configuration C
Definition nodes_of_conf(C: conf (state_space_G G)) :=
maps (fun x => C.2 x) (enum P).
The list of nodes visited in at most k steps starting from C
Definition nodes_visited J k (C: conf (state_space_G G)) :=
flatten (maps nodes_of_conf (evolution_seq J k C)).
Lemma card_nodes_visited: forall C k,
card (nodes_visited J k C) <= (card P) * (card (evolution_seq J k C)).
Proof.
move=>C k.
apply: card_flatten=>D; apply: leq_trans (card_size _) _;
rewrite cardA /nodes_of_conf size_maps; apply: leqnn.
Qed.
The next Theorem formalises Proposition 3. It expresses
that there exists a constant
c such that, for any k, the number
of nodes in the graph G that J can visit in k steps is bounded
by ((order G)*|P|)^{c^{|P|}}.
Theorem nodes_visited_bound:
exists c, forall k,
max (fun C=>card (nodes_visited J k C)) <= exp (eg_order G * card Q) (exp c (card P)).
Proof.
exists (exp 16 16)=>k.
have H: max (fun C=>card (nodes_visited J k C))
<= card P * max (fun C:(conf (state_space_G G))=> card (evolution_seq J k C)).
apply: max_lower=>C.
apply: leq_trans (card_nodes_visited C k) _.
apply: leq_mul; first by apply: leqnn.
apply: (@max_upper _ (fun C=> card (evolution_seq J k C))).
apply: leq_trans H _.
have H0: 1 < eg_order G * card Q.
rewrite -(muln1 2); apply: leq_mul. apply: orderGgt1. apply: cardQgt0.
have H1: card P <= exp (eg_order G * card Q) (card P) by apply: leqnexp.
have H2: exp (eg_order G * card Q) (card P) <= exp (eg_order G * card Q) (exp (exp 16 8) (card P)).
apply: leq_exp2l; first by apply: ltnW. by apply: leqnexp.
have H3: 2 <= exp (exp 16 8) (card P).
have H31: 2 <= exp (exp 16 8) 1 by auto.
apply: leq_trans H31 _; apply: leq_exp2l=>//; apply: ltnW; apply: cardPgt1.
have H4: (exp (eg_order G * card Q) (exp (exp 16 8) (card P))) * (exp (eg_order G * card Q) (exp (exp 16 8) (card P)))
<= (exp (eg_order G * card Q) (exp (exp 16 16) (card P))).
rewrite -exp_plus.
have H41: exp (exp 16 8) (card P) + exp (exp 16 8) (card P)
= 2 * exp (exp 16 8) (card P).
by rewrite [16]lock !mulSn mul0n addn0.
have H42: 16=8+8 by auto.
have H43: card P + card P = 2*(card P) by rewrite !mulSn mul0n /= addn0.
rewrite H41.
apply: leq_exp2l; first by apply: ltnW.
apply: (@leq_trans (exp (exp 16 8) (card P) * exp (exp 16 8) (card P))); first by apply: leq_mul; last by apply: leqnn.
by rewrite -exp_plus !exp_exp H43 mulnA; apply: leqnn.
apply: leq_trans _ H4; apply: leq_mul; first by apply: leq_trans H1 (leq_trans H2 _); apply: leqnn.
apply (@main J G (@abstractionG G) (@measure_abstG G)
(@measure_upper_abstG G) (@measure_lower_abstG G) (@measure_step_abstG G J)
(@measure_init_abstG G J) (@init_factors G) (@obs_abstG G)
(@econf_det_abstG G) orderGgt1 cardQgt0 cardPgt1 k).
Qed.
End MainResult.
Section InstanceU.
Finally, we show that the graphs that the main results can be used
for the concrete graphs constructed in graphs.v.
We instantiate the results for the graphs H_{m,d} in the paper
(which are called U here).
Variable J:jag.
Variable d m:nat.
Variable mgt1: 1 < m.
Graph gU corresponds to H_{m,d}.
Definition gU := graphU d mgt1.
We note that the bounds from Lemmas 15 and 18 hold without further
assumptions
Variable k:nat.
Definition RU := @R J gU (abstractionG gU) (@measure_abstG gU) k.
Definition AU := @A J gU (abstractionG gU) (@measure_abstG gU) k.
The following terms
R0_boundU, RSn_boundU and An_boundU are the
bounds from Lemma 14 and 17
Definition R0_boundU := (@R0_bound J gU (abstractionG gU)
(@measure_abstG gU) (@measure_upper_abstG gU) (@init_factors gU) k).
Definition RSn_boundU := (@RSn_bound J gU (abstractionG gU)
(@measure_abstG gU) (@measure_lower_abstG gU) (@measure_step_abstG gU J)
(@obs_abstG gU) (@econf_det_abstG gU) k).
Definition An_boundU := (@An_bound J gU (@abstractionG gU) (@measure_abstG gU)
(@measure_upper_abstG gU) (@measure_lower_abstG gU) (@measure_step_abstG gU J)
(@measure_init_abstG gU J) k).
Displaying the statements of the lemmas:
Check R0_boundU.
gives
R J (measure_abstG (G:=gU)) k 0 <= card Q * exp (card P) (card P)
Check RSn_boundU.
gives
forall n : nat,
R J (measure_abstG (G:=gU)) k (S n) <=
R J (measure_abstG (G:=gU)) k n
* S (S (A J (measure_abstG (G:=gU)) k n * exp (card P) (card P)))
* exp (card P) (card P)
Check An_boundU.
Finally, we instantiate the above main results for the graphs H_{m,d}
Variable cardQgt0: 0 < card Q.
Variable cardPgt1: 1 < card P.
Lemma orderUgt1: 1 < eg_order gU.
Proof.
rewrite /= /eg_order_CG.
apply: (leq_trans mgt1 _).
rewrite -{1}(muln1 m) leq_mul2l.
by apply/orP; right; apply: m_posU.
Qed.
Instance of Theorem
config_bound for gU
Theorem configs_boundU: exists c, forall k,
max (fun C:conf (state_space_G gU) => card (evolution_seq J k C))
<=
exp (eg_order gU * card Q) (exp c (card P)).
Proof. by apply: configs_bound; first by apply: orderUgt1. Qed.
Instance of Theorem
nodes_visited_bound for gU
Theorem nodes_visited_boundU:
exists c, forall k,
max (fun C => card (nodes_visited gU J k C))
<= exp (eg_order gU * card Q) (exp c (card P)).
Proof. by apply: nodes_visited_bound; first by apply: orderUgt1. Qed.
Definition Prop3 := (@main J gU (@abstractionG gU) (@measure_abstG gU)
(@measure_upper_abstG gU) (@measure_lower_abstG gU) (@measure_step_abstG gU J)
(@measure_init_abstG gU J) (@init_factors gU) (@obs_abstG gU)
(@econf_det_abstG gU) orderUgt1 cardQgt0 cardPgt1 k).
End InstanceU.