From 9c3743b4aa538d7ef3cca3738a56935734ae8294 Mon Sep 17 00:00:00 2001
From: Lionel Rieg <lionel.rieg@univ-grenoble-alpes.fr>
Date: Wed, 13 Sep 2023 18:55:41 +0200
Subject: [PATCH] GraphEquivalence.v ported to Coq v8.16
---
Models/GraphEquivalence.v | 124 ++++++++++++++++++++------------------
Setting.v | 3 +
Util/NumberComplements.v | 3 +
Util/Ratio.v | 3 +
_CoqProject | 2 +-
5 files changed, 76 insertions(+), 59 deletions(-)
diff --git a/Models/GraphEquivalence.v b/Models/GraphEquivalence.v
index bbe2bc1b..9f56147e 100644
--- a/Models/GraphEquivalence.v
+++ b/Models/GraphEquivalence.v
@@ -116,9 +116,14 @@ Proof.
exists (inverse (proj1_sig (change_frame da (config_G2V config) g))).
split; try reflexivity; []. cbn -[equiv]. apply stable_threshold_inverse, proj2_sig.
+ intros config1 config2 Hconfig gg g ?. subst gg. now rewrite Hconfig.
-+ intros config1 config2 Hconfig gg g ? traj1 traj2 Htraj. subst gg. now rewrite Hconfig, Htraj.
++ intros config1 config2 Hconfig gg g ? traj1 traj2 Htraj. subst gg.
+ destruct_match_eq Heq1; destruct_match_eq Heq2; try reflexivity; [|];
+ exfalso; apply Bool.diff_false_true; rewrite <- Heq1, <- Heq2; [ symmetry |];
+ apply (choose_update_compat da (config_G2V_compat _ _ Hconfig) (eq_refl g) _ _ Htraj).
+ intros config1 config2 Hconfig id1 id2 Hid. simpl in Hid. subst id1.
- now rewrite Hconfig.
+ destruct_match_eq Heq1; destruct_match_eq Heq2; try reflexivity; [|];
+ exfalso; apply Bool.diff_false_true; rewrite <- Heq1, <- Heq2; [ symmetry |];
+ apply (choose_inactive_compat da (config_G2V_compat _ _ Hconfig) (eq_refl id2)).
Defined.
Instance da_D2C_compat : Proper (equiv ==> equiv) da_D2C.
@@ -156,10 +161,10 @@ Proof using .
split; try reflexivity; []. apply stable_threshold_inverse, proj2_sig.
+ intros config1 config2 Hconfig gg g ?. subst gg. now rewrite Hconfig.
+ intros config1 config2 Hconfig gg g ? pt1 pt2 Hpt.
- rewrite Hpt, Hconfig, H. reflexivity.
+ subst. do 3 f_equiv; auto; []. now rewrite Hpt.
+ intros config1 config2 Hconfig id1 id2 Hid. simpl in Hid. subst id1.
- destruct (Cconfig id2) as [v1 e1 p1 | e1 p1]. all: cbn-[ratio_0].
- all: rewrite Hconfig. all: reflexivity.
+ destruct (Cconfig id2) as [v1 e1 p1 | e1 p1]; cbn -[ratio_0];
+ now do 3 f_equiv; rewrite Hconfig.
Defined.
Instance da_C2D_compat : Proper (equiv ==> equiv ==> equiv) da_C2D.
@@ -240,9 +245,9 @@ Defined.
Instance add_edge_compat : Proper (equiv ==> equiv ==> equiv ==> equiv) add_edge.
Proof using .
intros ? ? He Ï1 Ï1' HÏ1 Ï2 Ï2' HÏ2. unfold add_edge.
-Time repeat destruct_match; solve [ rewrite HÏ1, HÏ2 in *; contradiction
- | rewrite <- HÏ1, <- HÏ2 in *; contradiction
- | simpl; rewrite ?HÏ1, ?HÏ2; repeat split; apply He ].
+repeat destruct_match;
+try solve [hnf; split; apply He | apply proj_ratio_compat in HÏ1, HÏ2; congruence]; [].
+split; trivial; []. cbn. apply proj_ratio_compat in HÏ1, HÏ2. congruence.
Qed.
(** Move by a ratio [Ï] from the state [state]. *)
@@ -380,10 +385,13 @@ simpl activate. destruct_match.
{ unfold Cobs, Dobs. unfold obs_from_config at 1. unfold obs_V2G.
rewrite Hlocal_config, Hlocal_state. reflexivity. }
assert (Hlocal_robot_decision : Clocal_robot_decision == Dlocal_robot_decision).
- { unfold Dlocal_robot_decision. cbn -[equiv]. rewrite Hobs. reflexivity. }
+ { unfold Dlocal_robot_decision. cbn -[equiv]. now apply (pgm_compat rbg). }
assert (Hchoice : Cchoice == if Dchoice then ratio_1 else ratio_0).
- { cbn -[equiv]. unfold Dchoice.
- rewrite Hlocal_config, config_V2G2V, Hobs. reflexivity. }
+ { cbn -[equiv]. unfold Dchoice, Dlocal_robot_decision.
+ apply config_G2V_compat in Hlocal_config. rewrite config_V2G2V in Hlocal_config.
+ destruct_match_eq Heq1; destruct_match_eq Heq2; reflexivity || exfalso;
+ apply Bool.diff_false_true; rewrite <- Heq1, <- Heq2; [ symmetry |];
+ apply (choose_update_compat da Hlocal_config (eq_refl g) _ _ (pgm_compat rbg _ _ Hobs)). }
assert (Hnew_local_state : Cnew_local_state == state_V2G Dnew_local_state).
{ unfold Cnew_local_state, Dnew_local_state. unfold update, UpdateG, UpdateV.
assert (Hlocal_g := Hlocal_config (Good g)). unfold config_V2G in Hlocal_g.
@@ -396,7 +404,8 @@ simpl activate. destruct_match.
(v =?= src Dlocal_robot_decision) as [Hv | Hv].
+ (* valid case: the robot chooses an adjacent edge *)
unfold move. destruct_match; try contradiction; [].
- rewrite Hchoice, Hlocal_robot_decision. destruct Dchoice.
+ rewrite (add_edge_compat Hlocal_robot_decision (reflexivity ratio_0) Hchoice).
+ destruct Dchoice.
- (* the demon lets the robot move *)
unfold add_edge. simpl equiv_dec.
destruct ((0 + 1)%R =?= 0%R); try (simpl in *; lra); [].
@@ -437,13 +446,13 @@ simpl activate. destruct_match.
unfold liftG. cbn [projT2]. repeat split.
- rewrite HCiso'. cbn. f_equiv. symmetry. apply Hiso.
- unfold equiv. cbn -[equiv precondition_satisfied_inv].
- Time setoid_rewrite <- (proj1 (iso_morphism _ e)).
- Time setoid_rewrite HCiso'.
+ setoid_rewrite <- (proj1 (iso_morphism _ e)).
+ setoid_rewrite HCiso'.
transitivity (inverse Diso (src e)); try apply HDiso'; [].
f_equiv. apply inverse_compat. now symmetry.
- unfold equiv. cbn -[equiv precondition_satisfied_inv].
- Time setoid_rewrite <- (proj2 (iso_morphism _ e)).
- Time setoid_rewrite HCiso'.
+ setoid_rewrite <- (proj2 (iso_morphism _ e)).
+ setoid_rewrite HCiso'.
transitivity (inverse Diso (tgt e)); try apply HDiso'; [].
f_equiv. apply inverse_compat. now symmetry.
- hnf. rewrite <- 2 iso_threshold.
@@ -580,8 +589,8 @@ simpl activate. destruct_match_eq Hactive.
simpl liftG. simpl state_G2V.
assert (Heq : threshold ((iso_E (projT1 (precondition_satisfied da config g))) e) == threshold e).
{ now rewrite <- iso_threshold, (proj2 (projT2 (precondition_satisfied da config g))). }
- destruct (Rle_dec (threshold e) p);
- destruct_match; try (rewrite <- Heq in *; contradiction); [|].
+ destruct (Rle_dec (threshold e) p); destruct_match; repeat rewrite proj_ratio_strict_ratio in *;
+ try (hnf in Heq; rewrite <- Heq in *; contradiction); [|].
+ (* we are after the threshold, g is seen at the target of the edge *)
cbn -[precondition_satisfied]. repeat split.
- rewrite <- (proj2 (iso_morphism _ _)).
@@ -624,15 +633,17 @@ simpl activate. destruct_match_eq Hactive.
{ unfold Cobs, Dobs. unfold obs_from_config at 2. unfold obs_V2G.
rewrite Hlocal_config, Hlocal_state. reflexivity. }
assert (Hlocal_robot_decision : Dlocal_robot_decision == Clocal_robot_decision).
- { unfold Dlocal_robot_decision. cbn -[equiv]. rewrite Hobs. reflexivity. }
+ { unfold Clocal_robot_decision, Dlocal_robot_decision. now apply (pgm_compat rbg). }
assert (Hchoice : Dchoice == if Rle_dec (threshold Clocal_robot_decision) Cchoice
then true else false).
- { unfold Dchoice, choose_update, da_C2D.
- rewrite Hlocal_config, Hchoose_update. rewrite Hlocal_robot_decision at 2.
- rewrite Hlocal_robot_decision.
- destruct (Rle_dec (threshold Clocal_robot_decision) Cchoice) as [Hle | Hlt].
- - rewrite <- Rle_bool_true_iff in Hle. apply Hle.
- - rewrite <- Rle_bool_false_iff in Hlt. apply Hlt. }
+ { unfold Dchoice, choose_update, da_C2D, Rle_bool.
+ do 2 destruct_match; try reflexivity; [|]; exfalso;
+ revert_one not; revert_one Rle; repeat rewrite proj_ratio_strict_ratio;
+ assert (Heq := proj1_sig_compat equiv_dec _ _ (threshold_compat _ _ Hlocal_robot_decision));
+ hnf in Heq; rewrite Heq, Hlocal_config;
+ rewrite (proj_ratio_compat _ _ (Hchoose_update Clocal_config g Dlocal_robot_decision)),
+ (proj_ratio_compat _ _ (choose_update_compat da (reflexivity _) (eq_refl g) _ _ Hlocal_robot_decision));
+ unfold Cchoice; congruence. }
assert (HCiso' : forall v, projT1 (precondition_satisfied_inv da config g) v == inverse Ciso v).
{ destruct (precondition_satisfied_inv da config g)as [Ciso' [HCf HCt]].
simpl projT1. intro v.
@@ -679,25 +690,36 @@ simpl activate. destruct_match_eq Hactive.
unfold move. simpl fst. symmetry.
do 2 destruct_match.
* (* valid case: the robot chooses an adjacent edge *)
- rewrite Hchoice. unfold add_edge.
- destruct_match; [| destruct_match]; simpl state_G2V.
- + (* the robot will not move so will end up in its starting position *)
+ revert Hchoice. destruct_match; intro Hchoice; hnf in Hchoice; rewrite Hchoice;
+ unfold add_edge; (destruct_match; [| destruct_match]); simpl state_G2V.
+ + (* absurd case *)
assert (H0 : proj_ratio Cchoice = 0%R).
- { assert (Hbounds := ratio_bounds Cchoice). simpl in *; lra. }
+ { assert (Hbounds := ratio_bounds Cchoice). cbn in *; lra. }
assert (proj_ratio Cchoice < threshold Clocal_robot_decision)%R.
{ rewrite H0. apply strict_ratio_bounds. }
- destruct_match; try lra; []. symmetry. split; apply Hlocal_robot_decision.
+ lra.
+ (* the robot reaches its destination *)
change (proj_ratio ratio_0) with 0%R in *. rewrite Rplus_0_l in *.
+ symmetry. hnf. simpl fst. simpl snd. split; apply Hlocal_robot_decision.
+ + (* the robot moves and ends up on the edge *)
+ rewrite Rplus_0_l in *.
+ destruct_match; try contradiction; [].
+ (* the ending point is after the edge threshold *)
+ symmetry. repeat split; simpl; apply Hlocal_robot_decision.
+ + (* the robot will not move so will end up in its starting position *)
+ assert (H0 : proj_ratio Cchoice = 0%R).
+ { assert (Hbounds := ratio_bounds Cchoice). cbn in *; lra. }
+ assert (proj_ratio Cchoice < threshold Clocal_robot_decision)%R.
+ { rewrite H0. apply strict_ratio_bounds. }
+ symmetry. split; cbn -[equiv]; apply Hlocal_robot_decision.
+ + (* absurd case *)
+ exfalso. change (proj_ratio ratio_0) with 0%R in *. rewrite Rplus_0_l in *.
assert (threshold Clocal_robot_decision <= proj_ratio Cchoice)%R.
{ transitivity 1; trivial; []. apply Rlt_le. apply strict_ratio_bounds. }
- destruct_match; try lra; [].
- symmetry. hnf. simpl fst. simpl snd. split; apply Hlocal_robot_decision.
+ contradiction.
+ (* the robot moves and ends up on the edge *)
rewrite Rplus_0_l in *.
- destruct_match.
- - (* the ending point is after the edge threshold *)
- symmetry. repeat split; simpl; apply Hlocal_robot_decision.
+ destruct_match; try contradiction; [].
- (* the ending point is before the edge threshold *)
symmetry. repeat split; simpl; apply Hlocal_robot_decision.
* (* absurd case: the robot does not make the same choice *)
@@ -745,16 +767,9 @@ simpl activate. destruct_match_eq Hactive.
++ destruct Hnew_local_state as [Hv He]. simpl fst in Hv. simpl snd in He.
(* destruct takes too long... *)
assert (threshold (Bijection.section (iso_E (projT1 (precondition_satisfied_inv da config g))) e)
- <= proj_ratio (proj_strict_ratio p)) by now rewrite Htest.
-
- (* too slow, case is faster *)
- (* Time destruct_match; try contradiction; []. (* 230 sec!!!! *) *)
- Time match goal with
- | |- (match ?x with | _ => _ end) == _ => case x
- end.
- all:swap 1 2.
- { intros notH.
- apply (absurd _ H);assumption. }
+ <= proj_ratio (proj_strict_ratio p)).
+ { hnf in Htest. rewrite proj_ratio_strict_ratio in *. now rewrite Htest. }
+ destruct_match; try contradiction; [].
split; simpl fst; simpl snd.
-- transitivity (tgt (Bijection.section (iso_E (inverse Ciso)) e)); [apply HCisoE |].
rewrite Hv, <- (proj2 (iso_morphism _ e)). cbn -[equiv].
@@ -766,15 +781,9 @@ simpl activate. destruct_match_eq Hactive.
symmetry. apply E_subrelation, Hiso.
++ destruct Hnew_local_state as [Hv He]. simpl fst in Hv. simpl snd in He.
assert (¬ threshold (Bijection.section (iso_E (projT1 (precondition_satisfied_inv da config g))) e)
- <= proj_ratio (proj_strict_ratio p)) by now rewrite Htest.
-
- (* too slow, case is faster *)
- (* Time destruct_match; try contradiction; []. (* 230 sec!!!! *) *)
- Time match goal with
- | |- (match ?x with | _ => _ end) == _ => case x
- end.
- { intros notH.
- apply (absurd _ notH);assumption. }
+ <= proj_ratio (proj_strict_ratio p)).
+ { hnf in Htest. rewrite proj_ratio_strict_ratio in *. now rewrite Htest. }
+ destruct_match; try contradiction; [].
split; simpl fst; simpl snd.
-- rewrite <- (proj1 (iso_morphism _ _)), Hv.
transitivity (Bijection.section (iso_V (inverse Ciso)) (src e)); [apply HCiso' |].
@@ -793,9 +802,8 @@ simpl activate. destruct_match_eq Hactive.
cbn -[equiv equiv_dec]. destruct_match.
- (* the robot is at the edge src *)
unfold add_edge, state_G2V.
- assert (He := strict_ratio_bounds (threshold e)). rewrite Hchoose_inactive.
- change (proj_ratio ratio_0) with 0. rewrite Rplus_0_l at 2.
- destruct (Rle_bool (threshold e) (proj_ratio (choose_inactive da config id))) eqn:Htest;
+ assert (He := strict_ratio_bounds (threshold e)). rewrite (proj_ratio_compat _ _ (Hchoose_inactive id)).
+ change (proj_ratio ratio_0) with 0. symmetry. destruct_match_eq Htest;
rewrite Rle_bool_true_iff in Htest || rewrite Rle_bool_false_iff in Htest;
repeat destruct_match; try (now split; auto);
simpl in * |-; try rewrite Rplus_0_l in *; contradiction || lra.
@@ -818,7 +826,7 @@ simpl activate. destruct_match_eq Hactive.
assert (Hp := strict_ratio_bounds p).
intro Habs. simpl in Habs. lra. }
destruct_match; try contradiction; [].
- rewrite Hchoose_inactive.
+ rewrite (proj_ratio_compat _ _ (Hchoose_inactive id)).
destruct (Rle_bool (threshold e) (p + choose_inactive da config id)) eqn:Hcase;
rewrite Rle_bool_true_iff in Hcase || rewrite Rle_bool_false_iff in Hcase;
repeat destruct_match; try solve [split; reflexivity | simpl in *; contradiction]; [].
diff --git a/Setting.v b/Setting.v
index fc5be1c5..d2caa4e4 100644
--- a/Setting.v
+++ b/Setting.v
@@ -1,5 +1,8 @@
Require Export SetoidDec.
Require Export Pactole.Util.Coqlib.
+Require Export Pactole.Util.SetoidDefs.
+Require Export Pactole.Util.NumberComplements.
+Require Export Pactole.Util.ListComplements.
Require Export Pactole.Util.Ratio.
Require Pactole.Util.Stream.
Require Pactole.Util.Lexprod.
diff --git a/Util/NumberComplements.v b/Util/NumberComplements.v
index cf636fc9..76d8f79d 100644
--- a/Util/NumberComplements.v
+++ b/Util/NumberComplements.v
@@ -19,6 +19,7 @@
(**************************************************************************)
Require Import Utf8 SetoidDec Reals Lia Psatz.
+Require Import Pactole.Util.SetoidDefs.
Set Implicit Arguments.
(* ******************************** *)
@@ -41,6 +42,8 @@ intros x y. unfold Basics.flip. cbn. split; intro Hxy.
- destruct Hxy. now apply Rle_antisym.
Qed.
+Global Instance Rle_partialorder_equiv : PartialOrder equiv Rle := Rle_partialorder.
+
Global Instance Rlt_SO : StrictOrder Rlt.
Proof. split.
+ intro. apply Rlt_irrefl.
diff --git a/Util/Ratio.v b/Util/Ratio.v
index d7512ae9..496d3492 100644
--- a/Util/Ratio.v
+++ b/Util/Ratio.v
@@ -118,6 +118,9 @@ Notation "n '/sr' m" := (mk_strict_ratio n m ltac:(clear; abstract lia) ltac:(cl
(only parsing, at level 10).
Notation "n '/sr' m" := (mk_strict_ratio n m _ _) (at level 10, only printing).
+Lemma proj_ratio_strict_ratio : forall x, proj_ratio (proj_strict_ratio x) = proj1_sig x.
+Proof. intros []. reflexivity. Qed.
+
(** ** Trajectory **)
(** Trajectories are paths inside the space. *)
diff --git a/_CoqProject b/_CoqProject
index 087746b2..1caec517 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -59,7 +59,7 @@ Models/DiscreteGraph.v
Models/Isometry.v
Models/Similarity.v
Models/ContinuousGraph.v
-#Models/GraphEquivalence.v
+Models/GraphEquivalence.v
Models/RingSSync.v
## Spaces
--
GitLab