From dd01b3af69b1d9d9f483fccbdceb1413c975a669 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Fri, 11 Mar 2016 10:08:26 +0100
Subject: [PATCH] add some TODO so some stuff does not get forgotten
---
algebra/dra.v | 1 +
algebra/sts.v | 1 +
2 files changed, 2 insertions(+)
diff --git a/algebra/dra.v b/algebra/dra.v
index f62020e4..b2a0439d 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -127,6 +127,7 @@ Lemma to_validity_op (x y : A) :
to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y.
Proof. split; naive_solver auto using dra_op_valid. Qed.
+(* TODO: This has to be proven again. *)
(*
Lemma to_validity_included x y:
(✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
diff --git a/algebra/sts.v b/algebra/sts.v
index e35b4206..dccd85d5 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -385,6 +385,7 @@ Qed.
(* This is surprisingly different from to_validity_included. I am not sure
whether this is because to_validity_included is non-canonical, or this
one here is non-canonical - but I suspect both. *)
+(* TODO: These have to be proven again. *)
(*
Lemma sts_frag_included S1 S2 T1 T2 :
closed S2 T2 → S2 ≢ ∅ →
--
GitLab