From 9bae6a749f08dc27228dce1308b40bf2b05cf4f5 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Mon, 24 Mar 2025 14:59:14 +0100
Subject: [PATCH 1/3] add annotations to avoid evars

---
 theories/logrel/F_mu_ref_conc/binary/fundamental.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/logrel/F_mu_ref_conc/binary/fundamental.v b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
index 497cf885..9a7a69d5 100644
--- a/theories/logrel/F_mu_ref_conc/binary/fundamental.v
+++ b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
@@ -577,8 +577,8 @@ Section fundamental.
     - iApply bin_log_related_rec; done.
     - iApply bin_log_related_lam; done.
     - iApply bin_log_related_letin; done.
-    - iApply bin_log_related_seq; done.
-    - iApply bin_log_related_app; done.
+    - iApply (bin_log_related_seq _ _ _ _ _ Ï„1); done.
+    - iApply (bin_log_related_app _ _ _ _ _ Ï„1); done.
     - iApply bin_log_related_tlam; done.
     - iApply bin_log_related_tapp; done.
     - iApply bin_log_related_pack; done.
@@ -588,7 +588,7 @@ Section fundamental.
     - iApply bin_log_related_fork; done.
     - iApply bin_log_related_alloc; done.
     - iApply bin_log_related_load; done.
-    - iApply bin_log_related_store; done.
+    - iApply (bin_log_related_store _ _ _ _ _ Ï„); done.
     - iApply bin_log_related_CAS; done.
     - iApply bin_log_related_FAA; done.
   Qed.
-- 
GitLab


From e7841de1a01857475d844c579e7476a31cc0a49a Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Mon, 24 Mar 2025 15:44:45 +0100
Subject: [PATCH 2/3] name mangling

---
 .../logrel/F_mu_ref_conc/binary/fundamental.v | 62 ++++++++++---------
 1 file changed, 32 insertions(+), 30 deletions(-)

diff --git a/theories/logrel/F_mu_ref_conc/binary/fundamental.v b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
index 9a7a69d5..eae6b1e4 100644
--- a/theories/logrel/F_mu_ref_conc/binary/fundamental.v
+++ b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
@@ -560,36 +560,38 @@ Section fundamental.
   Theorem binary_fundamental Γ e τ :
     Γ ⊢ₜ e : τ → ⊢ Γ ⊨ e ≤log≤ e : τ.
   Proof.
-    induction 1.
-    - iApply bin_log_related_var; done.
+    elim=> {Γ e τ} Γ.
+    - intros; iApply bin_log_related_var; done.
     - iApply bin_log_related_unit.
-    - iApply bin_log_related_int.
-    - iApply bin_log_related_bool.
-    - iApply bin_log_related_int_binop; done.
-    - iApply bin_log_related_Eq_binop; done.
-    - iApply bin_log_related_pair; done.
-    - iApply bin_log_related_fst; done.
-    - iApply bin_log_related_snd; done.
-    - iApply bin_log_related_injl; done.
-    - iApply bin_log_related_injr; done.
-    - iApply bin_log_related_case; done.
-    - iApply bin_log_related_if; done.
-    - iApply bin_log_related_rec; done.
-    - iApply bin_log_related_lam; done.
-    - iApply bin_log_related_letin; done.
-    - iApply (bin_log_related_seq _ _ _ _ _ Ï„1); done.
-    - iApply (bin_log_related_app _ _ _ _ _ Ï„1); done.
-    - iApply bin_log_related_tlam; done.
-    - iApply bin_log_related_tapp; done.
-    - iApply bin_log_related_pack; done.
-    - iApply bin_log_related_unpack; done.
-    - iApply bin_log_related_fold; done.
-    - iApply bin_log_related_unfold; done.
-    - iApply bin_log_related_fork; done.
-    - iApply bin_log_related_alloc; done.
-    - iApply bin_log_related_load; done.
-    - iApply (bin_log_related_store _ _ _ _ _ Ï„); done.
-    - iApply bin_log_related_CAS; done.
-    - iApply bin_log_related_FAA; done.
+    - intros; iApply bin_log_related_int.
+    - intros; iApply bin_log_related_bool.
+    - intros; iApply bin_log_related_int_binop; done.
+    - intros; iApply bin_log_related_Eq_binop; done.
+    - intros; iApply bin_log_related_pair; done.
+    - intros; iApply bin_log_related_fst; done.
+    - intros; iApply bin_log_related_snd; done.
+    - intros; iApply bin_log_related_injl; done.
+    - intros; iApply bin_log_related_injr; done.
+    - intros; iApply bin_log_related_case; done.
+    - intros; iApply bin_log_related_if; done.
+    - intros; iApply bin_log_related_rec; done.
+    - intros; iApply bin_log_related_lam; done.
+    - intros; iApply bin_log_related_letin; done.
+    - move=> e1 e2 Ï„1 Ï„2 ? ? ? ?.
+      iApply (bin_log_related_seq _ _ _ _ _ Ï„1); done.
+    - move=> e1 e2 Ï„1 Ï„2 ? ? ? ?.
+      iApply (bin_log_related_app _ _ _ _ _ Ï„1); done.
+    - intros; iApply bin_log_related_tlam; done.
+    - intros; iApply bin_log_related_tapp; done.
+    - intros; iApply bin_log_related_pack; done.
+    - intros; iApply bin_log_related_unpack; done.
+    - intros; iApply bin_log_related_fold; done.
+    - intros; iApply bin_log_related_unfold; done.
+    - intros; iApply bin_log_related_fork; done.
+    - intros; iApply bin_log_related_alloc; done.
+    - intros; iApply bin_log_related_load; done.
+    - move=> e1 e2 Ï„ ? ? ? ?; iApply (bin_log_related_store _ _ _ _ _ Ï„); done.
+    - intros; iApply bin_log_related_CAS; done.
+    - intros; iApply bin_log_related_FAA; done.
   Qed.
 End fundamental.
-- 
GitLab


From 6567ed5b6b74b16c60faae48351a470f7eb127e5 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Mon, 24 Mar 2025 16:06:43 +0100
Subject: [PATCH 3/3] duplicate clear

---
 theories/logrel/F_mu_ref_conc/binary/fundamental.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/logrel/F_mu_ref_conc/binary/fundamental.v b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
index eae6b1e4..7d8696af 100644
--- a/theories/logrel/F_mu_ref_conc/binary/fundamental.v
+++ b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
@@ -560,7 +560,7 @@ Section fundamental.
   Theorem binary_fundamental Γ e τ :
     Γ ⊢ₜ e : τ → ⊢ Γ ⊨ e ≤log≤ e : τ.
   Proof.
-    elim=> {Γ e τ} Γ.
+    elim=> {}Γ {e τ}.
     - intros; iApply bin_log_related_var; done.
     - iApply bin_log_related_unit.
     - intros; iApply bin_log_related_int.
-- 
GitLab