Commit 16090ca5 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Changed some names that still referenced ExprSubst.

parent efdccc00
......@@ -1094,7 +1094,7 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
eapply UnmergeRelClosed; eauto.
Qed.
Theorem MergeExprSubst : forall E1 E2 E σ,
Theorem MergeLocalSubst : forall E1 E2 E σ,
CtrlExprMerge E1 E2 = Some E ->
CtrlExprMerge (E1 [cel| σ]) (E2 [cel| σ]) = Some (E [cel| σ]).
Proof using.
......@@ -1168,7 +1168,7 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
end; cbn; auto.
Qed.
Theorem MergeSubst : forall E1 E2 E σ,
Theorem MergeGlobalSubst : forall E1 E2 E σ,
CtrlExprMerge E1 E2 = Some E ->
CtrlExprMerge (E1 [ceg| σ]) (E2 [ceg| σ]) = Some (E [ceg| σ]).
Proof using.
......@@ -1766,14 +1766,14 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
lazymatch goal with
| [ _ : CtrlExprMerge (E1 [cel| σ]) (E2 [cel| σ]) = Some (E3 [cel| σ])
|- _ ] => fail
| _ => pose proof (MergeExprSubst E1 E2 E3 σ H)
| _ => pose proof (MergeLocalSubst E1 E2 E3 σ H)
end
| [ H : CtrlExprMerge ?E1 ?E2 = Some ?E3,
_ : context[?E1 [ceg| ?σ]] |- _ ] =>
lazymatch goal with
| [ _ : CtrlExprMerge (E1 [ceg| σ]) (E2 [ceg| σ]) = Some (E3 [ceg| σ])
|- _ ] => fail
| _ => pose proof (MergeSubst E1 E2 E3 σ H)
| _ => pose proof (MergeGlobalSubst E1 E2 E3 σ H)
end
| [ H : CtrlExprMerge ?E1 ?E2 = Some ?E3,
H' : CtrlExprMerge ?E1 ?E2 = Some ?E4 |- _ ] =>
......@@ -1961,26 +1961,26 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
lazymatch goal with
| [ _ : CtrlExprMerge (E1 [cel| σ]) (E2 [cel| σ]) = Some (E3 [cel| σ])
|- _ ] => fail
| _ => pose proof (MergeExprSubst E1 E2 E3 σ H)
| _ => pose proof (MergeLocalSubst E1 E2 E3 σ H)
end
| [ H : CtrlExprMerge ?E1 ?E2 = Some ?E3 |- context[?E1 [cel| ?σ]]] =>
lazymatch goal with
| [ _ : CtrlExprMerge (E1 [cel| σ]) (E2 [cel| σ]) = Some (E3 [cel| σ])
|- _ ] => fail
| _ => pose proof (MergeExprSubst E1 E2 E3 σ H)
| _ => pose proof (MergeLocalSubst E1 E2 E3 σ H)
end
| [ H : CtrlExprMerge ?E1 ?E2 = Some ?E3,
_ : context[?E1 [ceg| ?σ]] |- _ ] =>
lazymatch goal with
| [ _ : CtrlExprMerge (E1 [ceg| σ]) (E2 [ceg| σ]) = Some (E3 [ceg| σ])
|- _ ] => fail
| _ => pose proof (MergeSubst E1 E2 E3 σ H)
| _ => pose proof (MergeGlobalSubst E1 E2 E3 σ H)
end
| [ H : CtrlExprMerge ?E1 ?E2 = Some ?E3 |- context[?E1 [ceg| ?σ]]] =>
lazymatch goal with
| [ _ : CtrlExprMerge (E1 [ceg| σ]) (E2 [ceg| σ]) = Some (E3 [ceg| σ])
|- _ ] => fail
| _ => pose proof (MergeSubst E1 E2 E3 σ H)
| _ => pose proof (MergeGlobalSubst E1 E2 E3 σ H)
end
| [ H : CtrlExprMerge ?E1 ?E2 = Some ?E3,
H' : CtrlExprMerge ?E1 ?E2 = Some ?E4 |- _ ] =>
......@@ -2237,12 +2237,12 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
- exists (E1 [cel| ValSubst v]); exists (E2 [cel| ValSubst v]); split; [|split];
auto with CtrlExpr.
apply CtrlExprMergeRelSpec1 in H3; apply CtrlExprMergeRelSpec2;
rewrite MergeExprSubst with (E := E); auto.
rewrite MergeLocalSubst with (E := E); auto.
- inversion H4; subst.
exists (E21 [cel| ValSubst v]); exists (E22 [cel| ValSubst v]); split; [|split];
auto with CtrlExpr.
apply CtrlExprMergeRelSpec1 in H5; apply CtrlExprMergeRelSpec2;
rewrite MergeExprSubst with (E := E2); auto.
rewrite MergeLocalSubst with (E := E2); auto.
- inversion H3; subst.
exists ((F [cel| ValSubst v]) [ceg|FunLocalSubst F]);
exists ((F [cel| ValSubst v]) [ceg| FunLocalSubst F]);
......@@ -3170,7 +3170,7 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
Surprisingly, if something is less-nondetermistic than a value, then it must be
equal to the value.
*)
Lemma LessNondetExprSubst : forall E1 E2 σ,
Lemma LessNondetLocalSubst : forall E1 E2 σ,
LessNondet E1 E2 ->
LessNondet (E1 [cel| σ]) (E2 [cel| σ]).
Proof using.
......@@ -3184,7 +3184,7 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
intros E1 E2 ξ lnd; revert ξ; induction lnd; intro ξ; cbn; eauto with CtrlExpr.
Qed.
Lemma LessNondetSubst : forall E1 E2 σ,
Lemma LessNondetGlobalSubst : forall E1 E2 σ,
LessNondet E1 E2 ->
LessNondet (E1 [ceg| σ]) (E2 [ceg| σ]).
Proof using.
......@@ -3219,11 +3219,11 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
inversion lnd; subst; try (eexists; split; eauto with CtrlExpr; fail).
- exists (If e2 E0 E22); split; eauto with CtrlExpr.
- exists (Send l e2 E2); split; eauto with CtrlExpr.
- exists (E2 [cel|ValSubst v]); split; eauto with CtrlExpr. apply LessNondetExprSubst; auto.
- exists (E2 [cel|ValSubst v]); split; eauto with CtrlExpr. apply LessNondetLocalSubst; auto.
- destruct (IHstep E0 H1) as [E2' [lnd' step']].
exists (LetRet E2' E22); split; auto with CtrlExpr.
- inversion H2; subst. exists (E22 [cel|ValSubst v]); split; auto with CtrlExpr.
apply LessNondetExprSubst; auto.
apply LessNondetLocalSubst; auto.
- destruct (IHstep E2 H2) as [E22 [lnd' step']].
exists (AppLocal E22 e); split; auto with CtrlExpr.
- exists (AppLocal E2 e2); split; auto with CtrlExpr.
......@@ -3279,10 +3279,10 @@ Module CtrlLang (Import LL : LocalLang) (L : Locations) (LM : LocationMap L) (Im
end; try (eexists; split; eauto with CtrlExpr; fail).
- exists (If e2 E11 E12); split; auto with CtrlExpr.
- exists (Send l e2 E1); split; auto with CtrlExpr.
- exists (E1 [cel|ValSubst v]); split; auto with CtrlExpr; apply LessNondetExprSubst; auto.
- exists (E1 [cel|ValSubst v]); split; auto with CtrlExpr; apply LessNondetLocalSubst; auto.
- exists (LetRet E0 E12); split; auto with CtrlExpr.
- inversion H3; subst. exists (E12[cel|ValSubst v]); split; auto with CtrlExpr.
apply LessNondetExprSubst; auto.
apply LessNondetLocalSubst; auto.
- exists (AppLocal E2 e); split; auto with CtrlExpr.
- exists (AppLocal E1 e2); split; auto with CtrlExpr.
- inversion H2; subst.
......
......@@ -285,7 +285,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
[|destruct (n eq_refl)];
unfold ExprUpSubst
end; try reflexivity.
- erewrite MergeExprSubst; eauto.
- erewrite MergeLocalSubst; eauto.
- destruct d; inversion eq; subst; auto.
- rewrite LocalSubstGlobalRenameComm; reflexivity.
- rewrite LocalSubstGlobalRenameComm; reflexivity.
......@@ -341,7 +341,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
H : EPP ?C ?l = Some ?E |- context[EPP (C.PirExprRename ?C ?ξ) ?l]] =>
rewrite (IH l E ξ H)
end.
- repeat rewrite GlobalRenameSpec. apply MergeSubst; auto.
- repeat rewrite GlobalRenameSpec. apply MergeGlobalSubst; auto.
- repeat rewrite CtrlExprGlobalRenameFusion; cbn. reflexivity.
- unfold C.PirExprUpRename. unfold UpRename. reflexivity.
- repeat rewrite CtrlExprGlobalRenameFusion; cbn.
......@@ -423,7 +423,7 @@ Module EndPointProjection (Import LL : LocalLang) (L : Locations) (LM : Location
end
end.
- apply eq_σ.
- apply MergeSubst; auto.
- apply MergeGlobalSubst; auto.
- apply f_equal.
rewrite CtrlExprGlobalRenameSubstFusion.
rewrite CtrlExprGlobalSubstRenameFusion. cbn.
......
......@@ -47,8 +47,8 @@ The following table refers to theorems found only in Appendix G of the technical
| Merge is Commutative | Theorem 15 (Part 2) | CtrlLanguage.v | MergeComm |
| Merge is Associative | Theorem 15 (Part 3) | CtrlLanguage.v | MergeAssoc and MergeAssocNone |
| Merge Preserves Free Vars | Theorem 16 (Part 1) | CtrlLanguage.v | MergeClosed |
| Merge Preserves Local Substitution | Theorem 16 (Part 2) | CtrlLanguage.v | MergeExprSubst |
| Merge Preserves Global Substitution | Theorem 16 (Part 3) | CtrlLanguage.v | MergeSubst |
| Merge Preserves Local Substitution | Theorem 16 (Part 2) | CtrlLanguage.v | MergeLocalSubst |
| Merge Preserves Global Substitution | Theorem 16 (Part 3) | CtrlLanguage.v | MergeGlobalSubst |
| Merge Preserves Values | Theorem 16 (Part 4) | CtrlLanguage.v | MergeCtrlExprVals and MergeRelToVal |
| Merge Preserves Reduction | Theorem 17 | CtrlLanguage.v | MergeStep' and MergeStep'Exists |
| Merge Creates Reduction | Theorem 17 | CtrlLanguage.v | UnmergeRelStep |
......@@ -60,8 +60,8 @@ The following table refers to theorems found only in Appendix G of the technical
| LND is Reflexive | Theorem 19 (Part 1) | CtrlLanguage.v | LessNondetRefl |
| LND is Antisymmetric | Theorem 19 (Part 2) | CtrlLanguage.v | LessNondetAntisym |
| LND is Transitive | Theorem 19 (Part 3) | CtrlLanguage.v | LessNondetTrans |
| LND Preserves Local Substitition | Theorem 20 (Part 1) | CtrlLanguage.v | LessNondetExprSubst |
| LND Preserves Global Substitition | Theorem 20 (Part 2) | CtrlLanguage.v | LessNondetSubst |
| LND Preserves Local Substitition | Theorem 20 (Part 1) | CtrlLanguage.v | LessNondetLocalSubst |
| LND Preserves Global Substitition | Theorem 20 (Part 2) | CtrlLanguage.v | LessNondetGlobalSubst |
| Merging Creates LND | Thoerem 20 (Part 3) | CtrlLanguage.v | MergeLessNondet |
| Merging Preserves LND | Theorem 20 (Part 4) | CtrlLanguage.v | LessNondetMerge |
| LND is Reflexivity on Values | Theorem 20 (Part 5) | CtrlLanguage.v | LessNondetVals |
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment