Skip to content
Snippets Groups Projects
Commit bca74818 authored by Sébastien Bouchard's avatar Sébastien Bouchard
Browse files

Progress

parent 6a4b6099
No related branches found
No related tags found
No related merge requests found
...@@ -30,10 +30,10 @@ Typeclasses eauto := (bfs). ...@@ -30,10 +30,10 @@ Typeclasses eauto := (bfs).
Section ConvergenceAlgo. Section ConvergenceAlgo.
(** There are [n] good robots and no byzantine one. *) (** There are [ub] good robots and no byzantine one. *)
Variable n : nat. Context {gt0 : greater_than 0}.
Instance MyRobots : Names := Robots (S n) 0. Instance MyRobots : Names := Robots ub 0.
Instance NoByz : NoByzantine. Instance NoByz : NoByzantine.
Proof using . now split. Qed. Proof using . now split. Qed.
......
...@@ -17,26 +17,28 @@ Typeclasses eauto := (bfs). ...@@ -17,26 +17,28 @@ Typeclasses eauto := (bfs).
Section Exploration. Section Exploration.
(** Given an abitrary ring *) (** Given an abitrary ring *)
Context {RR : RingSpec}. Context {gt2 : greater_than 2}.
(** There are kG good robots and no byzantine ones. *) (** There are k good robots and no byzantine ones. *)
Variable k : nat. Context {gt0 : greater_than 0}.
Instance Robots : Names := Robots (S k) 0. Notation n := (@ub 2 gt2).
Notation k := (@ub 0 gt0).
Instance Robots : Names := Robots k 0.
(** Assumptions on the number of robots: it strictly divides the ring size. *) (** Assumptions on the number of robots: it strictly divides the ring size. *)
Hypothesis kdn : (S (S (S n)) mod (S k) = 0). Hypothesis kdn : (n mod k = 0).
Hypothesis k_inf_n : (S k < S (S (S n))). Hypothesis k_inf_n : (k < n).
Lemma local_subproof1 : S (S (S n)) = S k * (S (S (S n)) / (S k)). Lemma local_subproof1 : n = k * (n / k).
Proof using kdn. apply Nat.div_exact. apply Nat.neq_succ_0. apply kdn. Qed. Proof using kdn. apply Nat.div_exact. apply neq_ub_lb. apply kdn. Qed.
Lemma local_subproof2 : S (S (S n)) / (S k) 0. Lemma local_subproof2 : n / k 0.
Proof using kdn. Proof using kdn.
intros Habs. elim (Nat.neq_succ_0 (S (S n))). rewrite local_subproof1, Habs. intros Habs. eapply (@neq_ub_0 2 gt2). rewrite local_subproof1, Habs.
apply Nat.mul_0_r. apply Nat.mul_0_r.
Qed. Qed.
Lemma local_subproof3 : m : nat, Lemma local_subproof3 : m : nat,
m < S k -> m * (S (S (S n)) / (S k)) < S (S (S n)). m < k -> m * (n / k) < n.
Proof using kdn. Proof using kdn.
intros * H. rewrite local_subproof1 at 2. apply mult_lt_compat_r. intros * H. rewrite local_subproof1 at 2. apply mult_lt_compat_r.
apply H. apply Nat.neq_0_lt_0, local_subproof2. apply H. apply Nat.neq_0_lt_0, local_subproof2.
...@@ -62,7 +64,7 @@ Variable r : robogram. ...@@ -62,7 +64,7 @@ Variable r : robogram.
(** *** Definition of the demon used in the proof **) (** *** Definition of the demon used in the proof **)
Definition create_ref_config (g : G) : location := Definition create_ref_config (g : G) : location :=
mod2fin (fin2nat g * (S (S (S n)) / (S k))). mod2fin (fin2nat g * (n / k)).
(** The starting configuration where robots are evenly spaced: (** The starting configuration where robots are evenly spaced:
each robot is at a distance of [ring_size / kG] from the previous one, each robot is at a distance of [ring_size / kG] from the previous one,
...@@ -83,7 +85,7 @@ Proof using kdn. ...@@ -83,7 +85,7 @@ Proof using kdn.
all: apply local_subproof3, fin_lt. all: apply local_subproof3, fin_lt.
Qed. Qed.
(** Translating [ref_config] by multiples of [S (S (S n)) / (S k)] (** Translating [ref_config] by multiples of [n / k]
does not change its observation. *) does not change its observation. *)
Lemma obs_asbf_ref_config : forall g, Lemma obs_asbf_ref_config : forall g,
!! (map_config (asbf (create_ref_config g)⁻¹) ref_config) == !! ref_config. !! (map_config (asbf (create_ref_config g)⁻¹) ref_config) == !! ref_config.
...@@ -101,17 +103,17 @@ Proof using kdn. ...@@ -101,17 +103,17 @@ Proof using kdn.
+ rewrite NoDupA_Leibniz. apply names_NoDup. + rewrite NoDupA_Leibniz. apply names_NoDup.
* intro pt. repeat rewrite InA_map_iff; autoclass; []. * intro pt. repeat rewrite InA_map_iff; autoclass; [].
split; intros [id [Hpt _]]; revert Hpt; apply (no_byz id); clear id; intros g' Hpt. split; intros [id [Hpt _]]; revert Hpt; apply (no_byz id); clear id; intros g' Hpt.
+ pose (id' := subf g' g). change (fin (S k)) with G in id'. + pose (id' := subf g' g). change (fin k) with G in id'.
exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. } exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. }
rewrite <- Hpt. cbn-[subf create_ref_config]. split. 2: reflexivity. rewrite <- Hpt. cbn-[subf create_ref_config]. split. 2: reflexivity.
unfold create_ref_config, Datatypes.id, id'. apply fin2nat_inj. unfold create_ref_config, Datatypes.id, id'. apply fin2nat_inj.
rewrite 2 subf2nat, 3 mod2fin2nat, Nat.add_mod_idemp_l, rewrite 2 subf2nat, 3 mod2fin2nat, Nat.add_mod_idemp_l,
2 (Nat.mod_small (_ * _)). rewrite local_subproof1 at 3 5. 2 (Nat.mod_small (_ * _)). rewrite local_subproof1 at 3 5.
rewrite <- Nat.mul_sub_distr_r, <- Nat.mul_add_distr_r, rewrite <- Nat.mul_sub_distr_r, <- Nat.mul_add_distr_r,
Nat.mul_mod_distr_r. reflexivity. 1,5: apply Nat.neq_succ_0. Nat.mul_mod_distr_r. reflexivity. 1,5: apply neq_ub_0.
apply local_subproof2. all: apply local_subproof3. apply fin_lt. apply local_subproof2. all: apply local_subproof3. apply fin_lt.
apply mod2fin_lt. apply mod2fin_lt.
+ pose (id' := addf g' g). change (fin (S k)) with G in id'. + pose (id' := addf g' g). change (fin k) with G in id'.
exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. } exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. }
rewrite <- Hpt. cbn. split. 2: reflexivity. unfold create_ref_config, id'. rewrite <- Hpt. cbn. split. 2: reflexivity. unfold create_ref_config, id'.
apply fin2nat_inj. rewrite subf2nat, 3 mod2fin2nat, addf2nat, apply fin2nat_inj. rewrite subf2nat, 3 mod2fin2nat, addf2nat,
...@@ -121,7 +123,7 @@ Proof using kdn. ...@@ -121,7 +123,7 @@ Proof using kdn.
all: cycle 1. rewrite Nat.add_mod_idemp_l, <- Nat.add_assoc, all: cycle 1. rewrite Nat.add_mod_idemp_l, <- Nat.add_assoc,
le_plus_minus_r, <- Nat.add_mod_idemp_r, Nat.mod_same, Nat.add_0_r. le_plus_minus_r, <- Nat.add_mod_idemp_r, Nat.mod_same, Nat.add_0_r.
apply Nat.mod_small. 4: apply Nat.lt_le_incl. apply Nat.mod_small. 4: apply Nat.lt_le_incl.
2,3,5,6,10: apply Nat.neq_succ_0. 3,6: apply local_subproof2. 2,3,5,6,10: apply neq_ub_0. 3,6: apply local_subproof2.
3,4: apply local_subproof3. all: apply fin_lt. 3,4: apply local_subproof3. all: apply fin_lt.
Qed. Qed.
...@@ -181,12 +183,13 @@ Proof using Hmove kdn k_inf_n. ...@@ -181,12 +183,13 @@ Proof using Hmove kdn k_inf_n.
intros e Heq_e. exists (mod2fin 1). intro Hl. intros e Heq_e. exists (mod2fin 1). intro Hl.
induction Hl as [e [g Hvisited] | e Hlater IHvisited]. induction Hl as [e [g Hvisited] | e Hlater IHvisited].
* rewrite Heq_e in Hvisited. cbn in Hvisited. * rewrite Heq_e in Hvisited. cbn in Hvisited.
apply (f_equal (@fin2nat (S (S (S n))))) in Hvisited. revert Hvisited. apply (f_equal (@fin2nat n)) in Hvisited. revert Hvisited.
cbn-[Nat.modulo Nat.div]. rewrite local_subproof1 at 2. cbn-[Nat.modulo Nat.div]. rewrite local_subproof1 at 2.
rewrite Nat.mul_mod_distr_r, (Nat.mod_small 1), Nat.mul_eq_1. rewrite Nat.mul_mod_distr_r, (Nat.mod_small 1), Nat.mul_eq_1.
intros [_ Habs]. elim (lt_not_le _ _ k_inf_n). rewrite local_subproof1, intros [_ Habs]. elim (lt_not_le _ _ k_inf_n). rewrite local_subproof1,
Habs, Nat.mul_1_r. reflexivity. 3: apply local_subproof2. apply lt_n_S, Habs, Nat.mul_1_r. reflexivity. 3: apply local_subproof2.
Nat.neq_0_lt_0. all: apply Nat.neq_succ_0. 2: apply neq_ub_lb. erewrite <- smaller_bound_ub. apply lt_lb_ub.
Unshelve. auto.
* apply IHvisited. rewrite Heq_e, execute_tail. rewrite round_id. f_equiv. * apply IHvisited. rewrite Heq_e, execute_tail. rewrite round_id. f_equiv.
Qed. Qed.
...@@ -242,15 +245,15 @@ Qed. ...@@ -242,15 +245,15 @@ Qed.
Lemma f_config_injective_N : config m1 m2, Lemma f_config_injective_N : config m1 m2,
f_config config m1 == f_config config m2 f_config config m1 == f_config config m2
-> m1 mod (S (S (S n))) == m2 mod (S (S (S n))). -> m1 mod n == m2 mod n.
Proof using kdn k_inf_n. Proof using kdn k_inf_n.
unfold f_config. intros * Heq. specialize (Heq (Good fin0)). unfold f_config. intros * Heq. specialize (Heq (Good fin0)).
unshelve eapply addm_bounded_diff_inj. 6: rewrite 2 addm_mod. 5: apply Heq. unshelve eapply (@addm_bounded_diff_inj 2 gt2). 5: rewrite 2 addm_mod.
2,3: split. 2,4: apply Nat.le_0_l. all: apply mod2fin_lt. 5: apply Heq. 2,3: split. 2,4: apply Nat.le_0_l. all: apply mod2fin_lt.
Qed. Qed.
Lemma f_config_modulo : config m, Lemma f_config_modulo : config m,
f_config config (m mod (S (S (S n)))) == f_config config m. f_config config (m mod n) == f_config config m.
Proof using . intros * id. apply addm_mod. Qed. Proof using . intros * id. apply addm_mod. Qed.
Lemma asbf_f_config : (config : configuration) (id1 id2 : ident) (m : nat), Lemma asbf_f_config : (config : configuration) (id1 id2 : ident) (m : nat),
...@@ -268,11 +271,11 @@ Definition equiv_config config1 config2 : Prop ...@@ -268,11 +271,11 @@ Definition equiv_config config1 config2 : Prop
Lemma equiv_config_m_sym : m config1 config2, Lemma equiv_config_m_sym : m config1 config2,
equiv_config_m m config1 config2 equiv_config_m m config1 config2
-> equiv_config_m (@oppm (S (S n)) m) config2 config1. -> equiv_config_m (@oppm 2 gt2 m) config2 config1.
Proof using k_inf_n kdn. Proof using k_inf_n kdn.
unfold equiv_config_m. intros * Hequiv. unshelve erewrite Hequiv, unfold equiv_config_m. intros * Hequiv. unshelve erewrite Hequiv,
f_config_merge, <- f_config_modulo, (proj2 (Nat.mod_divide _ _ _)). f_config_merge, <- f_config_modulo, (proj2 (Nat.mod_divide _ _ _)).
apply Nat.neq_succ_0. symmetry. apply f_config_0. apply oppm_divide. apply neq_ub_0. symmetry. apply f_config_0. apply oppm_divide.
Qed. Qed.
Lemma equiv_config_m_trans : m1 m2 config1 config2 config3, Lemma equiv_config_m_trans : m1 m2 config1 config2 config3,
...@@ -286,14 +289,14 @@ Qed. ...@@ -286,14 +289,14 @@ Qed.
Instance equiv_config_equiv : Equivalence equiv_config. Instance equiv_config_equiv : Equivalence equiv_config.
Proof using k_inf_n kdn. split. Proof using k_inf_n kdn. split.
+ intro config. exists 0. unfold equiv_config_m. now rewrite f_config_0. + intro config. exists 0. unfold equiv_config_m. now rewrite f_config_0.
+ intros config1 config2 [m Hm]. exists (@oppm (S (S n)) m). + intros config1 config2 [m Hm]. exists (@oppm 2 gt2 m).
apply (equiv_config_m_sym Hm). apply (equiv_config_m_sym Hm).
+ intros ? ? ? [m1 Hm1] [m2 Hm2]. exists (m1 + m2). + intros ? ? ? [m1 Hm1] [m2 Hm2]. exists (m1 + m2).
revert Hm1 Hm2. apply equiv_config_m_trans. revert Hm1 Hm2. apply equiv_config_m_trans.
Qed. Qed.
Lemma equiv_config_mod : (m : nat) (config1 config2 : configuration), Lemma equiv_config_mod : (m : nat) (config1 config2 : configuration),
equiv_config_m (m mod (S (S (S n)))) config1 config2 equiv_config_m (m mod n) config1 config2
<-> equiv_config_m m config1 config2. <-> equiv_config_m m config1 config2.
Proof using . Proof using .
intros. split; intros H id. intros. split; intros H id.
...@@ -351,7 +354,7 @@ Proof using . ...@@ -351,7 +354,7 @@ Proof using .
Qed. Qed.
Lemma AlwaysEquiv_sym : m (e1 e2 : execution), Lemma AlwaysEquiv_sym : m (e1 e2 : execution),
AlwaysEquiv m e1 e2 -> AlwaysEquiv (@oppm (S (S n)) m) e2 e1. AlwaysEquiv m e1 e2 -> AlwaysEquiv (@oppm 2 gt2 m) e2 e1.
Proof using k_inf_n kdn. Proof using k_inf_n kdn.
cofix Hcoind. intros m1 e1 e2 [Hnow Hlater]. constructor. cofix Hcoind. intros m1 e1 e2 [Hnow Hlater]. constructor.
+ now apply equiv_config_m_sym. + now apply equiv_config_m_sym.
...@@ -374,7 +377,7 @@ Proof using k_inf_n kdn. ...@@ -374,7 +377,7 @@ Proof using k_inf_n kdn.
Qed. Qed.
Lemma AlwaysEquiv_mod : (m : nat) (e1 e2 : execution), Lemma AlwaysEquiv_mod : (m : nat) (e1 e2 : execution),
AlwaysEquiv (m mod (S (S (S n)))) e1 e2 <-> AlwaysEquiv m e1 e2. AlwaysEquiv (m mod n) e1 e2 <-> AlwaysEquiv m e1 e2.
Proof using . Proof using .
intros. split. intros. split.
- revert m e1 e2. cofix Hrec. intros * H. constructor. - revert m e1 e2. cofix Hrec. intros * H. constructor.
...@@ -476,15 +479,15 @@ Qed. ...@@ -476,15 +479,15 @@ Qed.
Lemma ref_config_AlwaysMoving : AlwaysMoving (execute r bad_demon ref_config). Lemma ref_config_AlwaysMoving : AlwaysMoving (execute r bad_demon ref_config).
Proof using Hmove k_inf_n kdn. Proof using Hmove k_inf_n kdn.
generalize (AlwaysEquiv_refl (execute r bad_demon ref_config)). generalize (AlwaysEquiv_refl (execute r bad_demon ref_config)).
generalize 0, (execute r bad_demon ref_config) at 1 3. generalize 0 at 1. generalize (execute r bad_demon ref_config) at 1 3.
cofix Hcoind. intros m e Hequiv. constructor. cofix Hcoind. intros e m Hequiv. constructor.
+ clear Hcoind. rewrite Hequiv. intros [Hstop _]. elim Hmove. + clear Hcoind. rewrite Hequiv. intros [Hstop _]. elim Hmove.
unfold Stall in Hstop. rewrite execute_tail, round_simplify in Hstop. unfold Stall in Hstop. rewrite execute_tail, round_simplify in Hstop.
simpl hd in Hstop. eapply move_along_I. rewrite move_along_0. simpl hd in Hstop. apply (move_along_I fin0). rewrite move_along_0.
apply fin2nat_inj. setoid_rewrite <- Nat.mod_small. 2,3: apply fin_lt. apply fin2nat_inj. setoid_rewrite <- Nat.mod_small. 2,3: apply fin_lt.
eapply f_config_injective_N. rewrite fin02nat, f_config_0. eapply f_config_injective_N. rewrite fin02nat, f_config_0.
symmetry. apply Hstop. symmetry. apply Hstop.
+ apply (Hcoind (addm (oppf target) m)). clear Hcoind. rewrite addm2nat, + eapply (Hcoind _ (addm (oppf target) m)). clear Hcoind. rewrite addm2nat,
Nat.add_comm. apply AlwaysEquiv_mod. Nat.add_comm. apply AlwaysEquiv_mod.
apply AlwaysEquiv_trans with (tl (execute r bad_demon ref_config)). apply AlwaysEquiv_trans with (tl (execute r bad_demon ref_config)).
apply Hequiv. rewrite oppf_oppm. apply Hequiv. rewrite oppf_oppm.
......
...@@ -42,10 +42,10 @@ Typeclasses eauto := (bfs) 10. ...@@ -42,10 +42,10 @@ Typeclasses eauto := (bfs) 10.
(** ** Framework of the correctness proof: a finite set with at least two elements **) (** ** Framework of the correctness proof: a finite set with at least two elements **)
Section GatheringInR2. Section GatheringInR2.
Variable n : nat. Context {gt1 : greater_than 1}.
(** There are n good robots and no byzantine ones. *) (** There are n good robots and no byzantine ones. *)
Instance MyRobots : Names := Robots (S (S n)) 0. Instance MyRobots : Names := Robots ub 0.
Instance NoByz : NoByzantine. Instance NoByz : NoByzantine.
Proof using . now split. Qed. Proof using . now split. Qed.
......
...@@ -34,8 +34,9 @@ Instance NoByz : NoByzantine. ...@@ -34,8 +34,9 @@ Instance NoByz : NoByzantine.
Proof using . now split. Qed. Proof using . now split. Qed.
Notation lt2 := (fun x => x < 2)%nat. Notation lt2 := (fun x => x < 2)%nat.
Definition lt02 : (0 < 2)%nat := ltac:(abstract auto).
Definition lt12 : (1 < 2)%nat := ltac:(abstract lia). Definition lt12 : (1 < 2)%nat := ltac:(abstract lia).
Definition r0 : G := fin0. Definition r0 : G := Fin lt02.
Definition r1 : G := Fin lt12. Definition r1 : G := Fin lt12.
Lemma id_case : forall id, id = Good r0 \/ id = Good r1. Lemma id_case : forall id, id = Good r0 \/ id = Good r1.
......
...@@ -6,7 +6,7 @@ Set Implicit Arguments. ...@@ -6,7 +6,7 @@ Set Implicit Arguments.
Section RingSSync. Section RingSSync.
Context {RR : RingSpec} {Robots : Names}. Context {gt2 : greater_than 2} {Robots : Names}.
Global Existing Instance NodesLoc. Global Existing Instance NodesLoc.
......
...@@ -8,7 +8,6 @@ ...@@ -8,7 +8,6 @@
*) *)
(**************************************************************************) (**************************************************************************)
Require Import Rbase SetoidDec. Require Import Rbase SetoidDec.
From Pactole Require Import Util.Coqlib Util.Fin Core.State. From Pactole Require Import Util.Coqlib Util.Fin Core.State.
Set Implicit Arguments. Set Implicit Arguments.
......
...@@ -14,14 +14,11 @@ From Pactole Require Import Util.Coqlib Util.Bijection Spaces.Graph ...@@ -14,14 +14,11 @@ From Pactole Require Import Util.Coqlib Util.Bijection Spaces.Graph
(** ** A ring **) (** ** A ring **)
(** What we need to define a ring. *)
Class RingSpec := { n : nat }.
Section Ring. Section Ring.
Context {RR : RingSpec}. Context {gt2 : greater_than 2}.
Definition ring_node := finite_node (S (S (S n))). Definition ring_node := finite_node ub.
Inductive direction := Forward | Backward | SelfLoop. Inductive direction := Forward | Backward | SelfLoop.
Definition ring_edge := (ring_node * direction)%type. Definition ring_edge := (ring_node * direction)%type.
...@@ -43,7 +40,7 @@ Definition dir2nat (d : direction) : nat := ...@@ -43,7 +40,7 @@ Definition dir2nat (d : direction) : nat :=
match d with match d with
| SelfLoop => 0 | SelfLoop => 0
| Forward => 1 | Forward => 1
| Backward => S (S n) | Backward => Nat.pred ub
end. end.
Definition dir2nat_compat : Proper (equiv ==> equiv) dir2nat := _. Definition dir2nat_compat : Proper (equiv ==> equiv) dir2nat := _.
...@@ -54,19 +51,24 @@ Proof using . reflexivity. Qed. ...@@ -54,19 +51,24 @@ Proof using . reflexivity. Qed.
Lemma dir21 : dir2nat Forward = 1. Lemma dir21 : dir2nat Forward = 1.
Proof using . reflexivity. Qed. Proof using . reflexivity. Qed.
Lemma dir2SSn : dir2nat Backward = S (S n). Lemma dir2SSn : dir2nat Backward = Nat.pred ub.
Proof using . reflexivity. Qed. Proof using . reflexivity. Qed.
Lemma dir2nat_lt : d : direction, dir2nat d < S (S (S n)). Lemma dir2nat_lt : d : direction, dir2nat d < ub.
Proof using . intros. destruct d. all: cbn. all: lia. Qed. Proof using .
intros. destruct d. all: cbn. 2: apply lt_pred_ub.
all: apply lt_sb_ub. all: auto.
Qed.
Lemma dir2nat_inj : Util.Preliminary.injective equiv equiv dir2nat. Lemma dir2nat_inj : Util.Preliminary.injective equiv equiv dir2nat.
Proof using . Proof using .
intros d1 d2 H. destruct d1, d2. all: try inversion H. all: reflexivity. intros d1 d2 H'. destruct d1, d2. all: inversion H' as [H].
all: try reflexivity. all: exfalso. 1,4: symmetry in H.
all: eapply neq_pred_ub_sb. 2,4,6,8: exact H. all: auto.
Qed. Qed.
Lemma dir2mod2fin : d : direction, Lemma dir2mod2fin : d : direction,
fin2nat (@mod2fin (S (S n)) (dir2nat d)) = dir2nat d. fin2nat (mod2fin (dir2nat d)) = dir2nat d.
Proof using . Proof using .
intros. rewrite mod2fin2nat. apply Nat.mod_small. apply dir2nat_lt. intros. rewrite mod2fin2nat. apply Nat.mod_small. apply dir2nat_lt.
Qed. Qed.
...@@ -76,7 +78,7 @@ Definition nat2Odir (m : nat) : option direction := ...@@ -76,7 +78,7 @@ Definition nat2Odir (m : nat) : option direction :=
match m with match m with
| 0 => Some SelfLoop | 0 => Some SelfLoop
| 1 => Some Forward | 1 => Some Forward
| _ => if m =? S (S n) then Some Backward else None | _ => if m =? Nat.pred ub then Some Backward else None
end. end.
Definition nat2Odir_compat : Proper (equiv ==> equiv) nat2Odir := _. Definition nat2Odir_compat : Proper (equiv ==> equiv) nat2Odir := _.
...@@ -85,9 +87,11 @@ Lemma nat2Odir_Some : ∀ (d : direction) (m : nat), ...@@ -85,9 +87,11 @@ Lemma nat2Odir_Some : ∀ (d : direction) (m : nat),
nat2Odir m = Some d <-> dir2nat d = m. nat2Odir m = Some d <-> dir2nat d = m.
Proof using . Proof using .
unfold dir2nat, nat2Odir. intros d m. split; intros H. unfold dir2nat, nat2Odir. intros d m. split; intros H.
all: destruct d, m as [|p]. all: try inversion H. 6: rewrite Nat.eqb_refl. all: destruct d, m as [|p]. all: try inversion H. all: try reflexivity.
all: try reflexivity. all: destruct p. all: try inversion H. 4:{ exfalso. eapply neq_pred_ub_sb. 2: exact H. auto. }
all: try reflexivity. all: destruct (S (S p) =? S (S n)) eqn:Hd. 4: rewrite Nat.eqb_refl. all: destruct p. all: try inversion H.
all: try reflexivity. 4:{ exfalso. eapply neq_pred_ub_sb. 2: exact H.
auto. } all: destruct (S (S p) =? Nat.pred ub) eqn:Hd.
all: try inversion H. symmetry. apply Nat.eqb_eq, Hd. all: try inversion H. symmetry. apply Nat.eqb_eq, Hd.
Qed. Qed.
...@@ -106,7 +110,7 @@ Lemma nat2Odir_pick : ∀ m : nat, ...@@ -106,7 +110,7 @@ Lemma nat2Odir_pick : ∀ m : nat,
Proof using . Proof using .
intros. unfold nat2Odir. destruct m as [|m]. apply Pick, dir20. intros. unfold nat2Odir. destruct m as [|m]. apply Pick, dir20.
destruct m as [|m]. apply Pick, dir21. destruct m as [|m]. apply Pick, dir21.
destruct (S (S m) =? S (S n)) eqn:Hd. destruct (S (S m) =? Nat.pred ub) eqn:Hd.
- apply Nat.eqb_eq in Hd. rewrite Hd. apply Pick, dir2SSn. - apply Nat.eqb_eq in Hd. rewrite Hd. apply Pick, dir2SSn.
- apply Nat.eqb_neq in Hd. apply Nopick. intros d H. elim Hd. - apply Nat.eqb_neq in Hd. apply Nopick. intros d H. elim Hd.
destruct d. all: inversion H. subst. reflexivity. destruct d. all: inversion H. subst. reflexivity.
...@@ -143,7 +147,7 @@ Lemma move_alongE : ∀ (v : ring_node) (d : direction), ...@@ -143,7 +147,7 @@ Lemma move_alongE : ∀ (v : ring_node) (d : direction),
Proof using . intros. reflexivity. Qed. Proof using . intros. reflexivity. Qed.
Definition move_along2nat : (v : ring_node) (d : direction), Definition move_along2nat : (v : ring_node) (d : direction),
fin2nat (move_along v d) = (v + dir2nat d) mod (S (S (S n))). fin2nat (move_along v d) = (v + dir2nat d) mod ub.
Proof using . intros. apply addm2nat. Qed. Proof using . intros. apply addm2nat. Qed.
Lemma move_alongI_ : d : direction, Lemma move_alongI_ : d : direction,
...@@ -224,13 +228,13 @@ Definition swap_direction_bij : bijection direction ...@@ -224,13 +228,13 @@ Definition swap_direction_bij : bijection direction
swap_directionK swap_directionK. swap_directionK swap_directionK.
Lemma dir2nat_swap_direction : d : direction, Lemma dir2nat_swap_direction : d : direction,
dir2nat (swap_direction d) = @oppm (S (S n)) (dir2nat d). dir2nat (swap_direction d) = oppm (dir2nat d).
Proof using . Proof using .
intros. rewrite oppm_oppf, oppf2nat, dir2mod2fin. symmetry. destruct d. intros. rewrite oppm_oppf, oppf2nat, dir2mod2fin. symmetry. destruct d.
2: cbn-[Nat.modulo Nat.sub]. 1,3: cbn-[Nat.modulo]. apply Nat.mod_small, 2: cbn-[Nat.modulo Nat.sub]. 1,3: cbn-[Nat.modulo]. rewrite Nat.sub_1_r.
Nat.lt_succ_diag_r. apply Nat.mod_same, Nat.neq_succ_0. apply Nat.mod_small, lt_pred_ub. rewrite Nat.sub_0_r. apply Nat.mod_same,
rewrite 2 Nat.sub_succ, Nat.sub_succ_l, Nat.sub_diag. 2: reflexivity. neq_ub_0. rewrite <- S_pred_ub at 1. rewrite Nat.sub_succ_l,
apply Nat.mod_small, lt_n_S, Nat.lt_0_succ. Nat.sub_diag. apply Nat.mod_small. apply lt_sb_ub. auto. reflexivity.
Qed. Qed.
Lemma move_along_swap_direction : (v : ring_node) (d : direction), Lemma move_along_swap_direction : (v : ring_node) (d : direction),
...@@ -324,10 +328,10 @@ Qed. ...@@ -324,10 +328,10 @@ Qed.
Definition Ring (thd : ring_edge -> R) Definition Ring (thd : ring_edge -> R)
(thd_pos : e, (0 < thd e < 1)%R) (thd_pos : e, (0 < thd e < 1)%R)
(thd_compat : Proper (equiv ==> eq) thd) (thd_compat : Proper (equiv ==> eq) thd)
: FiniteGraph (S (S (S n))) ring_edge. : FiniteGraph ub ring_edge.
Proof using . Proof using .
refine {| refine {|
V_EqDec := @finite_node_EqDec (S (S (S n))); V_EqDec := @finite_node_EqDec ub;
E_EqDec := ring_edge_EqDec; E_EqDec := ring_edge_EqDec;
src := fst; src := fst;
tgt := λ e, move_along (fst e) (snd e); tgt := λ e, move_along (fst e) (snd e);
...@@ -341,7 +345,7 @@ Proof using . ...@@ -341,7 +345,7 @@ Proof using .
Defined. Defined.
(** If we do not care about threshold values, we just take 1/2 everywhere. *) (** If we do not care about threshold values, we just take 1/2 everywhere. *)
Global Instance nothresholdRing : FiniteGraph (S (S (S n))) ring_edge := Global Instance nothresholdRing : FiniteGraph ub ring_edge :=
Ring (fun _ => 1/2)%R Ring (fun _ => 1/2)%R
ltac:(abstract (intro; lra)) ltac:(abstract (intro; lra))
(fun _ _ _ => eq_refl). (fun _ _ _ => eq_refl).
...@@ -354,7 +358,7 @@ Global Instance Ring_isomorphism_Setoid : ...@@ -354,7 +358,7 @@ Global Instance Ring_isomorphism_Setoid :
Global Instance Ring_isomorphism_Inverse : Inverse (isomorphism nothresholdRing) Global Instance Ring_isomorphism_Inverse : Inverse (isomorphism nothresholdRing)
:= @IsoInverse _ _ nothresholdRing. := @IsoInverse _ _ nothresholdRing.
Global Instance Ring_isomorphism_Compoosition Global Instance Ring_isomorphism_Composition
: Composition (isomorphism nothresholdRing) : Composition (isomorphism nothresholdRing)
:= @IsoComposition _ _ nothresholdRing. := @IsoComposition _ _ nothresholdRing.
...@@ -382,14 +386,14 @@ Defined. ...@@ -382,14 +386,14 @@ Defined.
Definition trans_compat : Proper (equiv ==> equiv) trans := _. Definition trans_compat : Proper (equiv ==> equiv) trans := _.
Lemma trans2nat : (m : nat) (v : ring_node), fin2nat (trans m v) Lemma trans2nat : (m : nat) (v : ring_node), fin2nat (trans m v)
= (v + (S (S (S n)) - m mod (S (S (S n))))) mod (S (S (S n))). = (v + (ub - m mod ub)) mod ub.
Proof using . apply asbmV2nat. Qed. Proof using . apply asbmV2nat. Qed.
Lemma transV2nat : (m : nat) (v : ring_node), Lemma transV2nat : (m : nat) (v : ring_node),
fin2nat ((trans m)⁻¹ v) = (v + m) mod (S (S (S n))). fin2nat ((trans m)⁻¹ v) = (v + m) mod ub.
Proof using . apply asbm2nat. Qed. Proof using . apply asbm2nat. Qed.
Lemma trans_mod : m : nat, trans (m mod (S (S (S n)))) == trans m. Lemma trans_mod : m : nat, trans (m mod ub) == trans m.
Proof using . Proof using .
intros. split; [|split]. all: unfold trans. intros. split; [|split]. all: unfold trans.
all: cbn-[equiv inverse Nat.modulo]. 1,2: rewrite asbm_mod. all: cbn-[equiv inverse Nat.modulo]. 1,2: rewrite asbm_mod.
...@@ -416,30 +420,30 @@ Lemma transI_fin_max : (trans 1)⁻¹ fin_max = fin0. ...@@ -416,30 +420,30 @@ Lemma transI_fin_max : (trans 1)⁻¹ fin_max = fin0.
Proof using . apply asbm_fin_max. Qed. Proof using . apply asbm_fin_max. Qed.
Lemma transI_fin0_divide : (v : ring_node) (m : nat), Lemma transI_fin0_divide : (v : ring_node) (m : nat),
Nat.divide (S (S (S n))) (v + m) (trans m)⁻¹ v = fin0. Nat.divide ub (v + m) (trans m)⁻¹ v = fin0.
Proof using . apply asbm_fin0_divide. Qed. Proof using . apply asbm_fin0_divide. Qed.
Lemma trans_locally_inj : (m1 m2 : nat), Lemma trans_locally_inj : (m1 m2 : nat),
m1 m2 m2 - m1 < S (S (S n)) trans m1 == trans m2 m1 = m2. m1 m2 m2 - m1 < ub trans m1 == trans m2 m1 = m2.
Proof using . Proof using .
intros * ?? H. eapply asbmV_locally_inj. 3: apply H. all: eassumption. intros * ?? H. eapply asbmV_locally_inj. 3: apply H. all: eassumption.
Qed. Qed.
Lemma transV_locally_inj : (m1 m2 : nat), Lemma transV_locally_inj : (m1 m2 : nat),
m1 m2 m2 - m1 < S (S (S n)) (trans m1)⁻¹ == (trans m2)⁻¹ m1 = m2. m1 m2 m2 - m1 < ub (trans m1)⁻¹ == (trans m2)⁻¹ m1 = m2.
Proof using . Proof using .
intros * ?? H. eapply asbm_locally_inj. 3: apply H. all: eassumption. intros * ?? H. eapply asbm_locally_inj. 3: apply H. all: eassumption.
Qed. Qed.
Lemma trans_bounded_diff_inj : (p : nat) (m1 m2 : nat), Lemma trans_bounded_diff_inj : (p : nat) (m1 m2 : nat),
bounded_diff (S (S (S n))) p m1 bounded_diff (S (S (S n))) p m2 bounded_diff ub p m1 bounded_diff ub p m2
trans m1 == trans m2 m1 = m2. trans m1 == trans m2 m1 = m2.
Proof using . Proof using .
intros * ?? H. eapply asbmV_bounded_diff_inj. 3: apply H. all: eassumption. intros * ?? H. eapply asbmV_bounded_diff_inj. 3: apply H. all: eassumption.
Qed. Qed.
Lemma transV_bounded_diff_inj : (p : nat) (m1 m2 : nat), Lemma transV_bounded_diff_inj : (p : nat) (m1 m2 : nat),
bounded_diff (S (S (S n))) p m1 bounded_diff (S (S (S n))) p m2 bounded_diff ub p m1 bounded_diff ub p m2
(trans m1)⁻¹ == (trans m2)⁻¹ m1 = m2. (trans m1)⁻¹ == (trans m2)⁻¹ m1 = m2.
Proof using . Proof using .
intros * ?? H. eapply asbm_bounded_diff_inj. 3: apply H. all: eassumption. intros * ?? H. eapply asbm_bounded_diff_inj. 3: apply H. all: eassumption.
......
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment