We define a semantic typing judgement on values and computations.
Values in VA and computations in CB are safe but not necessarily
syntactically well typed. However they behave like syntactically well typed
terms.
Set Implicit Arguments.
Require Import Omega Logic List.
Require Import Classes.Morphisms.
Import List Notations.
Require Export CBPV.Semantics CBPV.Terms CBPV.SyntacticTyping CBPV.Base.
Definition E' {n: nat} (C: comp n -> Prop) (c: comp n) := exists c', c ▷ c' /\ C c'.
Fixpoint V {n: nat} (A: valtype) (v: value n) :=
match A with
| zero => False
| one => v = u
| U B => exists c, v = <{ c }> /\ E' (C B) c
| Sigma A1 A2 => exists b v', v = inj b v' /\ V (if b then A1 else A2) v'
| A1 * A2 => exists v1 v2, v = pair v1 v2 /\ V A1 v1 /\ V A2 v2
end
with C {n: nat} (B: comptype) (c: comp n) :=
match B with
| cone => c = cu
| F A => exists v, c = ret v /\ V A v
| Pi B1 B2 => exists c1 c2, c = tuple c1 c2 /\ E' (C B1) c1 /\ E' (C B2) c2
| A → B => exists c', c = lambda c' /\ forall v, V A v -> E' (C B) (c'[v..])
end.
Notation E B c := (E' (C B) c).
Definition G {n m: nat} (Gamma : ctx n) (gamma: fin n -> value m) :=
forall i A, Gamma i = A -> V A (gamma i).
Definition val_semtype {n: nat} (Gamma: ctx n) (v: value n) (A: valtype) :=
forall m (gamma: fin n -> value m), G Gamma gamma -> V A (v[gamma]).
Notation "Gamma ⊫ v : A" := (val_semtype Gamma v A) (at level 80, v at level 99).
Definition comp_semtype {n: nat} (Gamma: ctx n) (c: comp n) (B: comptype) :=
forall m (gamma: fin n -> value m), G Gamma gamma -> E B (c[gamma]).
Notation "Gamma ⊨ c : B" := (comp_semtype Gamma c B) (at level 80, c at level 99).
Fixpoint V {n: nat} (A: valtype) (v: value n) :=
match A with
| zero => False
| one => v = u
| U B => exists c, v = <{ c }> /\ E' (C B) c
| Sigma A1 A2 => exists b v', v = inj b v' /\ V (if b then A1 else A2) v'
| A1 * A2 => exists v1 v2, v = pair v1 v2 /\ V A1 v1 /\ V A2 v2
end
with C {n: nat} (B: comptype) (c: comp n) :=
match B with
| cone => c = cu
| F A => exists v, c = ret v /\ V A v
| Pi B1 B2 => exists c1 c2, c = tuple c1 c2 /\ E' (C B1) c1 /\ E' (C B2) c2
| A → B => exists c', c = lambda c' /\ forall v, V A v -> E' (C B) (c'[v..])
end.
Notation E B c := (E' (C B) c).
Definition G {n m: nat} (Gamma : ctx n) (gamma: fin n -> value m) :=
forall i A, Gamma i = A -> V A (gamma i).
Definition val_semtype {n: nat} (Gamma: ctx n) (v: value n) (A: valtype) :=
forall m (gamma: fin n -> value m), G Gamma gamma -> V A (v[gamma]).
Notation "Gamma ⊫ v : A" := (val_semtype Gamma v A) (at level 80, v at level 99).
Definition comp_semtype {n: nat} (Gamma: ctx n) (c: comp n) (B: comptype) :=
forall m (gamma: fin n -> value m), G Gamma gamma -> E B (c[gamma]).
Notation "Gamma ⊨ c : B" := (comp_semtype Gamma c B) (at level 80, c at level 99).
Computations in CB have normal form
Lemma comp_nf {n: nat} (c: comp n) B: C B c -> nf c.
Proof.
destruct B; cbn; intros H; [ idtac | repeat (destruct H as [? H])..].
all: intuition; subst c; eauto.
Qed.
Proof.
destruct B; cbn; intros H; [ idtac | repeat (destruct H as [? H])..].
all: intuition; subst c; eauto.
Qed.
Computations in CB evaluate, explicitly CB ⊆ EB
Lemma comp_evaluates {n: nat} (c: comp n) B: C B c -> E B c.
Proof.
intros H; unfold E, E'; eexists c; split; [|assumption].
apply eval_bigstep; split; [reflexivity|]; eapply comp_nf; eassumption.
Qed.
Proof.
intros H; unfold E, E'; eexists c; split; [|assumption].
apply eval_bigstep; split; [reflexivity|]; eapply comp_nf; eassumption.
Qed.
EB is closed under reduction
Lemma closure_under_expansion {n: nat} (c c': comp n) B: c >* c' -> E B c' -> E B c.
Proof.
intros ? [c'' []] ; unfold E'; exists c''; split; eauto.
Qed.
Ltac expand := eapply closure_under_expansion.
Proof.
intros ? [c'' []] ; unfold E'; exists c''; split; eauto.
Qed.
Ltac expand := eapply closure_under_expansion.
Section compatibility_lemmas.
Variable (n: nat) (Gamma: ctx n) (A A1 A2: valtype) (B B1 B2: comptype).
Lemma compat_var i : Gamma i = A -> Gamma ⊫ var_value i : A.
Proof. firstorder. Qed.
Lemma compat_unit : Gamma ⊫ u : one.
Proof. now intros gamma H. Qed.
Lemma compat_pair v1 v2:
Gamma ⊫ v1 : A1 -> Gamma ⊫ v2 : A2 -> Gamma ⊫ pair v1 v2 : cross A1 A2.
Proof.
intros H1 H2 gamma H; specialize (H1 gamma H); specialize (H2 gamma H);
firstorder.
Qed.
Lemma compat_sum (b: bool) v:
Gamma ⊫ v : (if b then A1 else A2) -> Gamma ⊫ inj b v : Sigma A1 A2.
Proof.
intros H' gamma H; specialize (H' gamma H); firstorder.
Qed.
Lemma compat_thunk c:
Gamma ⊨ c : B -> Gamma ⊫ thunk c : U B.
Proof.
intros H' gamma H; specialize (H' gamma H); firstorder.
Qed.
Lemma compat_cone : Gamma ⊨ cu : cone.
Proof. intros m gamma H; cbn; unfold E'; eauto. Qed.
Lemma compat_lambda c:
A .: Gamma ⊨ c : B -> Gamma ⊨ lambda c : A → B.
Proof.
intros H' m gamma H; apply comp_evaluates; cbn; eexists; split; [reflexivity |].
intros v H1; pose (gamma' := v .: gamma); specialize (H' m gamma').
mp H'; [intros [i|]; cbn; eauto; intros ? ->; eauto |].
now asimpl.
Qed.
Lemma compat_letin c1 c2:
Gamma ⊨ c1 : F A -> A .: Gamma ⊨ c2 : B -> Gamma ⊨ $ <- c1; c2 : B.
Proof.
intros H' H'' m gamma H; destruct (H' m gamma H) as [c' [H1 H2]]; cbn.
destruct H2 as [v [-> H2]]; expand;
[ apply bigstep_soundness in H1; rewrite H1; reduce; reflexivity |].
pose (gamma' := v .: gamma); specialize (H'' m gamma').
mp H''; [intros [i|]; cbn; eauto; intros ? ->; eauto |].
now asimpl.
Qed.
Lemma compat_ret v:
Gamma ⊫ v : A -> Gamma ⊨ ret v : F A.
Proof.
intros H' m gamma H; specialize (H' m gamma H); apply comp_evaluates; firstorder.
Qed.
Lemma compat_app c v:
Gamma ⊨ c : A → B -> Gamma ⊫ v : A -> Gamma ⊨ c v : B.
Proof.
intros H1 H2 m gamma H; specialize (H1 m gamma H); specialize (H2 m gamma H); cbn.
destruct H1 as [? [H1 [c' [-> H3]]]]; apply bigstep_soundness in H1.
expand; [rewrite H1; reduce; reflexivity |].
eauto.
Qed.
Lemma compat_tuple c1 c2:
Gamma ⊨ c1 : B1 -> Gamma ⊨ c2 : B2 -> Gamma ⊨ tuple c1 c2 : Pi B1 B2.
Proof.
intros H' H'' m gamma H. apply comp_evaluates. cbn.
eexists; eexists; split; [reflexivity |].
split; cbn; eauto.
Qed.
Lemma compat_proj c b:
Gamma ⊨ c : Pi B1 B2 -> Gamma ⊨ proj b c : if b then B1 else B2.
Proof.
intros H m gamma H1; specialize (H m gamma H1).
destruct H as [c' [H2 [c1 [c2 [H4 [H5 H6]]]]]]; cbn;
apply bigstep_soundness in H2; destruct b;
expand.
all: try eassumption.
all: rewrite H2; subst c'; reduce; reflexivity.
Qed.
Lemma compat_force v:
Gamma ⊫ v : U B -> Gamma ⊨ v! : B.
Proof.
intros H' m gamma H; asimpl; specialize (H' m gamma H).
destruct H' as [c [-> H']]; now expand; [reduce; reflexivity|].
Qed.
Lemma compat_caseZ v:
Gamma ⊫ v : zero -> Gamma ⊨ caseZ v : B.
Proof.
intros H1 m gamma H; destruct (H1 m gamma H).
Qed.
Lemma compat_caseS v c1 c2:
Gamma ⊫ v : Sigma A1 A2 ->
A1 .: Gamma ⊨ c1 : B ->
A2 .: Gamma ⊨ c2 : B ->
Gamma ⊨ caseS v c1 c2 : B.
Proof.
intros H' H1 H2 m gamma H; specialize (H' m gamma H); cbn in H'.
destruct H' as [[] [v' [H3 H4]]].
all: asimpl; rewrite H3; expand; try (reduce; reflexivity).
all: pose (gamma' := v' .: gamma); specialize (H1 m gamma'); specialize (H2 m gamma').
all: [> mp H1 | mp H2].
1, 3: intros [i|]; cbn; eauto; intros ? ->; eauto.
all: now asimpl.
Qed.
Lemma compat_caseP v c:
Gamma ⊫ v : A1 * A2 ->
A2 .: (A1 .: Gamma) ⊨ c : B ->
Gamma ⊨ caseP v c : B.
Proof.
intros H' H1 m gamma H; specialize (H' m gamma H).
destruct H' as [v1 [v2 [H2 [H3 H4]]]]; asimpl.
rewrite H2; expand; [reduce; reflexivity |].
pose (gamma' := v2 .: (v1 .: gamma)); specialize (H1 m gamma').
mp H1; [intros [[]|] A0 ?; cbn; subst A0; eauto |].
now asimpl.
Qed.
End compatibility_lemmas.
Hint Resolve
compat_var compat_unit compat_pair compat_sum compat_thunk compat_cone
compat_lambda compat_letin compat_ret compat_app compat_tuple compat_proj
compat_force compat_caseZ compat_caseS compat_caseP : compatibility_lemmas.
Variable (n: nat) (Gamma: ctx n) (A A1 A2: valtype) (B B1 B2: comptype).
Lemma compat_var i : Gamma i = A -> Gamma ⊫ var_value i : A.
Proof. firstorder. Qed.
Lemma compat_unit : Gamma ⊫ u : one.
Proof. now intros gamma H. Qed.
Lemma compat_pair v1 v2:
Gamma ⊫ v1 : A1 -> Gamma ⊫ v2 : A2 -> Gamma ⊫ pair v1 v2 : cross A1 A2.
Proof.
intros H1 H2 gamma H; specialize (H1 gamma H); specialize (H2 gamma H);
firstorder.
Qed.
Lemma compat_sum (b: bool) v:
Gamma ⊫ v : (if b then A1 else A2) -> Gamma ⊫ inj b v : Sigma A1 A2.
Proof.
intros H' gamma H; specialize (H' gamma H); firstorder.
Qed.
Lemma compat_thunk c:
Gamma ⊨ c : B -> Gamma ⊫ thunk c : U B.
Proof.
intros H' gamma H; specialize (H' gamma H); firstorder.
Qed.
Lemma compat_cone : Gamma ⊨ cu : cone.
Proof. intros m gamma H; cbn; unfold E'; eauto. Qed.
Lemma compat_lambda c:
A .: Gamma ⊨ c : B -> Gamma ⊨ lambda c : A → B.
Proof.
intros H' m gamma H; apply comp_evaluates; cbn; eexists; split; [reflexivity |].
intros v H1; pose (gamma' := v .: gamma); specialize (H' m gamma').
mp H'; [intros [i|]; cbn; eauto; intros ? ->; eauto |].
now asimpl.
Qed.
Lemma compat_letin c1 c2:
Gamma ⊨ c1 : F A -> A .: Gamma ⊨ c2 : B -> Gamma ⊨ $ <- c1; c2 : B.
Proof.
intros H' H'' m gamma H; destruct (H' m gamma H) as [c' [H1 H2]]; cbn.
destruct H2 as [v [-> H2]]; expand;
[ apply bigstep_soundness in H1; rewrite H1; reduce; reflexivity |].
pose (gamma' := v .: gamma); specialize (H'' m gamma').
mp H''; [intros [i|]; cbn; eauto; intros ? ->; eauto |].
now asimpl.
Qed.
Lemma compat_ret v:
Gamma ⊫ v : A -> Gamma ⊨ ret v : F A.
Proof.
intros H' m gamma H; specialize (H' m gamma H); apply comp_evaluates; firstorder.
Qed.
Lemma compat_app c v:
Gamma ⊨ c : A → B -> Gamma ⊫ v : A -> Gamma ⊨ c v : B.
Proof.
intros H1 H2 m gamma H; specialize (H1 m gamma H); specialize (H2 m gamma H); cbn.
destruct H1 as [? [H1 [c' [-> H3]]]]; apply bigstep_soundness in H1.
expand; [rewrite H1; reduce; reflexivity |].
eauto.
Qed.
Lemma compat_tuple c1 c2:
Gamma ⊨ c1 : B1 -> Gamma ⊨ c2 : B2 -> Gamma ⊨ tuple c1 c2 : Pi B1 B2.
Proof.
intros H' H'' m gamma H. apply comp_evaluates. cbn.
eexists; eexists; split; [reflexivity |].
split; cbn; eauto.
Qed.
Lemma compat_proj c b:
Gamma ⊨ c : Pi B1 B2 -> Gamma ⊨ proj b c : if b then B1 else B2.
Proof.
intros H m gamma H1; specialize (H m gamma H1).
destruct H as [c' [H2 [c1 [c2 [H4 [H5 H6]]]]]]; cbn;
apply bigstep_soundness in H2; destruct b;
expand.
all: try eassumption.
all: rewrite H2; subst c'; reduce; reflexivity.
Qed.
Lemma compat_force v:
Gamma ⊫ v : U B -> Gamma ⊨ v! : B.
Proof.
intros H' m gamma H; asimpl; specialize (H' m gamma H).
destruct H' as [c [-> H']]; now expand; [reduce; reflexivity|].
Qed.
Lemma compat_caseZ v:
Gamma ⊫ v : zero -> Gamma ⊨ caseZ v : B.
Proof.
intros H1 m gamma H; destruct (H1 m gamma H).
Qed.
Lemma compat_caseS v c1 c2:
Gamma ⊫ v : Sigma A1 A2 ->
A1 .: Gamma ⊨ c1 : B ->
A2 .: Gamma ⊨ c2 : B ->
Gamma ⊨ caseS v c1 c2 : B.
Proof.
intros H' H1 H2 m gamma H; specialize (H' m gamma H); cbn in H'.
destruct H' as [[] [v' [H3 H4]]].
all: asimpl; rewrite H3; expand; try (reduce; reflexivity).
all: pose (gamma' := v' .: gamma); specialize (H1 m gamma'); specialize (H2 m gamma').
all: [> mp H1 | mp H2].
1, 3: intros [i|]; cbn; eauto; intros ? ->; eauto.
all: now asimpl.
Qed.
Lemma compat_caseP v c:
Gamma ⊫ v : A1 * A2 ->
A2 .: (A1 .: Gamma) ⊨ c : B ->
Gamma ⊨ caseP v c : B.
Proof.
intros H' H1 m gamma H; specialize (H' m gamma H).
destruct H' as [v1 [v2 [H2 [H3 H4]]]]; asimpl.
rewrite H2; expand; [reduce; reflexivity |].
pose (gamma' := v2 .: (v1 .: gamma)); specialize (H1 m gamma').
mp H1; [intros [[]|] A0 ?; cbn; subst A0; eauto |].
now asimpl.
Qed.
End compatibility_lemmas.
Hint Resolve
compat_var compat_unit compat_pair compat_sum compat_thunk compat_cone
compat_lambda compat_letin compat_ret compat_app compat_tuple compat_proj
compat_force compat_caseZ compat_caseS compat_caseP : compatibility_lemmas.
Theorem SemanticSoundness n (Gamma: ctx n):
(forall v A, Gamma ⊩ v : A -> Gamma ⊫ v : A) /\ (forall c B, Gamma ⊢ c : B -> Gamma ⊨ c : B).
Proof.
eapply mutind_value_computation_typing; eauto with compatibility_lemmas.
Qed.
Lemma ClosedSemanticSoundness:
(forall P A, null ⊩ P : A -> V A P) /\ (forall P A, null ⊢ P : A -> E A P).
Proof.
destruct (SemanticSoundness null) as [H1 H2].
split; intros P A; [intros H % H1 | intros H % H2].
all: specialize (H 0 ids); mp H; try now intros [].
all: now asimpl in H.
Qed.
Lemma Normal_nf M A:
null ⊢ M : A -> Normal step M -> nf M.
Proof.
destruct ClosedSemanticSoundness as [_ sem].
intros ? % sem N.
destruct X0. intuition.
eapply bigstep_soundness in H0.
inv H0. eapply comp_nf; eauto.
firstorder.
Qed.
(forall v A, Gamma ⊩ v : A -> Gamma ⊫ v : A) /\ (forall c B, Gamma ⊢ c : B -> Gamma ⊨ c : B).
Proof.
eapply mutind_value_computation_typing; eauto with compatibility_lemmas.
Qed.
Lemma ClosedSemanticSoundness:
(forall P A, null ⊩ P : A -> V A P) /\ (forall P A, null ⊢ P : A -> E A P).
Proof.
destruct (SemanticSoundness null) as [H1 H2].
split; intros P A; [intros H % H1 | intros H % H2].
all: specialize (H 0 ids); mp H; try now intros [].
all: now asimpl in H.
Qed.
Lemma Normal_nf M A:
null ⊢ M : A -> Normal step M -> nf M.
Proof.
destruct ClosedSemanticSoundness as [_ sem].
intros ? % sem N.
destruct X0. intuition.
eapply bigstep_soundness in H0.
inv H0. eapply comp_nf; eauto.
firstorder.
Qed.