Cleaned up Pirouette types. Removed closure requirement for values.

CtrlLang.v

@@ -69,8 +69,8 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
   Inductive CtrlExprVal : CtrlExpr -> Prop :=
     RetVal : forall v, ExprVal v -> CtrlExprVal (Ret v)
   | UnitVal : CtrlExprVal Unit
-  | FunLocalVal : forall B, CtrlExprClosedAbove B 1 1 -> CtrlExprVal (FunLocal B)
-  | FunGlobalVal : forall B, CtrlExprClosedAbove B 2 0 -> CtrlExprVal (FunGlobal B).
+  | FunLocalVal : forall B, (* CtrlExprClosedAbove B 1 1 -> *) CtrlExprVal (FunLocal B)
+  | FunGlobalVal : forall B, (* CtrlExprClosedAbove B 2 0 ->  *)CtrlExprVal (FunGlobal B).
   Global Hint Constructors CtrlExprVal : CtrlExpr.
 
   Definition CtrlExprEqDec : forall E1 E2 : CtrlExpr, {E1 = E2} + {E1 <> E2}.
@@ -302,11 +302,6 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
   Proof using.
     intros E σ val; inversion val; subst; cbn; constructor.
     rewrite ExprClosedSubst; auto. apply ExprValuesClosed; auto.
-    rewrite CtrlExprClosedAbove_LocalSubst with (n := 1) (m := 1); auto.
-    intros k k_lt_1; unfold ExprUpSubst; destruct k; auto.
-    apply lt_S_n in k_lt_1. inversion k_lt_1.
-    rewrite CtrlExprClosedAbove_LocalSubst with (n := 2) (m := 0); auto.
-    intros k k_lt_0; inversion k_lt_0.
   Qed.
   
   Definition GlobalUpSubst : (nat -> CtrlExpr) -> nat -> CtrlExpr :=
@@ -439,12 +434,6 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
   Lemma CtrlExprValGlobalSubst : forall E σ, CtrlExprVal E -> CtrlExprVal (E [ceg| σ]).
   Proof using.
     intros E; induction E; intros σ val; inversion val; subst; cbn; constructor; auto.
-    - rewrite CtrlExprClosedAbove_GlobalSubst with (n := 1) (m := 1); auto.
-      intros k lt_k_1; destruct k; auto.
-      apply lt_S_n in lt_k_1; inversion lt_k_1.
-    - rewrite CtrlExprClosedAbove_GlobalSubst with (n := 2) (m := 0); auto.
-      intros k k_lt_2; destruct k; auto; destruct k; auto; cbn.
-      repeat apply lt_S_n in k_lt_2; inversion k_lt_2.
   Qed.
 
   Inductive CtrlExprMergeRel : CtrlExpr -> CtrlExpr -> CtrlExpr -> Prop :=

EndPointProjection.v

@@ -837,17 +837,9 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
     intros V l E H H0; inversion H; subst; cbn in H0.
     destruct (L.eq_dec l l0); subst; cbn in H0; inversion H0; subst; clear H0; 
       constructor; auto.
-
     destruct (L.eq_dec l l0); destruct (ProjectPirExpr C l) eqn:eq; subst;
       inversion H0; subst; clear H0; constructor; eauto.
-    eapply ProjectPirExprClosedAbove in H1; eauto.
-    destruct (L.eq_dec l0 l0) as [_ | neq]; [| destruct (neq eq_refl)]; auto.
-    apply CtrlExprClosedAboveGlobalRenaming with (n := 1) (m := 0).
-    eapply ProjectPirExprClosedAbove in H1; eauto.
-    destruct (L.eq_dec l0 l) as [e |_]; [destruct (n (eq_sym e))|]; auto.
-    intros a b H'; apply lt_n_S; auto.
     destruct (ProjectPirExpr C l) eqn:eq; inversion H0; subst; clear H0; constructor; auto.
