GraphEquivalence.v ported to Coq v8.16

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]; [].

Setting.v

 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.

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.

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. *)

_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