Commit 40b4a580 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

New version of completeness with non-deterministic evaluation of app.

parent c1e752b1
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -9,6 +9,19 @@ Module Type Expression.
Parameter ExprValuesClosed : forall v : Expr, ExprVal v -> ExprClosed v.
Parameter ExprClosedBelowMono : forall m n e, m < n -> ExprClosedBelow m e -> ExprClosedBelow n e.
Parameter IsExprVal : Expr -> bool.
Parameter IsExprValSpec1 : forall v : Expr, ExprVal v -> IsExprVal v = true.
Parameter IsExprValSpec2 : forall v : Expr, IsExprVal v = true -> ExprVal v.
Lemma IsExprValSpec3 : forall e : Expr, ~ ExprVal e -> IsExprVal e = false.
Proof using.
intros e nv; destruct (IsExprVal e) eqn:eq; auto.
apply IsExprValSpec2 in eq; exfalso; apply nv; auto.
Qed.
Lemma IsExprValSpec4 : forall e : Expr, IsExprVal e = false -> ~ ExprVal e.
Proof using.
intros e eq val; apply IsExprValSpec1 in val; rewrite val in eq; inversion eq.
Qed.
Parameter ExprSubst : Expr -> (nat -> Expr) -> Expr.
Parameter ExprRename : Expr -> (nat -> nat) -> Expr.
Notation "e [e| sigma ]" := (ExprSubst e sigma) (at level 29).
......@@ -77,4 +90,16 @@ Module Type Expression.
Parameter ExprStep : Expr -> Expr -> Prop.
Parameter NoExprStepFromVal : forall v, ExprVal v -> forall e, ~ ExprStep v e.
Parameter ExprOpenVal : Expr -> Prop.
Parameter OpenValRename :
forall e ξ, ExprOpenVal e -> ExprOpenVal (e e|ξ⟩).
Parameter OpenValSubst :
forall e σ, ExprOpenVal e -> (forall n, ExprOpenVal (σ n)) -> ExprOpenVal (e [e|σ]).
Parameter OpenValFromSubst : forall e σ, ExprOpenVal (e [e| σ]) -> ExprOpenVal e.
Parameter ValToOpenVal : forall e, ExprVal e -> ExprOpenVal e.
Parameter VarToOpenVal : forall n, ExprOpenVal (ExprVar n).
Parameter NoStepFromOpenVal : forall e1, ExprOpenVal e1 -> forall e2, ~ ExprStep e1 e2.
Parameter IsOpenVal : Expr -> bool.
Parameter IsOpenValSpec : forall e, IsOpenVal e = true <-> ExprOpenVal e.
End Expression.
......@@ -54,6 +54,15 @@ Module LambdaCalc <: Expression.
| AbsVal : forall (τ : SimpleType) (e : LC), LCClosedBelow 1 e -> LCVal (abs τ e).
Definition ExprVal := LCVal.
Inductive LCOpenVal : LC -> Prop :=
| varOVal : forall n, LCOpenVal (var n)
| ttOVal : LCOpenVal ttLC
| ffOVal : LCOpenVal ffLC
| zeroOVal : LCOpenVal zero
| succOVal : forall e : Expr, LCOpenVal e -> LCOpenVal (succ e)
| AbsOVal : forall (τ : SimpleType) (e : LC), LCOpenVal (abs τ e).
Definition ExprOpenVal := LCOpenVal.
Lemma ExprValuesClosed : forall v : Expr, ExprVal v -> ExprClosed v.
Proof.
intros v val_v; induction val_v; unfold ExprClosed; simpl; auto.
......@@ -291,6 +300,74 @@ Module LambdaCalc <: Expression.
apply Lt.lt_le_S in l. apply Lt.le_lt_or_eq in l; destruct l; subst; eauto.
Qed.
Fixpoint IsClosedBelow (e : Expr) (n : nat) : bool :=
match e with
| var m => if m <? n then true else false
| ttLC => true
| ffLC => true
| zero => true
| succ e' => IsClosedBelow e' n
| fixP e' => IsClosedBelow e' n
| ite b e1 e2 => IsClosedBelow b n && IsClosedBelow e1 n && IsClosedBelow e2 n
| app e1 e2 => IsClosedBelow e1 n && IsClosedBelow e2 n
| abs τ e' => IsClosedBelow e' (S n)
end.
Lemma IsClosedBelowSpec : forall e n, IsClosedBelow e n = true <-> LCClosedBelow n e.
Proof using.
intro e; induction e; intro m; cbn; split; intro H; auto; try discriminate.
1,2: destruct m; cbn in *;
try match goal with
| [ |-context[?a <=? ?b]] => destruct (a <=? b)
end;
auto; try discriminate.
all: repeat match goal with
| [ H: (andb _ _) = true |- _ ] => apply andb_prop in H
| [ |- andb _ _ = true ] => apply andb_true_intro
| [ H : _ /\ _ |- _ ] => destruct H
| [|- _ /\ _ ] => split
| [IH : forall n, IsClosedBelow ?e n = true <-> LCClosedBelow n ?e,
H : IsClosedBelow ?e ?m = true |- LCClosedBelow ?m ?e ] =>
apply ((proj1 (IH m)) H)
| [IH : forall n, IsClosedBelow ?e n = true <-> LCClosedBelow n ?e,
H : LCClosedBelow ?m ?e |- IsClosedBelow ?e ?m = true ] =>
apply ((proj2 (IH m)) H)
end.
Qed.
Fixpoint IsExprVal (e : Expr) : bool :=
match e with
| var x => false
| ttLC => true
| ffLC => true
| zero => true
| succ e => IsExprVal e
| fixP e => false
| ite e1 e2 e3 => false
| app e1 e2 => false
| abs τ e1 => IsClosedBelow e1 1
end.
Lemma IsExprValSpec1 : forall v : Expr, ExprVal v -> IsExprVal v = true.
Proof using.
intros v val; induction val; cbn; auto.
apply IsClosedBelowSpec; auto.
Qed.
Lemma IsExprValSpec2 : forall v : Expr, IsExprVal v = true -> ExprVal v.
Proof using.
intros v eq; induction v; cbn in *; try discriminate; constructor; auto.
apply IHv; auto. apply IsClosedBelowSpec; auto.
Qed.
Lemma IsExprValSpec3 : forall e : Expr, ~ ExprVal e -> IsExprVal e = false.
Proof using.
intros e nv; destruct (IsExprVal e) eqn:eq; auto.
apply IsExprValSpec2 in eq; exfalso; apply nv; auto.
Qed.
Lemma IsExprValSpec4 : forall e : Expr, IsExprVal e = false -> ~ ExprVal e.
Proof using.
intros e eq val; apply IsExprValSpec1 in val; rewrite val in eq; inversion eq.
Qed.
Theorem NoExprStepFromVal : forall v, ExprVal v -> forall e, ~ ExprStep v e.
Proof using.
intros v; induction v; intros val_v e step; inversion val_v; subst;
......@@ -300,4 +377,64 @@ Module LambdaCalc <: Expression.
Theorem boolSeperation : tt <> ff. discriminate. Qed.
Theorem OpenValRename : forall e ξ, ExprOpenVal e -> ExprOpenVal (e e|ξ⟩).
Proof using.
intro e; induction e; cbn; intros ξ val_e; inversion val_e; subst;
constructor; auto.
apply IHe; auto.
Qed.
Theorem OpenValSubst : forall e σ,
ExprOpenVal e -> (forall n, ExprOpenVal (σ n)) -> ExprOpenVal (e [e| σ]).
Proof using.
intro e; induction e; cbn; intros σ val_e val_σ; auto; inversion val_e; subst.
constructor; apply IHe; auto.
constructor.
Qed.
Theorem OpenValFromSubst : forall e σ, ExprOpenVal (e [e| σ]) -> ExprOpenVal e.
Proof using.
intro e; induction e; cbn; intros σ val; inversion val; subst; constructor.
eapply IHe; eauto.
Qed.
Theorem ValToOpenVal : forall e, ExprVal e -> ExprOpenVal e.
Proof using.
intro e; induction e; intro val; inversion val; subst; constructor.
apply IHe; auto.
Qed.
Theorem VarToOpenVal : forall n, ExprOpenVal (ExprVar n).
Proof using.
intro n; constructor.
Qed.
Theorem NoStepFromOpenVal : forall e1, ExprOpenVal e1 -> forall e2, ~ ExprStep e1 e2.
Proof using.
intros e1; induction e1; intros val e2 step; inversion val; subst;
inversion step; subst.
apply IHe1 in H1; auto.
Qed.
Fixpoint IsOpenVal (e : Expr) : bool :=
match e with
| var x => true
| ttLC => true
| ffLC => true
| zero => true
| succ e => IsOpenVal e
| fixP x => false
| ite x x0 x1 => false
| app x x0 => false
| abs x x0 => true
end.
Theorem IsOpenValSpec : forall e, IsOpenVal e = true <-> ExprOpenVal e.
Proof using.
intro e; induction e; cbn; split; intro H; auto; try discriminate; try (inversion H; fail).
all: try (constructor; auto; fail).
- apply IHe in H; constructor; auto.
- inversion H; subst. apply IHe in H1; auto.
Qed.
End LambdaCalc.
......@@ -5,8 +5,6 @@ Require Import Coq.Classes.RelationClasses.
Require Import Coq.Lists.SetoidList.
Require Import Coq.FSets.FMapInterface.
Require Import Coq.Program.Wf.
From Equations Require Import Equations.
Require Import Psatz.
(* Maps keyed by locations *)
Module Type LocationMap (L : Locations).
......
......@@ -5,9 +5,6 @@ Require Import Coq.FSets.FMapInterface.
Require Import Coq.Program.Wf.
Require Import Coq.Sorting.Permutation.
Require Import Coq.Sorting.Mergesort.
From Equations Require Import Equations.
Require Import Psatz.
(*
A module describing the properties of locations in
......
......@@ -13,8 +13,6 @@ Require Import Coq.Bool.Bool.
Require Import Psatz.
Require Import Coq.Program.Equality.
From Equations Require Import Equations.
Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression E) (L : Locations).
Include (TypedChoreography L E TE). (* Note that a lot of results don't rely on typing, but the module system forces me to include it from the beginning *)
Include ListNotations.
......@@ -55,10 +53,10 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
RChorStep (RDefLocal l v) nil (DefLocal l (Done l v) C2) (C2 [ce| ValueSubst l v])
| AppLocalFunStep : forall l C1 C2 e R,
RChorStep R [] C1 C2 ->
RChorStep R [] (AppLocal l C1 e) (AppLocal l C2 e)
RChorStep (RFun R) [] (AppLocal l C1 e) (AppLocal l C2 e)
| AppLocalExprStep : forall l C e1 e2,
ExprStep e1 e2 ->
RChorStep (RAppLocalE l e1 e2) [] (AppLocal l (RecLocal l C) e1) (AppLocal l (RecLocal l C) e2)
RChorStep (RAppLocalE l e1 e2) [] (AppLocal l C e1) (AppLocal l C e2)
| AppLocalValStep : forall l C v,
ExprVal v ->
RChorStep (RAppLocal l v) []
......@@ -66,10 +64,10 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
(C [ce| ValueSubst l v] [c| AppLocalSubst l C])
| AppGlobalFunStep : forall C11 C12 C2 R,
RChorStep R [] C11 C12 ->
RChorStep R [] (AppGlobal C11 C2) (AppGlobal C12 C2)
RChorStep (RFun R) [] (AppGlobal C11 C2) (AppGlobal C12 C2)
| AppGlobalArgStep : forall C1 C21 C22 R,
RChorStep R [] C21 C22 ->
RChorStep R [] (AppGlobal (RecGlobal C1) C21) (AppGlobal (RecGlobal C1) C22)
RChorStep (RArg R) [] (AppGlobal C1 C21) (AppGlobal C1 C22)
| AppGlobalValStep : forall C1 C2,
ChorVal C2 ->
RChorStep RAppGlobal []
......@@ -334,14 +332,16 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
apply RetEquivInversion in equiv1; subst; eexists; split; eauto with Chor.
all: try (exfalso; eapply NoIStepInList; eauto; eauto with Chor; InList; fail).
all: try (eexists; split; [repeat econstructor |]; eauto with Chor; try NotInList; auto; try (eapply RStepRearrange; eauto with Chor; intros q; split; unfold In; intro i; tauto); fail).
- apply RecLocalEquivInversion in equiv0; destruct equiv0 as [C' [eq eqv]]; subst.
exists (AppLocal l (RecLocal l C') e2); split; auto with Chor.
(* - apply RecLocalEquivInversion in equiv0; destruct equiv0 as [C' [eq eqv]]; subst. *)
(* - apply RecLocalEquivInversion in equiv0; destruct equiv0 as [C' [eq eqv]]; subst. *)
(* exists (AppLocal l (RecLocal l C') e2); split; auto with Chor. *)
- apply RecLocalEquivInversion in equiv0; destruct equiv0 as [C' [eq eqv]]; subst.
exists (C' [ce|ValueSubst l e] [c|AppLocalSubst l C'] ); split; auto with Chor.
apply WeakSubstExt; [apply EquivStableExprSubst|]; auto.
intro n; destruct n; cbn; auto with Chor.
- apply RecGlobalEquivInversion in equiv1; destruct equiv1 as [C1' [eq equiv1]]; subst.
exists (AppGlobal (RecGlobal C1') C); split; auto with Chor.
(* - apply RecGlobalEquivInversion in equiv1; destruct equiv1 as [C1' [eq equiv1]]; subst. *)
(* exists (AppGlobal (RecGlobal C1') C12); split; auto with Chor. *)
- apply RecGlobalEquivInversion in equiv1; destruct equiv1 as [C1' [eq equiv1]]; subst.
exists (C1' [c| AppGlobalSubst C1' C22]); split; auto with Chor.
apply AppGlobalValStep; auto.
......@@ -413,7 +413,7 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
StdChorStep (AppLocal l C1 e) (AppLocal l C2 e)
| StdAppLocalArgStep : forall l C e1 e2,
ExprStep e1 e2 ->
StdChorStep (AppLocal l (RecLocal l C) e1) (AppLocal l (RecLocal l C) e2)
StdChorStep (AppLocal l C e1) (AppLocal l C e2)
| StdAppLocalStep : forall l C v,
ExprVal v ->
StdChorStep (AppLocal l (RecLocal l C) v) (C [ce|ValueSubst l v] [c|AppLocalSubst l C])
......@@ -422,7 +422,7 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
-> StdChorStep (AppGlobal C1 C2) (AppGlobal C1' C2)
| StdAppGlobalArgStep : forall (C1 C2 C2' : Chor),
StdChorStep C2 C2'
-> StdChorStep (AppGlobal (RecGlobal C1) C2) (AppGlobal (RecGlobal C1) C2')
-> StdChorStep (AppGlobal C1 C2) (AppGlobal C1 C2')
| StdAppGlobalStep : forall (C1 C2 : Chor),
ChorVal C2 ->
StdChorStep (AppGlobal (RecGlobal C1) C2) (C1 [c|AppGlobalSubst C1 C2])
......@@ -442,11 +442,13 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
- destruct IHstdstep as [R [C2' [equiv step]]].
exists R; exists (LetLocal l new C2' fby C2); split; auto with Chor.
- destruct IHstdstep as [R [C2' [equiv step]]].
exists R; exists (AppLocal l C2' e); split; auto with Chor.
exists (RFun R); exists (AppLocal l C2' e); split; auto with Chor.
(* - exists (RAppLocalE l e1 e2); exists (AppLocal l C e2); split; auto with Chor. *)
(* constructor. *)
- destruct IHstdstep as [R [C2' [equiv step]]].
exists R; exists (AppGlobal C2' C2); split; auto with Chor.
exists (RFun R); exists (AppGlobal C2' C2); split; auto with Chor.
- destruct IHstdstep as [R [C2'' [equiv step]]].
exists R; exists (AppGlobal (RecGlobal C1) C2''); split; auto with Chor.
exists (RArg R); exists (AppGlobal C1 C2''); split; auto with Chor.
- destruct IHstdstep as [R [C2'' [equiv step]]].
destruct (EquivSimulation C1' C1 ltac:(auto with Chor) R [] C2'' step) as [C2''' [step' equiv']].
exists R; exists C2'''; split; auto with Chor. transitivity C2'; auto; transitivity C2''; auto.
......@@ -462,13 +464,13 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
| SyncOnTop : forall p d q C, RedexOnTop (RSync p d q) (Sync p d q C)
| IDefLocalOntop : forall l C1 C2 R, RedexOnTop R C1 -> RedexOnTop R (DefLocal l C1 C2)
| DefLocalOnTop : forall l e C, RedexOnTop (RDefLocal l e) (DefLocal l (Done l e) C)
| AppLocalEOnTop : forall l e1 e2 C, RedexOnTop (RAppLocalE l e1 e2) (AppLocal l (RecLocal l C) e1)
| AppLocalEOnTop : forall l e1 e2 C, RedexOnTop (RAppLocalE l e1 e2) (AppLocal l C e1)
| AppLocalOnTop : forall l C e, RedexOnTop (RAppLocal l e) (AppLocal l (RecLocal l C) e)
| AppGlobalOnTop : forall C1 C2,
ChorVal C2 -> RedexOnTop RAppGlobal (AppGlobal (RecGlobal C1) C2)
| LocalFunOnTop : forall R l C e, RedexOnTop R C -> RedexOnTop R (AppLocal l C e)
| GlobalFunOnTop : forall R C1 C2, RedexOnTop R C1 -> RedexOnTop R (AppGlobal C1 C2)
| GlobalArgOnTop : forall R C1 C2, RedexOnTop R C2 -> RedexOnTop R (AppGlobal (RecGlobal C1) C2).
| LocalFunOnTop : forall R l C e, RedexOnTop R C -> RedexOnTop (RFun R) (AppLocal l C e)
| GlobalFunOnTop : forall R C1 C2, RedexOnTop R C1 -> RedexOnTop (RFun R) (AppGlobal C1 C2)
| GlobalArgOnTop : forall R C1 C2, RedexOnTop R C2 -> RedexOnTop (RArg R) (AppGlobal C1 C2).
Global Hint Constructors RedexOnTop : Chor.
Ltac ListClean :=
......@@ -551,7 +553,7 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
- exists (DefLocal l C C2); exists (DefLocal l C0 C2); split; [|split;[|split]]; auto with Chor.
- exists (AppLocal l C e); exists (AppLocal l C0 e); split; [|split;[|split]]; auto with Chor.
- exists (AppGlobal C C2); exists (AppGlobal C0 C2); split; [|split;[|split]]; auto with Chor.
- exists (AppGlobal (RecGlobal C1) C); exists (AppGlobal (RecGlobal C1) C0);
- exists (AppGlobal C1 C); exists (AppGlobal C1 C0);
split; [|split;[|split]]; auto with Chor.
- induction ontop.
all: inversion step0; subst; ListClean.
......@@ -580,8 +582,8 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
- apply NoIfEIStepInList in rstep1; [destruct rstep1 | left; reflexivity].
- apply NoIfTTStepInList in rstep1; [destruct rstep1 | left; reflexivity].
- apply NoIfFFStepInList in rstep1; [destruct rstep1 | left; reflexivity].
- inversion H1; subst; inversion rstep.
- inversion H1.
(* - inversion H1; subst; inversion rstep. *)
(* - inversion H1. *)
- apply NoSyncStepInList1 in rstep; [destruct rstep | left; reflexivity].
Qed.
......
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