Rename iris folder into modures.

iris/language.v

-Require Import prelude.prelude.
-
-Class language (E V S : Type) := Language {
-  to_expr : V → E;
-  of_expr : E → option V;
-  atomic : E → Prop;
-  prim_step : (E * S) → (E * S) → option E → Prop;
-  of_to_expr v : of_expr (to_expr v) = Some v;
-  to_of_expr e v : of_expr e = Some v → to_expr v = e;
-  values_stuck e σ s' ef : prim_step (e,σ) s' ef → of_expr e = None;
-  atomic_not_value e : atomic e → of_expr e = None;
-  atomic_step e1 σ1 e2 σ2 ef :
-    atomic e1 →
-    prim_step (e1,σ1) (e2,σ2) ef →
-    is_Some (of_expr e2)
-}.
-
-Section foo.
-  Context `{language E V St}.
-
-  Definition cfg : Type := (list E * St)%type.
-  Inductive step (ρ1 ρ2 : cfg) : Prop :=
-    | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
-       ρ1 = (t1 ++ e1 :: t2, σ1) →
-       ρ1 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
-       prim_step (e1, σ1) (e2, σ2) ef →
-       step ρ1 ρ2.
-
-  Definition steps := rtc step.
-  Definition stepn := nsteps step.
-End foo.
\ No newline at end of file

iris/namespace.v

-Require Export prelude.countable prelude.co_pset.
-
-Definition namespace := list positive.
-Definition nnil : namespace := nil.
-Definition ndot `{Countable A} (I : namespace) (x : A) : namespace :=
-  encode x :: I.
-Definition nclose (I : namespace) : coPset := coPset_suffixes (encode I).
-
-Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _).
-Proof. by intros I1 x1 I2 x2 ?; simplify_equality. Qed.
-Lemma nclose_nnil : nclose nnil = coPset_all.
-Proof. by apply (sig_eq_pi _). Qed.
-Lemma encode_nclose I : encode I ∈ nclose I.
-Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
-Lemma nclose_subseteq `{Countable A} I x : nclose (ndot I x) ⊆ nclose I.
-Proof.
-  intros p; unfold nclose; rewrite !elem_coPset_suffixes; intros [q ->].
-  destruct (list_encode_suffix I (ndot I x)) as [q' ?]; [by exists [encode x]|].
-  by exists (q ++ q')%positive; rewrite <-(associative_L _); f_equal.
-Qed.
-Lemma ndot_nclose `{Countable A} I x : encode (ndot I x) ∈ nclose I.
-Proof. apply nclose_subseteq with x, encode_nclose. Qed.
-Lemma nclose_disjoint `{Countable A} I (x y : A) :
-  x ≠ y → nclose (ndot I x) ∩ nclose (ndot I y) = ∅.
-Proof.
-  intros Hxy; apply elem_of_equiv_empty_L; intros p; unfold nclose, ndot.
-  rewrite elem_of_intersection, !elem_coPset_suffixes; intros [[q ->] [q' Hq]].
-  apply Hxy, (injective encode), (injective encode_nat); revert Hq.
-  rewrite !(list_encode_cons (encode _)).
-  rewrite !(associative_L _), (injective_iff (++ _)%positive); simpl.
-  generalize (encode_nat (encode y)).
-  induction (encode_nat (encode x)); intros [|?] ?; f_equal'; naive_solver.
-Qed.
\ No newline at end of file