Merge dev-cons-new into main

.nix/config.nix

@@ -29,7 +29,7 @@
   ## If not specified, it defaults to "_CoqProject"
   # coqproject = "_CoqProject";
 
-  default-bundle = "8.18";
+  default-bundle = "8.19";
 
   bundles."8.18" = {
     push-branches = [ "**" ];
@@ -42,6 +42,17 @@
     coqPackages.imm.override.version = "1.6.1";
   };
 
+  bundles."8.19" = {
+    push-branches = [ "**" ];
+    coqPackages.vscoq-language-server.override.version = "v2.1.7";
+    coqPackages.coq.override.version = "8.19";
+    coqPackages.hahn.override.version = "1.19.1";
+    coqPackages.hahnExt.override.version = "0.9.5";
+    coqPackages.sflib.override.version = "master";
+    coqPackages.promising-lib.override.version = "1.19.0";
+    coqPackages.imm.override.version = "1.6.2";
+  };
+
   cachix.coq = {};
   cachix.math-comp = {};
   cachix.coq-community = {};

.nix/nixpkgs.nix

@@ -1,4 +1,4 @@
 fetchTarball {
-         url = https://github.com/weakmemory/nixpkgs/archive/74f9c700bb92c7f7ba5052a2db9502b21b88f71a.tar.gz;
-         sha256 = "0d9jjn5mdky7np1mqbkis0dn4vj9vdxzdzrlfyqcm0znp1mjqd8l";
+         url = https://github.com/weakmemory/nixpkgs/archive/a93669e68292ca2319f73de7c3eb1cccb4b3bb63.tar.gz;
+         sha256 = "15cslfjdkzgb2ynssn7q0ars17mcang11kgc4l0ka16cbimi9x0w";
        }

.vscode/settings.json

@@ -14,5 +14,8 @@
         "**/*_cp_aux.v": true
     },
     "nixEnvSelector.suggestion": false,
-    "nixEnvSelector.nixFile": "${workspaceFolder}/default.nix"
+    "nixEnvSelector.nixFile": "${workspaceFolder}/default.nix",
+    "vscoq.args": [
+        "-R", "src", "xmm"
+    ]
 }

Makefile

@@ -1,5 +1,5 @@
 COQMODULE    := xmm
-COQTHEORIES  := src/reordering/*.v src/xmm/*.v src/lib/*.v
+COQTHEORIES  := src/reordering/*.v src/xmm/*.v src/lib/*.v src/traces/*.v src/xmm_cons/*.v
 
 .PHONY: all theories clean tounicode
 

src/lib/AuxRel.v

@@ -299,4 +299,43 @@ Proof using.
   destruct HREL as ((y' & R1 & EQ & YIN) & NEG). subst y'.
   exists y. splits; auto.
   intro FALSO. apply NEG. eauto.
+Qed.
+
+Lemma ct_unit_left A (r : relation A) :
+    r ⨾ r⁺ ⊆ r⁺.
+Proof.
+  arewrite (r ⊆ r⁺) at 1. apply ct_ct.
+Qed.
+
+Lemma trans_helper_swapped A (r r' : relation A)
+    (TRANS : transitive r) :
+  r ⨾ (r' ∪ r)⁺ ⊆ r ∪ (r ⨾ r'⁺)⁺ ⨾ r^?.
+Proof using.
+  rewrite path_union2. rewrite !seq_union_r.
+  arewrite (r ⨾ r＊ ⊆ r⁺).
+  arewrite (r ⨾ r⁺ ⊆ r⁺) by apply ct_unit_left.
+  arewrite (r⁺ ⊆ r).
+  arewrite (r'⁺ ⊆ r'＊).
+  rels.
+  rewrite rtE at 1. rewrite seq_union_r, seq_id_r.
+  unionL; eauto with hahn.
+  all: unionR right.
+  { rewrite <- ct_step with (r := r ;; r'⁺).
+    basic_solver 10. }
+  rewrite ct_rotl, <- !seqA.
+  rewrite <- ct_begin.
+  rewrite !seqA.
+  rewrite rtE, !seq_union_r, seq_id_r.
+  arewrite ((r ⨾ r'⁺)⁺ ⨾ r ⨾ r'⁺ ⊆ (r ⨾ r'⁺)⁺).
+  { now rewrite ct_unit. }
+  rewrite crE, seq_union_r, seq_id_r.
+  eauto with hahn.
+Qed.
+
+Lemma trans_helper A (r r' : relation A)
+        (TRANS : transitive r) :
+    r ⨾ (r ∪ r')⁺ ⊆ r ∪ (r ⨾ r'⁺)⁺ ⨾ r^?.
+Proof using.
+    arewrite (r ⨾ (r ∪ r')⁺ ≡ r ⨾ (r' ∪ r)⁺) by now rewrite unionC.
+    apply trans_helper_swapped; vauto.
 Qed.

src/lib/AuxRel3.v

@@ -0,0 +1,37 @@
+From hahn Require Import Hahn.
+From hahnExt Require Import HahnExt.
+
+Set Implicit Arguments.
+
+Lemma empty_codom_irr (A : Type) (r r' : relation A)
+        (EMP : codom_rel r ≡₁ ∅) :
+    irreflexive (r ⨾ r').
+Proof using.
+    apply empty_irr. split; try basic_solver.
+    intros x y H. destruct H. destruct H. assert (Q : ∅ x0).
+    { apply EMP. basic_solver. }
+    destruct Q.
+Qed.
+
+Lemma empty_seq_codom (A : Type) (r r' : relation A)
+        (EMP : codom_rel r ≡₁ ∅) :
+    codom_rel (r ⨾ r') ≡₁ ∅.
+Proof using.
+    split; try basic_solver. intros x H. induction H.
+    destruct H. destruct H. destruct EMP.
+    assert (IN : codom_rel r x1).
+    { exists x0; eauto. }
+    assert (F : ∅ x1).
+    { apply H1 in IN; eauto. }
+    basic_solver.
+Qed.
+
+Lemma set_disjoint_union_minus (A : Type) (s1 s2 s' : A -> Prop)
+    (E_MAP : s' ≡₁ s1 ∪₁ s2)
+    (NIN : set_disjoint s1 s2) :
+  s' \₁ s2 ≡₁ s1.
+Proof using.
+    rewrite E_MAP. rewrite set_minus_union_l.
+    rewrite set_minusK. rewrite set_union_empty_r.
+    apply set_minus_disjoint; eauto.
+Qed.