Commit 68553641 authored by Paul Wild's avatar Paul Wild
Browse files

move definition of contexts to Language.v/Lib.v, 

move soundness proofs to Binary{Typed}/Compatibility.v
parent 88618d6c

.gitignore

+3 −0
Original line number Diff line number Diff line
@@ -2,3 +2,6 @@ 
*.v.d

*.vo

*.swp

project/coqdoc.css

project/Makefile.bak

project/html

project/Binary/Compatibility.v

+60 −0
Original line number Diff line number Diff line
@@ -531,3 +531,63 @@ Proof. 
  induction 1; subst; eauto using types_closed_t with compat.

Qed.





(** ** Soundness

    

    TODO



    Now the proof of the compatibility lemma becomes a simple matter of combining

    the previous compatibility lemmas and the Fundamental property together,

    using the closedness lemmas to deal with any closedness conditions that arise.

*)



Lemma compat_cont : forall C k k' Γ Γ' t t' e1 e2

    (HCT: ctypes C (k, Γ, t) (k', Γ', t'))

    (HL: logrel k Γ e1 e2 t),

  logrel k' Γ' (csubst C e1) (csubst C e2) t'.

Proof.

  induction C; intros; simpl; inversion HCT; subst;

    eauto 6 using Fundamental, ctypes_closed_t, types_closed_t with compat.

Qed.



(** Definition of contextual approximation: *)



Definition terminates e := exists (v : val), e ↦* v.

Definition contapprox k Γ e1 e2 t :=

  forall C t'

    (HCT : ctypes C (k, Γ, t) (0, ∅, t'))

    (Hterm : terminates (csubst C e1)),

  terminates (csubst C e2).



(**

  Finally, here is the proof of the Soundness property. The proof works by

  induction on the number of steps taken by [csubst C e1] to terminate at a value.

*)



Theorem Soundness : forall k Γ e1 e2 t

    (HT1: [ k | Γ ⊢ e1 ::: t ])

    (HT2: [ k | Γ ⊢ e2 ::: t ])

    (HL: logrel k Γ e1 e2 t),

  contapprox k Γ e1 e2 t.

Proof.

  unfold contapprox; intros.

  (* Use the compatibility lemma. *)

  apply (compat_cont _ _ _ _ _ _ _ _ _  HCT) in HL.

  assert (HC := ctypes_closed_t HCT).

  (* Use mstep_stepn to obtain the number of steps, and use that number to

     instantiate the logical relation. *)

  destruct Hterm as [v HS']; destruct (mstep_stepn _ _ HS') as [n HS]; clear HS'.

  assert (HL': E[[t']] empFinI n (csubst C e1, csubst C e2)).

    apply (csubst_type HCT), types_closed_e in HT1.

    apply (csubst_type HCT), types_closed_e in HT2.

    eapply HL; eauto; [apply rel_nil | reflexivity | reflexivity].

  revert HS HL'; generalize (csubst C e1) (csubst C e2); clear - HC.

  induction n using wf_ind_lt; rename H into HInd; intros e1 e2 HS1 HL.

  destruct n as [| n]; inversion HS1; subst.

  - rewrite eval_simpl in HL; apply proj1 in HL; specialize (HL (val_irred v)). 

    destruct HL as [ e2' [ HS2 HL ] ]; apply interp_values, proj2 in HL.

    inversion HL as [v' EQ]; subst; eexists; eauto.

  - rewrite eval_simpl in HL; apply proj2 in HL.

    eapply HInd, HL; eauto with arith.

Qed.

project/Binary/Soundness.v

deleted100644 → 0
+0 −276
Original line number Diff line number Diff line 
Require Import DBLib.DeBruijn DBLib.Environments.

Require Import ModuRes.Constr ModuRes.UPred ModuRes.COFE.

Require Import Omega.

Require Import Language Lib.

Require Import Binary.LogRel Binary.WeakSub Binary.Compatibility.



Open Scope lang_scope.



(**

  With the Fundamental property being proven, we can now turn to proving soundness

  of our logical relation with respect to contextual approximation. For this, we first

  have to formalize this notion in Coq. The necessary definitions are fairly 

  straightforward, again following the presentation from the LSLR paper

  (Appendix A, figures 11 and 12).

*)



Section Contexts.



(** Contexts (terms with holes): *)



  Inductive cont : Set :=

  | chole : cont

  | cpair1 : cont -> exp -> cont

  | cpair2 : exp -> cont -> cont

  | cfst : cont -> cont

  | csnd : cont -> cont

  | cinl : cont -> cont

  | cinr : cont -> cont

  | ccase1 : cont -> exp -> exp -> cont

  | ccase2 : exp -> cont -> exp -> cont

  | ccase3 : exp -> exp -> cont -> cont

  | clam : cont -> cont

  | capp1 : cont -> exp -> cont

  | capp2 : exp -> cont -> cont

  | ctlam : cont -> cont

  | ctapp : cont -> cont

  | cpack : cont -> cont

  | cunpack1 : cont -> exp -> cont

  | cunpack2 : exp -> cont -> cont

  | cfold : cont -> cont

  | cunfold : cont -> cont.



(** Substituting a term for the hole in a context: *)



  Fixpoint csubst (C : cont) (e' : exp) :=

    match C with

      | chole => e'

      | cpair1 C eR => epair (csubst C e') eR

      | cpair2 eL C => epair eL (csubst C e')

      | cfst C => efst (csubst C e')

      | csnd C => esnd (csubst C e')

      | cinl C => einl (csubst C e')

      | cinr C => einr (csubst C e')

      | ccase1 C eL eR => ecase (csubst C e') eL eR

      | ccase2 e C eR => ecase e (csubst C e') eR

      | ccase3 e eL C => ecase e eL (csubst C e')

      | clam C => elam (csubst C e')

      | capp1 C ea => eapp (csubst C e') ea

      | capp2 e C => eapp e (csubst C e')

      | ctlam C => etlam (csubst C e')

      | ctapp C => etapp (csubst C e')

      | cpack C => epack (csubst C e')

      | cunpack1 C ep => eunpack (csubst C e') ep

      | cunpack2 e C => eunpack e (csubst C e')

      | cfold C => efold (csubst C e')

      | cunfold C => eunfold (csubst C e')

    end.

  

(**

  The typing relation for contexts: in [ctypes C (k, Γ, t) (k', Γ', t')],

  the intended semantics is that for any [e] with [ [ k | Γ ⊢ e ::: t ] ],

  we get that [ [ k' | Γ' ⊢ csubst C e ::: t' ] ]. We also prove this as a lemma.

*)



  Inductive ctypes : cont -> (nat * env typ * typ) -> (nat * env typ * typ) -> Prop :=

  | CThole : forall k Γ t

        (HC1: closed k Γ)

        (HC: closed k t),

      ctypes chole (k, Γ, t) (k, Γ, t)

  (* TODO: Do I need weakening rules?

  | CTholeW : forall k k' Γ Γ' t t1 t'

        (HCT: ctypes chole (k, Γ, t) (k', Γ', t'))

        (HC: closed k' t1),

      ctypes chole (k, Γ, t) (k', insert 0 t1 Γ', t')

  | CTholeTW : forall k k' Γ Γ' t t'

        (HCT: ctypes chole (k, Γ, t) (k', Γ', t')),

      ctypes chole (k, Γ, t) (S k', shift 0 Γ', t')

  *)

  | CTpair1 : forall C k k' Γ Γ' t t1 t2 eR

        (HCT: ctypes C (k, Γ, t) (k', Γ', t1))

        (HT: [ k' | Γ' ⊢ eR ::: t2 ]),

      ctypes (cpair1 C eR) (k, Γ, t) (k', Γ', t1 × t2)

  | CTpair2 : forall C k k' Γ Γ' t t1 t2 eL

        (HT: [ k' | Γ' ⊢ eL ::: t1 ])

        (HCT: ctypes C (k, Γ, t) (k', Γ', t2)),

      ctypes (cpair2 eL C) (k, Γ, t) (k', Γ', t1 × t2)

  | CTfst : forall C k k' Γ Γ' t t1 t2

        (HCT: ctypes C (k, Γ, t) (k', Γ', t1 × t2)),

      ctypes (cfst C) (k, Γ, t) (k', Γ', t1)

  | CTsnd : forall C k k' Γ Γ' t t1 t2

        (HCT: ctypes C (k, Γ, t) (k', Γ', t1 × t2)),

      ctypes (csnd C) (k, Γ, t) (k', Γ', t2)

  | CTinl : forall C k k' Γ Γ' t t1 t2

        (HCT: ctypes C (k, Γ, t) (k', Γ', t1))

        (HC: closed k' t2),

      ctypes (cinl C) (k, Γ, t) (k', Γ', t1 + t2)

  | CTinr : forall C k k' Γ Γ' t t1 t2

        (HCT: ctypes C (k, Γ, t) (k', Γ', t2))

        (HC: closed k' t1),

      ctypes (cinr C) (k, Γ, t) (k', Γ', t1 + t2)

  | CTcase1 : forall C k k' Γ Γ' t t1 t2 t' eL eR

        (HCT: ctypes C (k, Γ, t) (k', Γ', t1 + t2))

        (HTL: [ k' | insert 0 t1 Γ' ⊢ eL ::: t' ])

        (HTR: [ k' | insert 0 t2 Γ' ⊢ eR ::: t' ]),

      ctypes (ccase1 C eL eR) (k, Γ, t) (k', Γ', t')

  | CTcase2 : forall C k k' Γ Γ' t t1 t2 t' e eR

        (HT: [ k' | Γ' ⊢ e ::: t1 + t2 ])

        (HCT: ctypes C (k, Γ, t) (k', insert 0 t1 Γ', t'))

        (HTR: [ k' | insert 0 t2 Γ' ⊢ eR ::: t' ]),

      ctypes (ccase2 e C eR) (k, Γ, t) (k', Γ', t')

  | CTcase3 : forall C k k' Γ Γ' t t1 t2 t' e eL

        (HT: [ k' | Γ' ⊢ e ::: t1 + t2 ])

        (HTR: [ k' | insert 0 t1 Γ' ⊢ eL ::: t' ])

        (HCT: ctypes C (k, Γ, t) (k', insert 0 t2 Γ', t')),

      ctypes (ccase3 e eL C) (k, Γ, t) (k', Γ', t')

  | CTLam : forall C k k' Γ Γ' t t1 t2

        (HCT: ctypes C (k, Γ, t) (k', insert 0 t1 Γ', t2)),

      ctypes (clam C) (k, Γ, t) (k', Γ', t1 → t2)

  | CTApp1 : forall C k k' Γ Γ' t t2 t' ea

        (HCT: ctypes C (k, Γ, t) (k', Γ', t2 → t'))

        (HT: [ k' | Γ' ⊢ ea ::: t2 ]),

      ctypes (capp1 C ea) (k, Γ, t) (k', Γ', t')

  | CTApp2 : forall C k k' Γ Γ' t t2 t' e

        (HT: [ k' | Γ' ⊢ e ::: t2 → t' ])

        (HCT : ctypes C (k, Γ, t) (k', Γ', t2)),

      ctypes (capp2 e C) (k, Γ, t) (k', Γ', t')

  | CTTLam : forall C k k' Γ Γ' t t'

        (HCT: ctypes C (k, Γ, t) (S k', shift 0 Γ', t')),

      ctypes (ctlam C) (k, Γ, t) (k', Γ', ∀ t')

  | CTTapp : forall C k k' Γ Γ' (t t1 t2 t' : typ)

        (HCT: ctypes C (k, Γ, t) (k', Γ', ∀ t1))

        (HC: closed k' t2)

        (HS: subst t2 0 t1 = t'),

      ctypes (ctapp C) (k, Γ, t) (k', Γ', t')

  | CTPack : forall C k k' Γ Γ' t t1 t'

        (HCT: ctypes C (k, Γ, t) (k', Γ', subst t1 0 t'))

        (HC: closed (S k') t')

        (HC1: closed k' t1),

      ctypes (cpack C) (k, Γ, t) (k', Γ', ∃ t')

  | CTUnpack1 : forall C k k' Γ Γ' t t1 t' ep

        (HCT: ctypes C (k, Γ, t) (k', Γ', ∃ t1))

        (HT: [ S k' | insert 0 t1 (shift 0 Γ') ⊢ ep ::: shift 0 t' ])

        (HC: closed k' t'),

      ctypes (cunpack1 C ep) (k, Γ, t) (k', Γ', t')

  | CTUnpack2 : forall C k k' Γ Γ' t t1 t' e

        (HT: [ k' | Γ' ⊢ e ::: ∃ t1 ])

        (HCT: ctypes C (k, Γ, t) (S k', insert 0 t1 (shift 0 Γ'), shift 0 t'))

        (HC: closed k' t'),

      ctypes (cunpack2 e C) (k, Γ, t) (k', Γ', t')

  | CTFold : forall C k k' Γ Γ' t t'

        (HCT: ctypes C (k, Γ, t) (k', Γ', subst (μ t') 0 t'))

        (HC: closed (S k') t'),

      ctypes (cfold C) (k, Γ, t) (k', Γ', μ t')

  | CTUnfold : forall C k k' Γ Γ' t t1 t'

        (HCT: ctypes C (k, Γ, t) (k', Γ', μ t1))

        (HS: subst (μ t1) 0 t1 = t'),

      ctypes (cunfold C) (k, Γ, t) (k', Γ', t').



End Contexts.



Lemma csubst_type : forall {C k k' Γ Γ' t t' e}

    (HCT: ctypes C (k, Γ, t) (k', Γ', t'))

    (HT: [ k | Γ ⊢ e ::: t ]),

  [ k' | Γ' ⊢ csubst C e ::: t' ].

Proof.

  induction C; intros; simpl; inversion HCT; subst; eauto using types.

Qed.



(**

  For the proof of the Soundness property we are going to need the "semantic version"

  of the [csubst_type] lemma, which is going to be a compatibility lemma for (well-typed)

  contexts:

  whenever [logrel k Γ e1 e2 t], we also have [logrel k' Γ' (csubst C e1) (csubst C e2) t'].

  

  As with the original compatibility lemmas, there is first a more technical lemma

  about the closedness of types occuring in the typing relation for contexts:

*)



Lemma ctypes_closed : forall {C k k' Γ Γ' t t'}

    (HCT: ctypes C (k, Γ, t) (k', Γ', t')),

  closed k' Γ' /\ closed k' t'.

Proof.

  induction C; intros; simpl; inversion HCT; subst; eauto.

  apply IHC in HCT0. intuition. apply types_closed_t in HT. construction_closed.

  apply IHC in HCT0. intuition. apply types_closed_t in HT. construction_closed.

  apply IHC in HCT0. intuition. inversion_closed. assumption.

  apply IHC in HCT0. intuition. inversion_closed. assumption.

  apply IHC in HCT0. intuition. construction_closed.

  apply IHC in HCT0. intuition. construction_closed.

  apply IHC in HCT0. apply types_closed_t in HTL. intuition.

  apply IHC in HCT0. intuition. inversion_closed. construction_closed.

  apply IHC in HCT0. intuition. inversion_closed. construction_closed.

  apply IHC in HCT0. intuition; inversion_closed; construction_closed.

  apply IHC in HCT0. intuition. inversion_closed. assumption.

  apply IHC in HCT0. apply types_closed_t in HT. intuition. inversion_closed; assumption.

  apply IHC in HCT0. intuition. inversion_closed.

  apply fold_closed in H; erewrite <- lift_preserves_closed_iff in H.

  assumption. construction_closed.

  apply IHC in HCT0. intuition. inversion_closed. eapply subst_preserves_closed; auto. apply _.

  apply IHC in HCT0. intuition. inversion_closed. construction_closed.

  apply IHC in HCT0. intuition.

  apply IHC in HCT0. apply types_closed in HT. intuition.

  apply IHC in HCT0. intuition. construction_closed.

  apply IHC in HCT0. intuition. inversion_closed.

  eapply subst_preserves_closed. apply _. construction_closed. assumption.

Qed.



Definition ctypes_closed_t {C k k' Γ Γ' t t'} (HCT: ctypes C (k, Γ, t) (k', Γ', t')) :=

  proj2 (ctypes_closed HCT).



(**

  Now the proof of the compatibility lemma becomes a simple matter of combining

  the previous compatibility lemmas and the Fundamental property together,

  using the closedness lemmas to deal with any closedness conditions that arise.

*)



Lemma compat_cont : forall C k k' Γ Γ' t t' e1 e2

    (HCT: ctypes C (k, Γ, t) (k', Γ', t'))

    (HL: logrel k Γ e1 e2 t),

  logrel k' Γ' (csubst C e1) (csubst C e2) t'.

Proof.

  induction C; intros; simpl; inversion HCT; subst;

    eauto 6 using Fundamental, ctypes_closed_t, types_closed_t with compat.

Qed.



(** Definition of contextual approximation: *)



Definition terminates e := exists (v : val), e ↦* v.

Definition contapprox k Γ e1 e2 t :=

  forall C t'

    (HCT : ctypes C (k, Γ, t) (0, ∅, t'))

    (Hterm : terminates (csubst C e1)),

  terminates (csubst C e2).



(**

  Finally, here is the proof of the Soundness property. The proof works by

  induction on the number of steps taken by [csubst C e1] to terminate at a value.

*)



Theorem Soundness : forall k Γ e1 e2 t

    (HT1: [ k | Γ ⊢ e1 ::: t ])

    (HT2: [ k | Γ ⊢ e2 ::: t ])

    (HL: logrel k Γ e1 e2 t),

  contapprox k Γ e1 e2 t.

Proof.

  unfold contapprox; intros.

  (* Use the compatibility lemma. *)

  apply (compat_cont _ _ _ _ _ _ _ _ _  HCT) in HL.

  assert (HC := ctypes_closed_t HCT).

  (* Use mstep_stepn to obtain the number of steps, and use that number to

     instantiate the logical relation. *)

  destruct Hterm as [v HS']; destruct (mstep_stepn _ _ HS') as [n HS]; clear HS'.

  assert (HL': E[[t']] empFinI n (csubst C e1, csubst C e2)).

    apply (csubst_type HCT), types_closed_e in HT1.

    apply (csubst_type HCT), types_closed_e in HT2.

    eapply HL; eauto; [apply rel_nil | reflexivity | reflexivity].

  revert HS HL'; generalize (csubst C e1) (csubst C e2); clear - HC.

  induction n using wf_ind_lt; rename H into HInd; intros e1 e2 HS1 HL.

  destruct n as [| n]; inversion HS1; subst.

  - rewrite eval_simpl in HL; apply proj1 in HL; specialize (HL (val_irred v)). 

    destruct HL as [ e2' [ HS2 HL ] ]; apply interp_values, proj2 in HL.

    inversion HL as [v' EQ]; subst; eexists; eauto.

  - rewrite eval_simpl in HL; apply proj2 in HL.

    eapply HInd, HL; eauto with arith.

Qed.

project/BinaryTyped/Compatibility.v

+59 −0
Original line number Diff line number Diff line
@@ -683,3 +683,62 @@ Proof. 
  induction 1; subst; eauto using types_closed_t with compat.

Qed.



(** ** Soundness

    

    TODO



    Now the proof of the compatibility lemma becomes a simple matter of combining

    the previous compatibility lemmas and the Fundamental property together,

    using the closedness lemmas to deal with any closedness conditions that arise.

*)



Lemma compat_cont : forall C k k' Γ Γ' t t' e1 e2

    (HCT: ctypes C (k, Γ, t) (k', Γ', t'))

    (HL: logrel k Γ e1 e2 t),

  logrel k' Γ' (csubst C e1) (csubst C e2) t'.

Proof.

  induction C; intros; simpl; inversion HCT; subst;

    eauto 6 using Fundamental, ctypes_closed_t, types_closed_t with compat.

Qed.



(** Definition of contextual approximation: *)



Definition terminates e := exists (v : val), e ↦* v.

Definition contapprox k Γ e1 e2 t :=

  forall C t'

    (HCT : ctypes C (k, Γ, t) (0, ∅, t'))

    (Hterm : terminates (csubst C e1)),

  terminates (csubst C e2).



(**

  Finally, here is the proof of the Soundness property. The proof works by

  induction on the number of steps taken by [csubst C e1] to terminate at a value.

*)



Theorem Soundness : forall k Γ e1 e2 t

    (HT1: [ k | Γ ⊢ e1 ::: t ])

    (HT2: [ k | Γ ⊢ e2 ::: t ])

    (HL: logrel k Γ e1 e2 t),

  contapprox k Γ e1 e2 t.

Proof.

  unfold contapprox; intros.

  (* Use the compatibility lemma. *)

  apply (compat_cont _ _ _ _ _ _ _ _ _  HCT) in HL.

  assert (HC := ctypes_closed_t HCT).

  (* Use mstep_stepn to obtain the number of steps, and use that number to

     instantiate the logical relation. *)

  destruct Hterm as [v HS']; destruct (mstep_stepn _ _ HS') as [n HS]; clear HS'.

  assert (HL': E[[t']] empFinI n (csubst C e1, csubst C e2)).

    apply (csubst_type HCT), types_closed_e in HT1.

    apply (csubst_type HCT), types_closed_e in HT2.

    eapply HL; eauto; [apply rel_nil | reflexivity | reflexivity].

  revert HS HL'; generalize (csubst C e1) (csubst C e2); clear - HC.

  induction n using wf_ind_lt; rename H into HInd; intros e1 e2 HS1 HL.

  destruct n as [| n]; inversion HS1; subst.

  - rewrite eval_simpl in HL; apply proj1 in HL; specialize (HL (val_irred v)). 

    destruct HL as [ e2' [ HS2 HL ] ]; apply interp_values, proj2 in HL.

    inversion HL as [v' EQ]; subst; eexists; eauto.

  - rewrite eval_simpl in HL; apply proj2 in HL.

    eapply HInd, HL; eauto with arith.

Qed.

project/BinaryTyped/Soundness.v

deleted100644 → 0
+0 −275

File deleted.

Preview size limit exceeded, changes collapsed.