-    eapply ProjectPirExprClosedAbove in H1; eauto.
   Qed.
 
   Inductive CompatibleRedices (l : Loc) : CtrlExprRedex -> C.Redex -> Prop :=
@@ -3187,22 +3179,18 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
     - destruct ls; [destruct (nempty eq_refl)|].
       destruct (eq l ltac:(left; reflexivity)) as [E [eq' val]]; ProjectPirExprDestructor.
       inversion val.
-    - destruct (eq ℓ (tn ℓ ltac:(left; reflexivity))) as [E [eq' val]]; ProjectPirExprDestructor; try discriminate.
-      inversion val; subst. constructor.
-      apply (ClosedSoundness C ls _ _ nempty).
-      intros l0 i; apply tn; right; auto.
-      intros l0 i; destruct (eq l0 i) as [E [eq' val']]; ProjectPirExprDestructor; try discriminate.
-      exists c; split; auto.
-      exists c0; split; auto. inversion val'; subst.
-      apply CtrlExprClosedAboveGlobalRenaming' with (ξ := S); auto.
-      apply lt_S_n.
+    (* - destruct (eq ℓ (tn ℓ ltac:(left; reflexivity))) as [E [eq' val]]; ProjectPirExprDestructor; try discriminate. *)
+    (*   inversion val; subst. constructor. *)
+    (*   apply (ClosedSoundness C ls _ _ nempty). *)
+    (*   intros l0 i; apply tn; right; auto. *)
+    (*   intros l0 i; destruct (eq l0 i) as [E [eq' val']]; ProjectPirExprDestructor; try discriminate. *)
+    (*   exists c; split; auto. *)
+    (*   exists c0; split; auto. inversion val'; subst. *)
+    (*   apply CtrlExprClosedAboveGlobalRenaming' with (ξ := S); auto. *)
+    (*   apply lt_S_n. *)
     - destruct ls; [destruct (nempty eq_refl)|].
       constructor; destruct (eq l ltac:(left; reflexivity)) as [E [eq' val]]; ProjectPirExprDestructor;
-        try discriminate. inversion val; subst.
-      apply (ClosedSoundness C (l :: ls) _ _ nempty tn).
-      intros l' i; destruct (eq l' i) as [E [eq' val']]; ProjectPirExprDestructor; try discriminate.
-      inversion val'.
-      exists c0; split; auto.
+        try discriminate. 
     - destruct ls; [destruct (nempty eq_refl)|].
       destruct (eq l ltac:(left; reflexivity)) as [E [eq' val]]; ProjectPirExprDestructor; try discriminate.
       inversion val.

Pirouette.v

@@ -1469,18 +1469,18 @@ Module Pirouette (Import E : LocalLang) (L : Locations) (Import SL : SyncLabels)
   Inductive PirExprVal : PirExpr -> Prop :=
   | ReturnVal : forall (l : Loc) (v : Expr),
       ExprVal v -> PirExprVal (Done l v)
-  | FunLocalVal : forall l C, PirExprClosedAbove (fun l' => if L.eq_dec l l' then 1 else 0) 1 C
-                         -> PirExprVal (FunLocal l C)
-  | FunGlobalVal : forall C, PirExprClosedAbove (fun _ => 0) 2 C ->
+  | FunLocalVal : forall l C, (* PirExprClosedAbove (fun l' => if L.eq_dec l l' then 1 else 0) 1 C *)
+                         (* ->  *)PirExprVal (FunLocal l C)
+  | FunGlobalVal : forall C, (* PirExprClosedAbove (fun _ => 0) 2 C -> *)
                         PirExprVal (FunGlobal C).
 
-  Lemma PirExprValuesClosed : forall C : PirExpr, PirExprVal C -> PirExprClosed C.
-  Proof.
-    intros C H; induction H; unfold PirExprClosed.
-    apply DoneClosedAbove; apply ExprValuesClosed in H; unfold ExprClosed in H; exact H.
-    apply FunLocalClosedAbove; auto.
-    apply FunGlobalClosedAbove; auto.
-  Qed.
+  (* Lemma PirExprValuesClosed : forall C : PirExpr, PirExprVal C -> PirExprClosed C. *)
+  (* Proof. *)
+  (*   intros C H; induction H; unfold PirExprClosed. *)
+  (*   apply DoneClosedAbove; apply ExprValuesClosed in H; unfold ExprClosed in H; exact H. *)
+  (*   apply FunLocalClosedAbove; auto. *)
+  (*   apply FunGlobalClosedAbove; auto. *)
+  (* Qed. *)
 
   Lemma PirExprValStableEquiv : forall C1 C2,
       PirExprVal C1 -> C1 ≡ C2 -> PirExprVal C2.

RestrictedSemantics.v

@@ -609,15 +609,15 @@ Module RestrictedSemantics (Import LL : LocalLang) (Import TLL : TypedLocalLang
     2: inversion H2.
     2-5,8,9: right.
     8,9: left; constructor; auto.
-    - destruct (ExprProgress e τ (Γ p) ltac:(assumption) ltac:(assumption));
+    - destruct (ExprProgress e τ (Γ ℓ) ltac:(assumption) ltac:(assumption));
         [left; constructor; auto | right].
-      destruct H0 as [e' step]; exists (RDone p e e'); exists (Done p e'); auto with PirExpr.
-    - destruct (ExprProgress e τ (Γ p) ltac:(assumption) ltac:(assumption))
+      destruct H0 as [e' step]; exists (RDone ℓ e e'); exists (Done ℓ e'); auto with PirExpr.
+    - destruct (ExprProgress e τ (Γ ℓ₁) ltac:(assumption) ltac:(assumption))
         as [eval | [e' step]];
         eexists; eexists; eauto with PirExpr.
-    - destruct (ExprProgress e bool (Γ p) ltac:(assumption) ltac:(assumption))
+    - destruct (ExprProgress e bool (Γ ℓ) ltac:(assumption) ltac:(assumption))
         as [eval | [e' step]];
-        [destruct (BoolInversion e (Γ p) ltac:(assumption) eval); subst|].
+        [destruct (BoolInversion e (Γ ℓ) ltac:(assumption) eval); subst|].
       all: eexists; eexists; eauto with PirExpr.
     - eexists; eexists; eauto with PirExpr.
     - destruct (IHtyp1 ltac:(assumption)) as [cval | [R [C' step]]].
@@ -625,7 +625,7 @@ Module RestrictedSemantics (Import LL : LocalLang) (Import TLL : TypedLocalLang
       all: eexists; eexists; eauto with PirExpr.
     - fold PirExprClosed in H4; specialize (IHtyp H4); destruct IHtyp.
       inversion H0; subst; inversion typ; subst.
-      destruct (ExprProgress _ _ _ H H6); [| destruct H2 as [e' step]];
+      destruct (ExprProgress _ _ _ H H6); [| destruct H1 as [e' step]];
         eexists; eexists; eauto with PirExpr.
       destruct H0 as [R [C' step]]; eexists; eexists; eauto with PirExpr.
     - specialize (IHtyp1 H3); specialize (IHtyp2 H4).

SoundlyTypedPirouette.v

@@ -9,7 +9,6 @@ Module SoundlyTypedPirouette (Import LL : LocalLang) (Import TLL : TypedLocalLan
        (L : Locations) (Import SL : SyncLabels).
   Include (TypedPirouette L LL TLL SL).
 
-
     Theorem Preservation:
       forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> PirTyp) (C : PirExpr) (τ : PirTyp),
         Γ;; Δ ⊢c C ::: τ -> forall (R : Redex) (B : list L.t) (C': PirExpr),
@@ -39,5 +38,3 @@ Module SoundlyTypedPirouette (Import LL : LocalLang) (Import TLL : TypedLocalLan
     Qed.
 
 End SoundlyTypedPirouette.
-
-