From ec0401066cae98776b18dd783bc5a7728983494e Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 13 Mar 2019 14:49:47 +0100
Subject: [PATCH] remove a useless file
---
_CoqProject | 1 -
theories/logic/proofmode/tactics.v | 1 -
theories/logic/rules.v | 2 +-
theories/prelude/pureclosed.v | 114 -----------------------------
4 files changed, 1 insertion(+), 117 deletions(-)
delete mode 100644 theories/prelude/pureclosed.v
diff --git a/_CoqProject b/_CoqProject
index 38508df..86b7cd1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,7 +3,6 @@
theories/prelude/ctx_subst.v
theories/prelude/properness.v
theories/prelude/asubst.v
-theories/prelude/pureclosed.v
theories/prelude/bijections.v
theories/logic/spec_ra.v
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index ab31686..9c8cc51 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -6,7 +6,6 @@ From iris.proofmode Require Import
reduction.
From reloc.logic Require Import proofmode.spec_tactics.
From reloc.logic Require Export model rules.
-From reloc.prelude Require Export pureclosed.
From iris.proofmode Require Export tactics.
(* Set Default Proof Using "Type". *)
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 6602d87..2247bc7 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -5,7 +5,7 @@ From iris.algebra Require Import list.
From iris.program_logic Require Import ectx_lifting.
From iris.heap_lang Require Import proofmode.
From reloc.logic Require Import model proofmode.spec_tactics.
-From reloc.prelude Require Import ctx_subst pureclosed.
+From reloc.prelude Require Import ctx_subst.
Section rules.
Context `{relocG Σ}.
diff --git a/theories/prelude/pureclosed.v b/theories/prelude/pureclosed.v
deleted file mode 100644
index 5af10a1..0000000
--- a/theories/prelude/pureclosed.v
+++ /dev/null
@@ -1,114 +0,0 @@
-(* ReLoC -- Relational logic for fine-grained concurrency *)
-(** An alternative to `PureExec` *)
-From iris.heap_lang Require Export lang notation proofmode metatheory.
-
-Class PureClosed Ï• n (e1 e2 : expr) :=
- pureexec_subst_map : ∀ vs, PureExec ϕ n (subst_map vs e1) (subst_map vs e2).
-
-Ltac solve_pure_exec := intros vs; simpl; apply _.
-
-Instance pure_pairc (v1 v2 : val) :
- PureClosed True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
-Proof. solve_pure_exec. Qed.
-Instance pure_injlc (v : val) :
- PureClosed True 1 (InjL $ Val v) (Val $ InjLV v).
-Proof. solve_pure_exec. Qed.
-Instance pure_injrc (v : val) :
- PureClosed True 1 (InjR $ Val v) (Val $ InjRV v).
-Proof. solve_pure_exec. Qed.
-
-(** TODO : Move to metatheory *)
-Lemma subst_map_subst vs x v e :
- subst_map vs (subst x v e) =
- subst_map (<[x:=v]> vs) e.
-Proof.
- revert vs.
- assert (∀ x f vs, BNamed x ≠f → binder_delete f (<[x:=v]> vs) = <[x:=v]>(binder_delete f vs)) as Hdel.
- { intros ? [|?] vs =>/= // He. rewrite delete_insert_ne // =>?. apply He; by subst. }
- induction e=> vs; simplify_map_eq; auto with f_equal.
- - match goal with
- | |- context [ <[?x:=_]> _ !! ?y ] =>
- destruct (decide (x = y)); simplify_map_eq=> //
- end.
- - f_equal. destruct (decide _) as [[??]|[<-%dec_stable|[<-%dec_stable ?]]%not_and_l_alt].
- + etrans. apply IHe. rewrite !Hdel //.
- + simpl. by rewrite delete_insert_delete.
- + rewrite Hdel // /=. by rewrite delete_insert_delete.
-Qed.
-Lemma subst_map_subst' vs x v e :
- subst_map vs (subst' x v e) =
- subst_map (binder_insert x v vs) e.
-Proof. destruct x; eauto using subst_map_subst. Qed.
-
-Instance pure_unop op v v' :
- PureClosed (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
-Proof. solve_pure_exec. Qed.
-
-Instance pure_binop op v1 v2 v' :
- PureClosed (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v').
-Proof. solve_pure_exec. Qed.
-
-Instance pure_if_true e1 e2 : PureClosed True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
-Proof. solve_pure_exec. Qed.
-
-Instance pure_if_false e1 e2 : PureClosed True 1 (If (Val $ LitV $ LitBool false) e1 e2) e2.
-Proof. solve_pure_exec. Qed.
-
-Instance pure_fst v1 v2 :
- PureClosed True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
-Proof. solve_pure_exec. Qed.
-
-Instance pure_snd v1 v2 :
- PureClosed True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
-Proof. solve_pure_exec. Qed.
-
-Instance pure_case_inl v e1 e2 :
- PureClosed True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
-Proof. solve_pure_exec. Qed.
-
-Instance pure_case_inr v e1 e2 :
- PureClosed True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
-Proof. solve_pure_exec. Qed.
-
-(** Closedness condition are required for lambdas *)
-Class ClosedExpr (e : expr) := closed_expr : is_closed_expr [] e.
-Hint Extern 0 (ClosedExpr _) => compute; reflexivity : typeclass_instances.
-
-Instance pure_beta f x (erec : expr) (v1 v2 : val) `{AsRecV v1 f x erec} :
- ClosedExpr (Rec f x erec) →
- PureClosed True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
-Proof.
- rewrite (@as_recv v1). simpl.
- intros Hcl vs. simpl.
- rewrite subst_map_subst'.
- rewrite subst_map_binder_insert.
- rewrite subst_map_subst'.
- rewrite subst_map_binder_insert.
- enough ((subst_map (binder_delete f (binder_delete x vs)) erec) = erec) as ->;
- first apply _.
- eapply subst_map_is_closed=> // y.
- admit.
-Admitted.
-
-Instance pure_recc f x (erec : expr) :
- ClosedExpr (Rec f x erec) →
- PureClosed True 1 (Rec f x erec) (Val $ RecV f x erec).
-Proof.
- move=>/= Herec vs /=.
- enough ((subst_map (binder_delete x (binder_delete f vs)) erec) = erec) as ->;
- first apply _.
- admit.
-Admitted.
-
-(* TODO: this is needed to reduce (v ;; t) → t for an arbitrary expression t. *)
-Instance pure_seq v (t : expr) :
- PureClosed True 2 (Val v;; t) t.
-Proof.
- intros vs. simpl.
- assert (AsRecV (λ: <>, (subst_map vs t)) <> <> (subst_map vs t)).
- { by unlock. }
- intros _. eapply (nsteps_trans 1 1); last first.
- { set (L := lifting.pure_beta BAnon BAnon (subst_map vs t) _ v).
- rewrite <- lock in L. simpl in *. by apply L. }
- eapply (pure_exec_fill [AppLCtx v]); [apply _|done].
-Qed.
--
GitLab