diff --git a/_CoqProject b/_CoqProject index 4f9d311..54d7406 100644 --- a/_CoqProject +++ b/_CoqProject @@ -41,9 +41,13 @@ theories/type_systems/systemf/notation.v theories/type_systems/systemf/types.v theories/type_systems/systemf/tactics.v theories/type_systems/systemf/bigstep.v +theories/type_systems/systemf/church_encodings.v theories/type_systems/systemf/parallel_subst.v theories/type_systems/systemf/logrel.v +theories/type_systems/systemf/logrel_sol.v theories/type_systems/systemf/free_theorems.v +theories/type_systems/systemf/binary_logrel.v +theories/type_systems/systemf/existential_invariants.v # By removing the # below, you can add the exercise sheets to make theories/type_systems/warmup/warmup.v @@ -57,3 +61,5 @@ theories/type_systems/stlc/exercises02.v #theories/type_systems/systemf/exercises03.v #theories/type_systems/systemf/exercises03_sol.v #theories/type_systems/systemf/exercises04.v +#theories/type_systems/systemf/exercises04_sol.v +#theories/type_systems/systemf/exercises05.v diff --git a/theories/type_systems/systemf/binary_logrel.v b/theories/type_systems/systemf/binary_logrel.v new file mode 100644 index 0000000..33787fa --- /dev/null +++ b/theories/type_systems/systemf/binary_logrel.v @@ -0,0 +1,1095 @@ +(* NOTE: import order matters here. + stdpp and Equations both set different default obligation tactics, + and the one from Equations is much better at solving the Equations goals. *) +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.lib Require Export facts. +From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep tactics. +From Equations Require Export Equations. + +(** * Logical relation for SystemF *) + +Implicit Types + (Δ : nat) + (Γ : typing_context) + (v : val) + (α : var) + (e : expr) + (A : type). + +(** ** Definition of the logrel *) +(** + In Coq, we need to make argument why the logical relation is well-defined precise: + This holds true in particular for the mutual recursion between the value relation and the expression relation. + We therefore define a termination measure [mut_measure] that makes sure that for each recursive call, we either + - decrease the size of the type + - or switch from the expression case to the value case. + + We use the Equations package to define the logical relation, as it's tedious to make the termination + argument work with Coq's built-in support for recursive functions. + *) +Inductive val_or_expr : Type := +| inj_val : val → val → val_or_expr +| inj_expr : expr → expr → val_or_expr. + +(* The [type_size] function essentially computes the size of the "type tree". *) +(* Note that we have added some additional primitives to make our (still + simple) language more expressive. *) +Equations type_size (A : type) : nat := + type_size Int := 1; + type_size Bool := 1; + type_size Unit := 1; + type_size (A → B) := type_size A + type_size B + 1; + type_size (#α) := 1; + type_size (∀: A) := type_size A + 2; + type_size (∃: A) := type_size A + 2; + type_size (A × B) := type_size A + type_size B + 1; + type_size (A + B) := max (type_size A) (type_size B) + 1. + +(* The definition of the expression relation uses the value relation -- therefore, it needs to be larger, and we add [1]. *) +Equations mut_measure (ve : val_or_expr) (t : type) : nat := + mut_measure (inj_val _ _) t := type_size t; + mut_measure (inj_expr _ _) t := 1 + type_size t. + +(** A semantic type consists of a value-relation and a proof of closedness *) +Record sem_type := mk_ST { + sem_type_car :> val → val → Prop; + sem_type_closed_val v w : sem_type_car v w → is_closed [] (of_val v) ∧ is_closed [] (of_val w); + }. +(** Two tactics we will use later on. + [pose_sem_type P as N] defines a semantic type at name [N] with the value predicate [P]. + [specialize_sem_type S with P as N] specializes a universal quantifier over sem types in [S] with + a semantic type with predicate [P], giving it the name [N]. + *) +(* slightly complicated formulation to make the proof term [p] opaque and prevent it from polluting the context *) +Tactic Notation "pose_sem_type" uconstr(P) "as" ident(N) := + let p := fresh "__p" in + unshelve refine ((λ p, let N := (mk_ST P p) in _) _); first (simpl in p); cycle 1. +Tactic Notation "specialize_sem_type" constr(S) "with" uconstr(P) "as" ident(N) := + pose_sem_type P as N; last specialize (S N). + +(** We represent type variable assignments [δ] as lists of semantic types. + The variable #n (in De Bruijn representation) is mapped to the [n]-th element of the list. + *) +Definition tyvar_interp := nat → sem_type. +Implicit Types + (δ : tyvar_interp) + (τ : sem_type) +. + +(** The logical relation *) +Equations type_interp (c : val_or_expr) (t : type) δ : Prop by wf (mut_measure c t) := { + type_interp (inj_val v w) Int δ => + ∃ z : Z, v = #z ∧ w = #z; + type_interp (inj_val v w) Bool δ => + ∃ b : bool, v = #b ∧ w = #b; + type_interp (inj_val v w) Unit δ => + v = #LitUnit ∧ w = #LitUnit ; + type_interp (inj_val v w) (A × B) δ => + ∃ v1 v2 w1 w2 : val, v = (v1, v2)%V ∧ w = (w1, w2)%V ∧ type_interp (inj_val v1 w1) A δ ∧ type_interp (inj_val v2 w2) B δ; + type_interp (inj_val v w) (A + B) δ => + (∃ v' w' : val, v = InjLV v' ∧ w = InjLV w' ∧ type_interp (inj_val v' w') A δ) ∨ + (∃ v' w' : val, v = InjRV v' ∧ w = InjRV w' ∧ type_interp (inj_val v' w') B δ); + type_interp (inj_val v w) (A → B) δ => + ∃ x y e1 e2, v = LamV x e1 ∧ w = LamV y e2 ∧ is_closed (x :b: nil) e1 ∧ is_closed (y :b: nil) e2 ∧ + ∀ v' w', + type_interp (inj_val v' w') A δ → + type_interp (inj_expr (subst' x (of_val v') e1) (subst' y (of_val w') e2)) B δ; + (** Type variable case *) + type_interp (inj_val v w) (#α) δ => + (δ α).(sem_type_car) v w; + (** ∀ case *) + type_interp (inj_val v w) (∀: A) δ => + ∃ e1 e2, v = TLamV e1 ∧ w = TLamV e2 ∧ is_closed [] e1 ∧ is_closed [] e2 ∧ + ∀ τ, type_interp (inj_expr e1 e2) A (τ .: δ); + (** ∃ case *) + type_interp (inj_val v w) (∃: A) δ => + ∃ v' w', v = PackV v' ∧ w = PackV w' ∧ + ∃ τ : sem_type, type_interp (inj_val v' w') A (τ .: δ); + + type_interp (inj_expr e1 e2) t δ => + ∃ v1 v2, big_step e1 v1 ∧ big_step e2 v2 ∧ type_interp (inj_val v1 v2) t δ +}. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. + simp mut_measure. simp type_size. + destruct A; repeat simp mut_measure; repeat simp type_size; lia. +Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. + +(** Value relation and expression relation *) +Notation sem_val_rel A δ v w := (type_interp (inj_val v w) A δ). +Notation sem_expr_rel A δ e1 e2 := (type_interp (inj_expr e1 e2) A δ). + +Notation 𝒱 A δ v w := (sem_val_rel A δ v w). +Notation ℰ A δ e1 e2 := (sem_expr_rel A δ e1 e2). + + +Lemma val_rel_is_closed v w δ A: + 𝒱 A δ v w → is_closed [] (of_val v) ∧ is_closed [] (of_val w). +Proof. + induction A as [ | | | | | A IHA | | A IH1 B IH2 | A IH1 B IH2] in v, w, δ |-*; simp type_interp. + - by eapply sem_type_closed_val. + - intros [z [-> ->]]. done. + - intros [b [-> ->]]. done. + - intros [-> ->]. done. + - intros (e1 & e2 & -> & -> & ? & ? & _). done. + - intros (v' & w' & -> & -> & (τ & Hinterp)). simpl. by eapply IHA. + - intros (x & y & e1 & e2 & -> & -> & ? & ? & _). done. + - intros (v1 & v2 & w1 & w2 & -> & -> & ? & ?). simpl. split; apply andb_True; split; naive_solver. + - intros [(v' & w' & -> & -> & ?) | (v' & w' & -> & -> & ?)]; simpl; eauto. +Qed. + +(** Interpret a syntactic type *) +Program Definition interp_type A δ : sem_type := {| + sem_type_car := fun v w => 𝒱 A δ v w; +|}. +Next Obligation. by eapply val_rel_is_closed. Qed. + +(* Semantic typing of contexts *) +Implicit Types + (θ : gmap string expr). + +(** Context relation *) +Inductive sem_context_rel (δ : tyvar_interp) : typing_context → (gmap string expr) → (gmap string expr) → Prop := + | sem_context_rel_empty : sem_context_rel δ ∅ ∅ ∅ + | sem_context_rel_insert Γ θ1 θ2 v w x A : + 𝒱 A δ v w → + sem_context_rel δ Γ θ1 θ2 → + sem_context_rel δ (<[x := A]> Γ) (<[x := of_val v]> θ1) (<[x := of_val w]> θ2). + +Notation 𝒢 := sem_context_rel. + +(** Semantic typing judgment *) +Definition sem_typed Δ Γ e1 e2 A := + is_closed (elements (dom Γ)) e1 ∧ is_closed (elements (dom Γ)) e2 ∧ + ∀ θ1 θ2 δ, 𝒢 δ Γ θ1 θ2 → ℰ A δ (subst_map θ1 e1) (subst_map θ2 e2). +Notation "'TY' Δ ; Γ ⊨ e1 ≈ e2 : A" := (sem_typed Δ Γ e1 e2 A) (at level 74, e1, e2, A at next level). + +Lemma sem_expr_rel_of_val A δ v w : + ℰ A δ (of_val v) (of_val w) → 𝒱 A δ v w. +Proof. + simp type_interp. + intros (v' & w' & ->%big_step_val & ->%big_step_val & Hv'). + apply Hv'. +Qed. + +Lemma sem_context_rel_vals {δ Γ θ1 θ2 x A} : + sem_context_rel δ Γ θ1 θ2 → + Γ !! x = Some A → + ∃ e1 e2 v1 v2, θ1 !! x = Some e1 ∧ θ2 !! x = Some e2 ∧ to_val e1 = Some v1 ∧ to_val e2 = Some v2 ∧ 𝒱 A δ v1 v2. +Proof. + induction 1 as [|Γ θ1 θ2 v w y B Hvals Hctx IH]. + - naive_solver. + - rewrite lookup_insert_Some. intros [[-> ->]|[Hne Hlook]]. + + do 4 eexists. + split; first by rewrite lookup_insert. + split; first by rewrite lookup_insert. + split; first by eapply to_of_val. + split; first by eapply to_of_val. + done. + + eapply IH in Hlook as (e1 & e2 & w1 & w2 & Hlook1 & Hlook2 & He1 & He2 & Hval). + do 4 eexists. + split; first by rewrite lookup_insert_ne. + split; first by rewrite lookup_insert_ne. + repeat split; done. +Qed. + +Lemma sem_context_rel_subset δ Γ θ1 θ2 : + 𝒢 δ Γ θ1 θ2 → dom Γ ⊆ dom θ1 ∧ dom Γ ⊆ dom θ2. +Proof. + intros Hctx. split; apply elem_of_subseteq; intros x (A & Hlook)%elem_of_dom. + all: eapply sem_context_rel_vals in Hlook as (e1 & e2 & v1 & v2 & Hlook1 & Hlook2 & Heq1 & Heq2 & Hval); last done. + all: eapply elem_of_dom; eauto. +Qed. + + +Lemma sem_context_rel_closed δ Γ θ1 θ2: + 𝒢 δ Γ θ1 θ2 → subst_is_closed [] θ1 ∧ subst_is_closed [] θ2. +Proof. + induction 1 as [ | Γ θ1 θ2 v w x A Hv Hctx [IH1 IH2]]; rewrite /subst_is_closed. + - naive_solver. + - split; intros y e; rewrite lookup_insert_Some. + all: intros [[-> <-]|[Hne Hlook]]. + + eapply val_rel_is_closed in Hv. naive_solver. + + eapply IH1; last done. + + eapply val_rel_is_closed in Hv. naive_solver. + + eapply IH2; last done. +Qed. +Lemma sem_context_rel_dom δ Γ θ1 θ2 : + 𝒢 δ Γ θ1 θ2 → dom Γ = dom θ1 /\ dom Γ = dom θ2. +Proof. + induction 1. + - by rewrite !dom_empty. + - rewrite !dom_insert. set_solver. +Qed. + + +Section boring_lemmas. + (** The lemmas in this section are all quite boring and expected statements, + but are quite technical to prove due to De Bruijn binders. + We encourage to skip over the proofs of these lemmas. + *) + + Lemma sem_val_rel_ext B δ δ' v w : + (∀ n v w, δ n v w ↔ δ' n v w) → + 𝒱 B δ v w ↔ 𝒱 B δ' v w. + Proof. + induction B in δ, δ', v, w |-*; simpl; simp type_interp; eauto; intros Hiff. + - f_equiv; intros e1. f_equiv; intros e2. do 4 f_equiv. + eapply forall_proper; intros τ. + simp type_interp. f_equiv. intros v1. f_equiv. intros v2. + do 2 f_equiv. etransitivity; last apply IHB; first done. + intros [|m] ?; simpl; eauto. + - f_equiv. intros v1. f_equiv. intros v2. do 3 f_equiv. intros τ. + etransitivity; last apply IHB; first done. + intros [|m] ?; simpl; eauto. + - do 4 (f_equiv; intros ?). + do 4 f_equiv. + eapply forall_proper; intros v1. + eapply forall_proper; intros v2. + eapply if_iff; first eauto. + simp type_interp. f_equiv. intros v3. + f_equiv. intros v4. + do 2 f_equiv. + eauto. + - do 4 (f_equiv; intros ?). + do 3 f_equiv; eauto. + - f_equiv; f_equiv; intros ?; f_equiv; intros ?. + all: do 2 f_equiv; eauto. + Qed. + + + Lemma sem_val_rel_move_ren B δ σ v w: + 𝒱 B (λ n, δ (σ n)) v w ↔ 𝒱 (rename σ B) δ v w. + Proof. + induction B in σ, δ, v, w |-*; simpl; simp type_interp; eauto. + - f_equiv; intros e1. f_equiv; intros e2. do 4 f_equiv. + eapply forall_proper; intros τ. + simp type_interp. f_equiv. intros v1. f_equiv. intros v2. + do 2 f_equiv. etransitivity; last apply IHB. + eapply sem_val_rel_ext; intros [|n] u; asimpl; done. + - f_equiv. intros v1. f_equiv. intros v2. do 3 f_equiv. intros τ. + etransitivity; last apply IHB. + eapply sem_val_rel_ext; intros [|n] u. + + simp type_interp. done. + + simpl. rewrite /up. simpl. done. + - do 4 (f_equiv; intros ?). + do 4 f_equiv. + eapply forall_proper; intros v1. + eapply forall_proper; intros v2. + eapply if_iff; first eauto. + simp type_interp. f_equiv. intros v3. + f_equiv. intros v4. + do 2 f_equiv. + eauto. + - do 4 (f_equiv; intros ?). + do 3 f_equiv; eauto. + - f_equiv; f_equiv; intros ?; f_equiv; intros ?. + all: do 2 f_equiv; eauto. + Qed. + + + Lemma sem_val_rel_move_subst B δ σ v w : + 𝒱 B (λ n, interp_type (σ n) δ) v w ↔ 𝒱 (B.[σ]) δ v w. + Proof. + induction B in σ, δ, v, w |-*; simpl; simp type_interp; eauto. + - f_equiv; intros e1. f_equiv; intros e2. do 4 f_equiv. + eapply forall_proper; intros τ. + simp type_interp. f_equiv. intros v1. f_equiv. intros v2. + do 2 f_equiv. etransitivity; last apply IHB. + eapply sem_val_rel_ext; intros [|n] u. + + simp type_interp. done. + + simpl. rewrite /up. simpl. + etransitivity; last eapply sem_val_rel_move_ren. + simpl. done. + - f_equiv. intros v1. f_equiv. intros v2. do 3 f_equiv. intros τ. + etransitivity; last apply IHB. + eapply sem_val_rel_ext; intros [|n] u. + + simp type_interp. done. + + simpl. rewrite /up. simpl. + etransitivity; last eapply sem_val_rel_move_ren. + simpl. done. + - do 4 (f_equiv; intros ?). + do 4 f_equiv. + eapply forall_proper; intros v1. + eapply forall_proper; intros v2. + eapply if_iff; first eauto. + simp type_interp. f_equiv. intros v3. + f_equiv. intros v4. + do 2 f_equiv. + eauto. + - do 4 (f_equiv; intros ?). + do 3 f_equiv; eauto. + - f_equiv; f_equiv; intros ?; f_equiv; intros ?. + all: do 2 f_equiv; eauto. + Qed. + + Lemma sem_val_rel_move_single_subst A B δ v w : + 𝒱 B (interp_type A δ .: δ) v w ↔ 𝒱 (B.[A/]) δ v w. + Proof. + rewrite -sem_val_rel_move_subst. eapply sem_val_rel_ext. + intros [| n] w1 w2; simpl; done. + Qed. + + Lemma sem_val_rel_cons A δ v w τ : + 𝒱 A δ v w ↔ 𝒱 A.[ren (+1)] (τ .: δ) v w. + Proof. + rewrite -sem_val_rel_move_subst; simpl. + eapply sem_val_rel_ext; done. + Qed. + + Lemma sem_context_rel_cons Γ δ θ1 θ2 τ : + 𝒢 δ Γ θ1 θ2 → + 𝒢 (τ .: δ) (⤉ Γ) θ1 θ2. + Proof. + induction 1 as [ | Γ θ1 θ2 v w x A Hv Hctx IH]; simpl. + - rewrite fmap_empty. constructor. + - rewrite fmap_insert. constructor; last done. + rewrite -sem_val_rel_cons. done. + Qed. +End boring_lemmas. + +(** ** Compatibility lemmas *) + +Lemma compat_int Δ Γ z : TY Δ; Γ ⊨ (Lit $ LitInt z) ≈ (Lit $ LitInt z) : Int. +Proof. + do 2 (split; first done). + intros θ1 θ2 δ _. simp type_interp. + exists #z, #z. + split; first by constructor. + split; first by constructor. + simp type_interp. eauto. +Qed. + +Lemma compat_bool Δ Γ b : TY Δ; Γ ⊨ (Lit $ LitBool b) ≈ (Lit $ LitBool b) : Bool. +Proof. + do 2 (split; first done). + intros θ1 θ2 δ _. simp type_interp. + exists #b, #b. + split; first by constructor. + split; first by constructor. + simp type_interp. eauto. +Qed. + +Lemma compat_unit Δ Γ : TY Δ; Γ ⊨ (Lit $ LitUnit) ≈ (Lit $ LitUnit) : Unit. +Proof. + do 2 (split; first done). + intros θ1 θ2 δ _. simp type_interp. + exists #LitUnit, #LitUnit. + split; first by constructor. + split; first by constructor. + simp type_interp. split; eauto. +Qed. + +Lemma compat_var Δ Γ x A : + Γ !! x = Some A → + TY Δ; Γ ⊨ (Var x) ≈ (Var x) : A. +Proof. + intros Hx. + do 2 (split; first eapply bool_decide_pack, elem_of_elements, elem_of_dom_2, Hx). + intros θ1 θ2 δ Hctx; simpl. + + (* TODO: exercise *) +Admitted. + + +Lemma compat_app Δ Γ e1 e1' e2 e2' A B : + TY Δ; Γ ⊨ e1 ≈ e1': (A → B) → + TY Δ; Γ ⊨ e2 ≈ e2' : A → + TY Δ; Γ ⊨ (e1 e2) ≈ (e1' e2') : B. +Proof. + intros (Hfuncl & Hfuncl' & Hfun) (Hargcl & Hargcl' & Harg). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx; simpl. + + specialize (Hfun _ _ _ Hctx). simp type_interp in Hfun. destruct Hfun as (v1 & v2 & Hbs1 & Hbs2 & Hv12). + simp type_interp in Hv12. destruct Hv12 as (x & y & e1'' & e2'' & -> & -> & ? & ? & Hv12). + specialize (Harg _ _ _ Hctx). simp type_interp in Harg. + destruct Harg as (v3 & v4 & Hbs3 & Hbs4 & Hv34). + + apply Hv12 in Hv34. + simp type_interp in Hv34. + destruct Hv34 as (v5 & v6 & Hbs5 & Hbs6 & Hv56). + + simp type_interp. + exists v5, v6. eauto. +Qed. + + + +(* Compatibility for [lam] unfortunately needs a very technical helper lemma. *) +Lemma lam_closed Γ θ (x : string) A e : + dom Γ = dom θ → + subst_is_closed [] θ → + closed (elements (dom (<[x:=A]> Γ))) e → + closed [] (Lam x (subst_map (delete x θ) e)). +Proof. + intros Hdom Hsubstcl Hcl. + eapply subst_map_closed. + - eapply is_closed_weaken; first done. + rewrite dom_delete dom_insert Hdom //. + intros y. destruct (decide (x = y)); set_solver. + - intros x' e' Hx. + eapply (is_closed_weaken []); last set_solver. + eapply Hsubstcl. + eapply map_subseteq_spec; last done. + apply map_delete_subseteq. +Qed. +(** Lambdas need to be closed by the context *) +Lemma compat_lam_named Δ Γ x e1 e2 A B : + TY Δ; (<[ x := A ]> Γ) ⊨ e1 ≈ e2 : B → + TY Δ; Γ ⊨ (Lam (BNamed x) e1) ≈ (Lam (BNamed x) e2): (A → B). +Proof. + intros (Hbodycl & Hbodycl' & Hbody). + do 2 (split; first (simpl; eapply is_closed_weaken; set_solver)). + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + + exists ((λ: x, subst_map (delete x θ1) e1))%V, ((λ: x, subst_map (delete x θ2) e2))%V. + split; first by eauto. + split; first by eauto. + simp type_interp. + + opose proof* sem_context_rel_dom as []; first done. + opose proof* sem_context_rel_closed as []; first done. + eexists (BNamed x), (BNamed x), _, _. split_and!. + 1-2: reflexivity. + 1-2: eapply lam_closed; eauto. + intros v' w' Hvw'. + specialize (Hbody (<[ x := of_val v']> θ1) (<[ x := of_val w']> θ2)). + simpl. generalize Hctx=>Hctx'. + eapply sem_context_rel_closed in Hctx' as Hclosed. + rewrite !subst_subst_map; [|naive_solver..]. + apply Hbody. apply sem_context_rel_insert; done. +Qed. + + +Lemma compat_lam_anon Δ Γ e1 e2 A B : + TY Δ; Γ ⊨ e1 ≈ e2 : B → + TY Δ; Γ ⊨ (Lam BAnon e1) ≈ (Lam BAnon e2) : (A → B). +Proof. + intros (Hbodycl & Hbodycl' & Hbody). + do 2 (split; first done). + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + + exists (λ: <>, subst_map θ1 e1)%V, (λ: <>, subst_map θ2 e2)%V. + split; first by eauto. + split; first by eauto. + simp type_interp. + eexists BAnon, BAnon, _, _. split_and!; try reflexivity. + - simpl. eapply subst_map_closed; simpl. + + replace (dom θ1) with (dom Γ); first done. + eapply sem_context_rel_dom in Hctx. naive_solver. + + apply sem_context_rel_closed in Hctx. naive_solver. + - simpl. eapply subst_map_closed; simpl. + + replace (dom θ2) with (dom Γ); first done. + eapply sem_context_rel_dom in Hctx. naive_solver. + + apply sem_context_rel_closed in Hctx. naive_solver. + - intros v' w' Hvw'. + specialize (Hbody θ1 θ2). + simpl. apply Hbody; done. +Qed. + +Lemma compat_int_binop Δ Γ op e1 e1' e2 e2' : + bin_op_typed op Int Int Int → + TY Δ; Γ ⊨ e1 ≈ e1' : Int → + TY Δ; Γ ⊨ e2 ≈ e2' : Int → + TY Δ; Γ ⊨ (BinOp op e1 e2) ≈ (BinOp op e1' e2') : Int. +Proof. + intros Hop (He1cl & He1cl' & He1) (He2cl & He2cl' & He2). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + specialize (He1 _ _ _ Hctx). specialize (He2 _ _ _ Hctx). + simp type_interp in He1. simp type_interp in He2. + + destruct He1 as (v1 & v1' & Hb1 & Hb1' & Hv1). + destruct He2 as (v2 & v2' & Hb2 & Hb2' & Hv2). + simp type_interp in Hv1, Hv2. + destruct Hv1 as (z1 & -> & ->). + destruct Hv2 as (z2 & -> & ->). + + inversion Hop; subst op. + + exists #(z1 + z2)%Z, #(z1 + z2)%Z. split_and!. + - econstructor; done. + - econstructor; done. + - exists (z1 + z2)%Z. done. + + exists #(z1 - z2)%Z, #(z1 - z2)%Z. split_and!. + - econstructor; done. + - econstructor; done. + - exists (z1 - z2)%Z. done. + + exists #(z1 * z2)%Z, #(z1 * z2)%Z. split_and!. + - econstructor; done. + - econstructor; done. + - exists (z1 * z2)%Z. done. +Qed. + +Lemma compat_int_bool_binop Δ Γ op e1 e1' e2 e2' : + bin_op_typed op Int Int Bool → + TY Δ; Γ ⊨ e1 ≈ e1' : Int → + TY Δ; Γ ⊨ e2 ≈ e2' : Int → + TY Δ; Γ ⊨ (BinOp op e1 e2) ≈ (BinOp op e1' e2') : Bool. +Proof. + intros Hop (He1cl & He1cl' & He1) (He2cl & He2cl' & He2). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + + simp type_interp. + specialize (He1 _ _ _ Hctx). specialize (He2 _ _ _ Hctx). + simp type_interp in He1. simp type_interp in He2. + + destruct He1 as (v1 & v1' & Hb1 & Hb1' & Hv1). + destruct He2 as (v2 & v2' & Hb2 & Hb2' & Hv2). + simp type_interp in Hv1, Hv2. + destruct Hv1 as (z1 & -> & ->). + destruct Hv2 as (z2 & -> & ->). + + inversion Hop; subst op. + + exists #(bool_decide (z1 < z2))%Z, #(bool_decide (z1 < z2))%Z. split_and!. + - econstructor; done. + - econstructor; done. + - by eexists _. + + exists #(bool_decide (z1 ≤ z2))%Z, #(bool_decide (z1 ≤ z2))%Z. split_and!. + - econstructor; done. + - econstructor; done. + - by eexists _. + + exists #(bool_decide (z1 = z2))%Z, #(bool_decide (z1 = z2))%Z. split_and!. + - econstructor; done. + - econstructor; done. + - eexists _. done. +Qed. + +Lemma compat_unop Δ Γ op A B e e' : + un_op_typed op A B → + TY Δ; Γ ⊨ e ≈ e' : A → + TY Δ; Γ ⊨ (UnOp op e) ≈ (UnOp op e') : B. +Proof. + intros Hop (Hecl & Hecl' & He). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + + simp type_interp. specialize (He _ _ _ Hctx). + simp type_interp in He. + + destruct He as (v & v' & Hb & Hb' & Hv). + inversion Hop; subst; simp type_interp in Hv. + - destruct Hv as (b & -> & ->). + exists #(negb b), #(negb b). split_and!. + + econstructor; done. + + econstructor; done. + + by eexists _. + - destruct Hv as (z & -> & ->). + exists #(-z)%Z, #(-z)%Z. split_and!. + + econstructor; done. + + econstructor; done. + + by eexists _. +Qed. + + +Lemma compat_tlam Δ Γ e1 e2 A : + TY S Δ; (⤉ Γ) ⊨ e1 ≈ e2 : A → + TY Δ; Γ ⊨ (Λ, e1) ≈ (Λ, e2) : (∀: A). +Proof. + intros (Hcl & Hcl' & He). + do 2 (split; first (simpl; by erewrite <-dom_fmap)). + + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + exists (Λ, subst_map θ1 e1)%V, (Λ, subst_map θ2 e2)%V. + split; first constructor. + split; first constructor. + + simp type_interp. + eexists _, _. split_and!; try done. + - simpl. eapply subst_map_closed; simpl. + + replace (dom θ1) with (dom Γ). + * by erewrite <-dom_fmap. + * apply sem_context_rel_dom in Hctx. naive_solver. + + apply sem_context_rel_closed in Hctx. naive_solver. + - simpl. eapply subst_map_closed; simpl. + + replace (dom θ2) with (dom Γ). + * by erewrite <-dom_fmap. + * apply sem_context_rel_dom in Hctx. naive_solver. + + apply sem_context_rel_closed in Hctx. naive_solver. + - intros τ. eapply He. + by eapply sem_context_rel_cons. +Qed. + +Lemma compat_tapp Δ Γ e e' A B : + type_wf Δ B → + TY Δ; Γ ⊨ e ≈ e' : (∀: A) → + TY Δ; Γ ⊨ (e <>) ≈ (e' <>) : (A.[B/]). +Proof. + intros Hwf (Hecl & Hecl' & He). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + + (* TODO: exercise *) +Admitted. + + +Lemma compat_pack Δ Γ e e' n A B : + type_wf n B → + type_wf (S n) A → + TY n; Γ ⊨ e ≈ e': A.[B/] → + TY n; Γ ⊨ (pack e) ≈ (pack e') : (∃: A). +Proof. + intros Hwf Hwf' (Hecl & Hecl' & He). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + + (* TODO: exercise *) +Admitted. + + +Lemma compat_unpack n Γ A B e1 e1' e2 e2' x : + type_wf n B → + TY n; Γ ⊨ e1 ≈ e2 : (∃: A) → + TY S n; <[x:=A]> (⤉Γ) ⊨ e1' ≈ e2' : B.[ren (+1)] → + TY n; Γ ⊨ (unpack e1 as BNamed x in e1') ≈ (unpack e2 as BNamed x in e2') : B. +Proof. + intros Hwf (Hecl & Hecl' & He) (He'cl & He'cl' & He'). + split. { simpl. apply andb_True. split; first done. + eapply is_closed_weaken; set_solver. } + split. { simpl. apply andb_True. split; first done. + eapply is_closed_weaken; set_solver. } + intros θ1 θ2 δ Hctx. simpl. + + (* TODO: exercise *) +Admitted. + + +Lemma compat_if n Γ e0 e0' e1 e1' e2 e2' A : + TY n; Γ ⊨ e0 ≈ e0' : Bool → + TY n; Γ ⊨ e1 ≈ e1' : A → + TY n; Γ ⊨ e2 ≈ e2' : A → + TY n; Γ ⊨ (if: e0 then e1 else e2) ≈ (if: e0' then e1' else e2') : A. +Proof. + intros (He0cl & He0cl' & He0) (He1cl & He1cl' & He1) (He2cl & He2cl' & He2). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + + specialize (He0 _ _ _ Hctx). simp type_interp in He0. + specialize (He1 _ _ _ Hctx). simp type_interp in He1. + specialize (He2 _ _ _ Hctx). simp type_interp in He2. + + destruct He0 as (v0 & v0' & Hb0 & Hb0' & Hv0). simp type_interp in Hv0. + destruct Hv0 as (b & -> & ->). + destruct He1 as (v1 & w1 & Hb1 & Hb1' & Hv1). + destruct He2 as (v2 & w2 & Hb2 & Hb2' & Hv2). + + destruct b. + - exists v1, w1. split_and!; try by repeat econstructor. + - exists v2, w2. split_and!; try by repeat econstructor. +Qed. + +Lemma compat_pair Δ Γ e1 e1' e2 e2' A B : + TY Δ; Γ ⊨ e1 ≈ e1' : A → + TY Δ; Γ ⊨ e2 ≈ e2' : B → + TY Δ; Γ ⊨ (e1, e2) ≈ (e1', e2') : A × B. +Proof. + intros (He1cl & He1cl' & He1) (He2cl & He2cl' & He2). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + + specialize (He1 _ _ _ Hctx). specialize (He2 _ _ _ Hctx). + simp type_interp in He1. simp type_interp in He2. + + destruct He1 as (v1 & v1' & Hb1 & Hb1' & Hv1). + destruct He2 as (v2 & v2' & Hb2 & Hb2' & Hv2). + simp type_interp in Hv1, Hv2. + eexists _, _. split_and!; try by econstructor. + simp type_interp. eexists _, _, _, _. + split_and!; eauto. +Qed. + +Lemma compat_fst Δ Γ e e' A B : + TY Δ; Γ ⊨ e ≈ e' : A × B → + TY Δ; Γ ⊨ Fst e ≈ Fst e' : A. +Proof. + intros (Hecl & Hecl' & He). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + + specialize (He _ _ _ Hctx). simp type_interp in He. + destruct He as (v & v' & Hb & Hb' & Hv). + simp type_interp in Hv. + destruct Hv as (v1 & v2 & w1 & w2 & -> & -> & Hv & Hw). + eexists _, _. + split_and!; eauto. +Qed. + +Lemma compat_snd Δ Γ e e' A B : + TY Δ; Γ ⊨ e ≈ e' : A × B → + TY Δ; Γ ⊨ Snd e ≈ Snd e' : B. +Proof. + intros (Hecl & Hecl' & He). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + + specialize (He _ _ _ Hctx). simp type_interp in He. + destruct He as (v & v' & Hb & Hb' & Hv). + simp type_interp in Hv. + destruct Hv as (v1 & v2 & w1 & w2 & -> & -> & Hv & Hw). + eexists _, _. + split_and!; eauto. +Qed. + +Lemma compat_injl Δ Γ e e' A B : + TY Δ; Γ ⊨ e ≈ e' : A → + TY Δ; Γ ⊨ InjL e ≈ InjL e' : A + B. +Proof. + intros (Hecl & Hecl' & He). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + + specialize (He _ _ _ Hctx). simp type_interp in He. + destruct He as (v & v' & Hb & Hb' & Hv). + simp type_interp in Hv. + eexists _, _. + split_and!; eauto. + simp type_interp. + left. eexists _, _. split_and!; eauto. +Qed. + +Lemma compat_injr Δ Γ e e' A B : + TY Δ; Γ ⊨ e ≈ e' : B → + TY Δ; Γ ⊨ InjR e ≈ InjR e' : A + B. +Proof. + intros (Hecl & Hecl' & He). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + + specialize (He _ _ _ Hctx). simp type_interp in He. + destruct He as (v & v' & Hb & Hb' & Hv). + simp type_interp in Hv. + eexists _, _. + split_and!; eauto. + simp type_interp. + right. eexists _, _. split_and!; eauto. +Qed. + +Lemma compat_case Δ Γ e e' e1 e1' e2 e2' A B C : + TY Δ; Γ ⊨ e ≈ e' : B + C → + TY Δ; Γ ⊨ e1 ≈ e1' : (B → A) → + TY Δ; Γ ⊨ e2 ≈ e2' : (C → A) → + TY Δ; Γ ⊨ Case e e1 e2 ≈ Case e' e1' e2' : A. +Proof. + intros (He0cl & He0cl' & He0) (He1cl & He1cl' & He1) (He2cl & He2cl' & He2). + do 2 (split; first naive_solver). + intros θ1 θ2 δ Hctx. simpl. + simp type_interp. + + specialize (He0 _ _ _ Hctx). simp type_interp in He0. + specialize (He1 _ _ _ Hctx). simp type_interp in He1. + specialize (He2 _ _ _ Hctx). simp type_interp in He2. + + destruct He0 as (v0 & v0' & Hb0 & Hb0' & Hv0). simp type_interp in Hv0. + destruct He1 as (v1 & w1 & Hb1 & Hb1' & Hv1). + destruct He2 as (v2 & w2 & Hb2 & Hb2' & Hv2). + + destruct Hv0 as [(v' & w' & -> & -> & Hv)|(v' & w' & -> & -> & Hv)]. + - simp type_interp in Hv1. destruct Hv1 as (x & y & e'' & e''' & -> & -> & Cl & Cl' & Hv1). + apply Hv1 in Hv. simp type_interp in Hv. destruct Hv as (v & w & Hb''' & Hb'''' & Hv''). + eexists _, _. split_and!; eauto using big_step, big_step_of_val. + - simp type_interp in Hv2. destruct Hv2 as (x & y & e'' & e''' & -> & -> & Cl & Cl' & Hv2). + apply Hv2 in Hv. simp type_interp in Hv. destruct Hv as (v & w & Hb''' & Hb'''' & Hv''). + eexists _, _. split_and!; eauto using big_step, big_step_of_val. +Qed. + + + +(* we register the compatibility lemmas with eauto *) +Local Hint Resolve + compat_var compat_lam_named compat_lam_anon + compat_tlam compat_tapp compat_pack compat_unpack + compat_int compat_bool compat_unit compat_if + compat_app compat_int_binop compat_int_bool_binop + compat_unop compat_pair compat_fst compat_snd + compat_injl compat_injr compat_case : core. + + + + + +Lemma sem_soundness Δ Γ e A : + TY Δ; Γ ⊢ e : A → + TY Δ; Γ ⊨ e ≈ e : A. +Proof. + induction 1 as [ | Δ Γ x e A B Hsyn IH | Δ Γ e A B Hsyn IH| Δ Γ e A Hsyn IH| | | | | | | | | n Γ e1 e2 op A B C [] ? ? ? ? | | | | | | | ]; eauto. +Qed. + + +Program Definition any_type : sem_type := {| sem_type_car := λ v w, is_closed [] v ∧ is_closed [] w |}. +Definition δ_any : var → sem_type := λ _, any_type. + + + +(* Contextual Equivalence *) +Inductive pctx := + | HolePCtx + | AppLPCtx (C: pctx) (e2 : expr) + | AppRPCtx (e1 : expr) (C: pctx) + | TAppPCtx (C: pctx) + | PackPCtx (C: pctx) + | UnpackLPCtx (x : binder)(C: pctx) (e2 : expr) + | UnpackRPCtx (x : binder) (e1 : expr) (C: pctx) + | UnOpPCtx (op : un_op) (C: pctx) + | BinOpLPCtx (op : bin_op) (C: pctx) (e2 : expr) + | BinOpRPCtx (op : bin_op) (e1 : expr) (C: pctx) + | IfPCtx (C: pctx) (e1 e2 : expr) + | IfTPCtx (e: expr) (C: pctx) (e2 : expr) + | IfEPCtx (e e1: expr) (C: pctx) + | PairLPCtx (C: pctx) (e2 : expr) + | PairRPCtx (e1 : expr) (C: pctx) + | FstPCtx (C: pctx) + | SndPCtx (C: pctx) + | InjLPCtx (C: pctx) + | InjRPCtx (C: pctx) + | CasePCtx (C: pctx) (e1 e2 : expr) + | CaseTPCtx (e: expr) (C: pctx) (e2 : expr) + | CaseEPCtx (e e1: expr) (C: pctx) + | LamPCtx (x: binder) (C: pctx) + | TLamPCtx (C: pctx). + +Fixpoint pfill (C : pctx) (e : expr) : expr := + match C with + | HolePCtx => e + | AppLPCtx K e2 => App (pfill K e) e2 + | AppRPCtx e1 K => App e1 (pfill K e) + | TAppPCtx K => TApp (pfill K e) + | PackPCtx K => Pack (pfill K e) + | UnpackLPCtx x K e2 => Unpack x (pfill K e) e2 + | UnpackRPCtx x e1 K => Unpack x e1 (pfill K e) + | UnOpPCtx op K => UnOp op (pfill K e) + | BinOpLPCtx op K e2 => BinOp op (pfill K e) e2 + | BinOpRPCtx op e1 K => BinOp op e1 (pfill K e) + | IfPCtx K e1 e2 => If (pfill K e) e1 e2 + | IfTPCtx e' K e2 => If e' (pfill K e) e2 + | IfEPCtx e' e1 K => If e' e1 (pfill K e) + | PairLPCtx K e2 => Pair (pfill K e) e2 + | PairRPCtx e1 K => Pair e1 (pfill K e) + | FstPCtx K => Fst (pfill K e) + | SndPCtx K => Snd (pfill K e) + | InjLPCtx K => InjL (pfill K e) + | InjRPCtx K => InjR (pfill K e) + | CasePCtx K e1 e2 => Case (pfill K e) e1 e2 + | CaseTPCtx e' K e2 => Case e' (pfill K e) e2 + | CaseEPCtx e' e1 K => Case e' e1 (pfill K e) + | LamPCtx x C => Lam x (pfill C e) + | TLamPCtx C => TLam (pfill C e) + end. + + +Inductive pctx_typed (Δ: nat) (Γ: typing_context) (A: type): pctx → nat → typing_context → type → Prop := + | pctx_typed_HolePCtx : pctx_typed Δ Γ A HolePCtx Δ Γ A + | pctx_typed_AppLPCtx K e2 B C Δ' Γ': + pctx_typed Δ Γ A K Δ' Γ' (B → C) → + TY Δ'; Γ' ⊢ e2 : B → + pctx_typed Δ Γ A (AppLPCtx K e2) Δ' Γ' C + | pctx_typed_AppRPCtx e1 K B C Δ' Γ': + (TY Δ'; Γ' ⊢ e1 : Fun B C) → + pctx_typed Δ Γ A K Δ' Γ' B → + pctx_typed Δ Γ A (AppRPCtx e1 K) Δ' Γ' C + | pctx_typed_TLamPCtx K B Δ' Γ': + pctx_typed Δ Γ A K (S Δ') (⤉ Γ') B → + pctx_typed Δ Γ A (TLamPCtx K) Δ' Γ' (∀: B) + | pctx_typed_TAppPCtx K B C Δ' Γ': + type_wf Δ' C → + pctx_typed Δ Γ A K Δ' Γ' (∀: B) → + pctx_typed Δ Γ A (TAppPCtx K) Δ' Γ' (B.[C/]) + | pctx_typed_PackPCtx K B C Δ' Γ': + type_wf Δ' C → + type_wf (S Δ') B → + pctx_typed Δ Γ A K Δ' Γ' (B.[C/]) → + pctx_typed Δ Γ A (PackPCtx K) Δ' Γ' (∃: B) + | pctx_typed_UnpackLPCtx (x: string) K e2 B C Δ' Γ' : + type_wf Δ' C → + pctx_typed Δ Γ A K Δ' Γ' (∃: B) → + (TY S Δ'; (<[x := B]> (⤉ Γ')) ⊢ e2 : C.[ren (+1)]) → + pctx_typed Δ Γ A (UnpackLPCtx x K e2) Δ' Γ' C + | pctx_typed_UnpackRPCtx (x: string) e1 K B C Δ' Γ' : + type_wf Δ' C → + (TY Δ'; Γ' ⊢ e1 : (∃: B)) → + (pctx_typed Δ Γ A K (S Δ') (<[x := B]> (⤉ Γ')) (C.[ren (+1)])) → + pctx_typed Δ Γ A (UnpackRPCtx x e1 K) Δ' Γ' C + | pctx_typed_UnOpPCtx op K Δ' Γ' B C: + un_op_typed op B C → + pctx_typed Δ Γ A K Δ' Γ' B → + pctx_typed Δ Γ A (UnOpPCtx op K) Δ' Γ' C + | pctx_typed_BinOpLPCtx op K e2 B1 B2 C Δ' Γ' : + bin_op_typed op B1 B2 C → + pctx_typed Δ Γ A K Δ' Γ' B1 → + TY Δ'; Γ' ⊢ e2 : B2 → + pctx_typed Δ Γ A (BinOpLPCtx op K e2) Δ' Γ' C + | pctx_typed_BinOpRPCtx op K e1 B1 B2 C Δ' Γ' : + bin_op_typed op B1 B2 C → + TY Δ'; Γ' ⊢ e1 : B1 → + pctx_typed Δ Γ A K Δ' Γ' B2 → + pctx_typed Δ Γ A (BinOpRPCtx op e1 K) Δ' Γ' C + | pctx_typed_IfPCtx K e1 e2 B Δ' Γ' : + pctx_typed Δ Γ A K Δ' Γ' Bool → + TY Δ'; Γ' ⊢ e1 : B → + TY Δ'; Γ' ⊢ e2 : B → + pctx_typed Δ Γ A (IfPCtx K e1 e2) Δ' Γ' B + | pctx_typed_IfTPCtx K e e2 B Δ' Γ' : + TY Δ'; Γ' ⊢ e : Bool → + pctx_typed Δ Γ A K Δ' Γ' B → + TY Δ'; Γ' ⊢ e2 : B → + pctx_typed Δ Γ A (IfTPCtx e K e2) Δ' Γ' B + | pctx_typed_IfEPCtx K e e1 B Δ' Γ' : + TY Δ'; Γ' ⊢ e : Bool → + TY Δ'; Γ' ⊢ e1 : B → + pctx_typed Δ Γ A K Δ' Γ' B → + pctx_typed Δ Γ A (IfEPCtx e e1 K) Δ' Γ' B + | pctx_typed_PairLPCtx K e2 B1 B2 Δ' Γ' : + pctx_typed Δ Γ A K Δ' Γ' B1 → + TY Δ'; Γ' ⊢ e2 : B2 → + pctx_typed Δ Γ A (PairLPCtx K e2) Δ' Γ' (Prod B1 B2) + | pctx_typed_PairRPCtx K e1 B1 B2 Δ' Γ' : + TY Δ'; Γ' ⊢ e1 : B1 → + pctx_typed Δ Γ A K Δ' Γ' B2 → + pctx_typed Δ Γ A (PairRPCtx e1 K) Δ' Γ' (Prod B1 B2) + | pctx_typed_FstPCtx K Δ' Γ' B C: + pctx_typed Δ Γ A K Δ' Γ' (Prod B C) → + pctx_typed Δ Γ A (FstPCtx K) Δ' Γ' B + | pctx_typed_SndPCtx K Δ' Γ' B C: + pctx_typed Δ Γ A K Δ' Γ' (Prod B C) → + pctx_typed Δ Γ A (SndPCtx K) Δ' Γ' C + | pctx_typed_InjLPCtx K Δ' Γ' B C: + type_wf Δ' C → + pctx_typed Δ Γ A K Δ' Γ' B → + pctx_typed Δ Γ A (InjLPCtx K) Δ' Γ' (Sum B C) + | pctx_typed_InjRPCtx K Δ' Γ' B C: + type_wf Δ' B → + pctx_typed Δ Γ A K Δ' Γ' C → + pctx_typed Δ Γ A (InjRPCtx K) Δ' Γ' (Sum B C) + | pctx_typed_CasePCtx K e1 e2 B C D Δ' Γ' : + pctx_typed Δ Γ A K Δ' Γ' (Sum B C) → + TY Δ'; Γ' ⊢ e1 : (Fun B D) → + TY Δ'; Γ' ⊢ e2 : (Fun C D) → + pctx_typed Δ Γ A (CasePCtx K e1 e2) Δ' Γ' D + | pctx_typed_CaseTPCtx K e e2 B C D Δ' Γ' : + TY Δ'; Γ' ⊢ e : (Sum B C) → + pctx_typed Δ Γ A K Δ' Γ' (Fun B D) → + TY Δ'; Γ' ⊢ e2 : (Fun C D) → + pctx_typed Δ Γ A (CaseTPCtx e K e2) Δ' Γ' D + | pctx_typed_CaseEPCtx K e e1 B C D Δ' Γ' : + TY Δ'; Γ' ⊢ e : (Sum B C) → + TY Δ'; Γ' ⊢ e1 : (Fun B D) → + pctx_typed Δ Γ A K Δ' Γ' (Fun C D) → + pctx_typed Δ Γ A (CaseEPCtx e e1 K) Δ' Γ' D + | pctx_typed_named_LamPCtx (x: string) K B C Γ' Δ' : + type_wf Δ' B → + pctx_typed Δ Γ A K Δ' (<[x := B]> Γ') C → + pctx_typed Δ Γ A (LamPCtx x K) Δ' Γ' (Fun B C) + | pctx_typed_anon_LamPCtx K B C Γ' Δ' : + type_wf Δ' B → + pctx_typed Δ Γ A K Δ' Γ' C → + pctx_typed Δ Γ A (LamPCtx BAnon K) Δ' Γ' (Fun B C) + . + + +Lemma pfill_typed C Δ Δ' Γ Γ' e A B: + pctx_typed Δ Γ A C Δ' Γ' B → TY Δ; Γ ⊢ e : A → TY Δ'; Γ' ⊢ pfill C e : B. +Proof. + induction 1 in |-*; simpl; eauto using pctx_typed. +Qed. + + +Lemma syn_typed_closed Δ Γ A e: + TY Δ; Γ ⊢ e : A → + is_closed (elements (dom Γ)) e. +Proof. + intros Hty; eapply syn_typed_closed; eauto. + intros x Hx. by eapply elem_of_elements. +Qed. + +Lemma pctx_typed_fill_closed Δ Δ' Γ Γ' A B K e: + is_closed (elements (dom Γ)) e → + pctx_typed Δ Γ A K Δ' Γ' B → + is_closed (elements (dom Γ')) (pfill K e). +Proof. + intros Hcl. induction 1; simplify_closed; eauto using syn_typed_closed. + - eapply is_closed_weaken; first by eapply syn_typed_closed. + rewrite dom_insert. + intros y Hin. destruct (decide (x = y)); subst; first set_solver. + eapply elem_of_elements in Hin. eapply elem_of_union in Hin as []. + + set_solver. + + rewrite dom_fmap in H2. eapply elem_of_list_further. + by eapply elem_of_elements. + - rewrite dom_insert. + intros y Hin. destruct (decide (x = y)); subst; first set_solver. + eapply elem_of_elements in Hin. eapply elem_of_union in Hin as []. + + set_solver. + + rewrite dom_fmap in H2. eapply elem_of_list_further. + by eapply elem_of_elements. + - rewrite dom_insert. + intros y Hin. destruct (decide (x = y)); subst; first set_solver. + eapply elem_of_elements in Hin. eapply elem_of_union in Hin as []. + + set_solver. + + eapply elem_of_list_further. + by eapply elem_of_elements. +Qed. + + +Lemma sem_typed_congruence Δ Δ' Γ Γ' e1 e2 C A B : + closed (elements (dom Γ)) e1 → + closed (elements (dom Γ)) e2 → + TY Δ; Γ ⊨ e1 ≈ e2 : A → + pctx_typed Δ Γ A C Δ' Γ' B → + TY Δ'; Γ' ⊨ pfill C e1 ≈ pfill C e2 : B. +Proof. + intros ???. + induction 1; simpl; eauto using sem_soundness. + - inversion H2; subst; eauto using sem_soundness. + - inversion H2; subst; eauto using sem_soundness. +Qed. + +Lemma adequacy δ e1 e2: ℰ Int δ e1 e2 → ∃ n, big_step e1 n ∧ big_step e2 n. +Proof. + simp type_interp. intros (? & ? & ? & ? & Hty). + simp type_interp in Hty. naive_solver. +Qed. + + +Definition ctx_equiv Δ Γ e1 e2 A := + ∀ K, pctx_typed Δ Γ A K 0 ∅ Int → ∃ n: Z, big_step (pfill K e1) #n ∧ big_step (pfill K e2) #n. + + +Lemma sem_typing_ctx_equiv Δ Γ e1 e2 A : + (* the closedness assumptions could be replaced by typing assumptions *) + closed (elements (dom Γ)) e1 → + closed (elements (dom Γ)) e2 → + TY Δ; Γ ⊨ e1 ≈ e2 : A → ctx_equiv Δ Γ e1 e2 A. +Proof. + intros Hcl Hcl' Hsem C Hty. eapply sem_typed_congruence in Hty as (Htycl & Htycl' & Hty); last done. + all: try done. + opose proof* (Hty ∅ ∅ δ_any) as He; first constructor. + revert He. rewrite !subst_map_empty. + simp type_interp. destruct 1 as (v1 & v2 & Hbs1 & Hbs2 & Hv). + simp type_interp in Hv. destruct Hv as (z & -> & ->). eauto. +Qed. + +Lemma soundness_wrt_ctx_equiv Δ Γ e1 e2 A : + TY Δ; Γ ⊢ e1 : A → + TY Δ; Γ ⊢ e2 : A → + TY Δ; Γ ⊨ e1 ≈ e2 : A → + ctx_equiv Δ Γ e1 e2 A. +Proof. + intros ???; eapply sem_typing_ctx_equiv; eauto. + all: by eapply syn_typed_closed. +Qed. diff --git a/theories/type_systems/systemf/church_encodings.v b/theories/type_systems/systemf/church_encodings.v new file mode 100644 index 0000000..9578db5 --- /dev/null +++ b/theories/type_systems/systemf/church_encodings.v @@ -0,0 +1,173 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.lib Require Export debruijn. +From semantics.ts.systemf Require Import lang notation types bigstep tactics. + +(** * Church encodings *) +Implicit Types + (Δ : nat) + (Γ : typing_context) + (v : val) + (α : var) + (e : expr) + (A : type). + +Definition empty_type : type := ∀: #0. + +(** *** Unit *) +Definition unit_type : type := ∀: #0 → #0. +Definition unit_inh : val := Λ, λ: "x", "x". + +Lemma unit_wf n : type_wf n unit_type. +Proof. solve_typing. Qed. +Lemma unit_inh_typed n Γ : TY n; Γ ⊢ unit_inh : unit_type. +Proof. solve_typing. Qed. + +(** *** Bool *) +Definition bool_type : type := ∀: #0 → #0 → #0. +Definition bool_true : val := Λ, λ: "t" "f", "t". +Definition bool_false : val := Λ, λ: "t" "f", "f". +Definition bool_if e e1 e2 : expr := (e <> (λ: <>, e1)%E (λ: <>, e2)%E) unit_inh. + +Lemma bool_true_typed n Γ : TY n; Γ ⊢ bool_true : bool_type. +Proof. solve_typing. Qed. +Lemma bool_false_typed n Γ: TY n; Γ ⊢ bool_false : bool_type. +Proof. solve_typing. Qed. + +Lemma bool_if_typed n Γ e e1 e2 A : + type_wf n A → + TY n; Γ ⊢ e1 : A → + TY n; Γ ⊢ e2 : A → + TY n; Γ ⊢ e : bool_type → + TY n; Γ ⊢ bool_if e e1 e2 : A. +Proof. + intros. solve_typing. + apply unit_wf. + all: solve_typing. +Qed. + +Lemma bool_if_true_red e1 e2 v : + is_closed [] e1 → + big_step e1 v → + big_step (bool_if bool_true e1 e2)%E v. +Proof. + intros. bs_step_det. +Qed. + +Lemma bool_if_false_red e1 e2 v : + is_closed [] e2 → + big_step e2 v → + big_step (bool_if bool_false e1 e2)%E v. +Proof. + intros. bs_step_det. +Qed. + +(** *** Product types *) +(* Using De Bruijn indices, we need to be a bit careful: + The binder introduced by [∀:] should not be visible in [A] and [B]. + Therefore, we need to shift [A] and [B] up by one, using the renaming substitution [ren]. + *) +Definition product_type (A B : type) : type := ∀: (A.[ren (+1)] → B.[ren (+1)] → #0) → #0. +Definition pair_val (v1 v2 : val) : val := Λ, λ: "p", "p" v1 v2. +Definition pair_expr (e1 e2 : expr) : expr := + let: "x2" := e2 in + let: "x1" := e1 in + Λ, λ: "p", "p" "x1" "x2". +Definition proj1_expr (e : expr) : expr := e <> (λ: "x" "y", "x")%E. +Definition proj2_expr (e : expr) : expr := e <> (λ: "x" "y", "y")%E. + +Lemma proj1_red v1 v2 : + is_closed [] v1 → + is_closed [] v2 → + big_step (proj1_expr (pair_val v1 v2)) v1. +Proof. + intros. bs_step_det. + rewrite subst_is_closed_nil; last done. + bs_step_det. +Qed. +Lemma proj2_red v1 v2 : + is_closed [] v1 → + is_closed [] v2 → + big_step (proj2_expr (pair_val v1 v2)) v2. +Proof. + intros. bs_steps_det. +Qed. + +Lemma pair_red e1 e2 v1 v2 : + is_closed [] v2 → + is_closed [] e1 → + big_step e1 v1 → + big_step e2 v2 → + big_step (pair_expr e1 e2) (pair_val v1 v2). +Proof. + intros. bs_steps_det. +Qed. + +Lemma proj1_typed n Γ e A B : + type_wf n A → + type_wf n B → + TY n; Γ ⊢ e : product_type A B → + TY n; Γ ⊢ proj1_expr e : A. +Proof. + intros. solve_typing. +Qed. + +Lemma proj2_typed n Γ e A B : + type_wf n A → + type_wf n B → + TY n; Γ ⊢ e : product_type A B → + TY n; Γ ⊢ proj2_expr e : B. +Proof. + intros. solve_typing. +Qed. + +(** We need to assume that x2 is not bound by Γ. + This is a bit annoying, as it puts a restriction on the context in which this typing rule + can be used. + Alternatively, we could parameterize the encoding of [pair_expr] by a name to use, + so that we can always choose a name for it that does not conflict with Γ. +*) +Lemma pair_expr_typed n Γ e1 e2 A B : + Γ !! "x2" = None → + type_wf n A → + type_wf n B → + TY n; Γ ⊢ e1 : A → + TY n; Γ ⊢ e2 : B → + TY n; Γ ⊢ pair_expr e1 e2 : product_type A B. +Proof. + intros. + solve_typing. + eapply typed_weakening; [done | | lia]. apply insert_subseteq. done. +Qed. + + +(** *** Church numerals *) +Definition nat_type : type := ∀: #0 → (#0 → #0) → #0. +Definition zero_val : val := Λ, λ: "z" "s", "z". +Definition num_val (n : nat) : val := Λ, λ: "z" "s", Nat.iter n (App "s") "z". +Definition succ_val : val := λ: "n", Λ, λ: "z" "s", "s" ("n" <> "z" "s"). +Definition iter_val : val := λ: "n" "z" "s", "n" <> "z" "s". + +Lemma zero_typed Γ n : TY n; Γ ⊢ zero_val : nat_type. +Proof. solve_typing. Qed. + +Lemma num_typed Γ n m : TY n; Γ ⊢ num_val m : nat_type. +Proof. + solve_typing. + induction m as [ | m IH]; simpl. + - solve_typing. + - solve_typing. +Qed. + +Lemma succ_typed Γ n : + TY n; Γ ⊢ succ_val : (nat_type → nat_type). +Proof. + solve_typing. +Qed. + +Lemma iter_typed n Γ C : + type_wf n C → + TY n; Γ ⊢ iter_val : (nat_type → C → (C → C) → C). +Proof. + intros. solve_typing. +Qed. diff --git a/theories/type_systems/systemf/exercises04_sol.v b/theories/type_systems/systemf/exercises04_sol.v new file mode 100644 index 0000000..71cd5f9 --- /dev/null +++ b/theories/type_systems/systemf/exercises04_sol.v @@ -0,0 +1,454 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.ts.systemf Require Import lang notation parallel_subst types logrel tactics. + +(** Exercise 1 (LN Exercise 19): De Bruijn Terms *) +Module dbterm. + (** Your type of expressions only needs to encompass the operations of our base lambda calculus. *) + Inductive expr := + | Lit (l : base_lit) + | Var (n : nat) + | Lam (e : expr) + | Plus (e1 e2 : expr) + | App (e1 e2 : expr) + . + + (** Formalize substitutions and renamings as functions. *) + Definition subt := nat → expr. + Definition rent := nat → nat. + + Implicit Types + (σ : subt) + (δ : rent) + (n x : nat) + (e : expr). + + + + (* Operations on renamings *) + Definition RCons n δ x := + match x with + | 0 => n + | S x => δ x + end. + Definition RComp δ1 δ2 := δ1 ∘ δ2. + Definition RUp δ := RCons 0 (RComp S δ). + + Fixpoint ren_expr δ e := + match e with + | Lit l => Lit l + | Var x => Var (δ x) + | Lam e => Lam (ren_expr (RUp δ) e) + | App e1 e2 => App (ren_expr δ e1) (ren_expr δ e2) + | Plus e1 e2 => Plus (ren_expr δ e1) (ren_expr δ e2) + end. + + (* Operations on substitutions *) + Definition Cons e σ x := + match x with + | 0 => e + | S x => σ x + end. + Definition ren_subst δ σ n := ren_expr δ (σ n). + Definition Up σ := Cons (Var 0) (ren_subst S σ). + + Fixpoint subst σ e := + match e with + | Lit l => Lit l + | Var x => σ x + | Lam e => Lam (subst (Up σ) e) + | App e1 e2 => App (subst σ e1) (subst σ e2) + | Plus e1 e2 => Plus (subst σ e1) (subst σ e2) + end. + + Goal (subst + (λ n, match n with + | 0 => Lit (LitInt 42) + | 1 => Var 0 + | _ => Var n + end) + (Lam (Plus (Plus (Var 2) (Var 1)) (Var 0)))) = + Lam (Plus (Plus (Var 1) (Lit 42%Z)) (Var 0)). + Proof. + cbn. + (* Should be by reflexivity. *) + reflexivity. + Qed. + +End dbterm. + +Section church_encodings. + (** Exercise 2 (LN Exercise 24): Church encoding, sum types *) + (* a) Define your encoding *) + Definition sum_type (A B : type) : type := + ∀: (A.[ren (+1)] → #0) → (B.[ren (+1)] → #0) → #0. + + (* b) Implement inj1, inj2, case *) + Definition injl_val (v : val) : val := Λ, λ: "f" "g", "f" v. + Definition injl_expr (e : expr) : expr := let: "x" := e in Λ, λ: "f" "g", "f" "x". + Definition injr_val (v : val) : val := Λ, λ: "f" "g", "g" v. + Definition injr_expr (e : expr) : expr := let: "x" := e in Λ, λ: "f" "g", "g" "x". + + (* You may want to use the variables x1, x2 for the match arms to fit the typing statements below. *) + Definition match_expr (e : expr) (e1 e2 : expr) : expr := + (e <> (λ: "x1", e1) (λ: "x2", e2))%E. + + (* c) Reduction behavior *) + (* Some lemmas about substitutions might be useful. Look near the end of the lang.v file! *) + Lemma match_expr_red_injl e e1 e2 (vl v' : val) : + is_closed [] vl → + is_closed ["x1"] e1 → + big_step e (injl_val vl) → + big_step (subst' "x1" vl e1) v' → + big_step (match_expr e e1 e2) v'. + Proof. + intros. bs_step_det. + erewrite (lang.subst_is_closed ["x1"] _ "g"); [ done | done | rewrite elem_of_list_singleton; done]. + Qed. + + Lemma match_expr_red_injr e e1 e2 (vl v' : val) : + is_closed [] vl → + big_step e (injr_val vl) → + big_step (subst' "x2" vl e2) v' → + big_step (match_expr e e1 e2) v'. + Proof. + intros. bs_step_det. + Qed. + + Lemma injr_expr_red e v : + big_step e v → + big_step (injr_expr e) (injr_val v). + Proof. + intros. bs_step_det. + Qed. + + Lemma injl_expr_red e v : + big_step e v → + big_step (injl_expr e) (injl_val v). + Proof. + intros. bs_step_det. + Qed. + + + (* d) Typing rules *) + Lemma sum_injl_typed n Γ (e : expr) A B : + type_wf n B → + type_wf n A → + TY n; Γ ⊢ e : A → + TY n; Γ ⊢ injl_expr e : sum_type A B. + Proof. + intros. solve_typing. + Qed. + + Lemma sum_injr_typed n Γ e A B : + type_wf n B → + type_wf n A → + TY n; Γ ⊢ e : B → + TY n; Γ ⊢ injr_expr e : sum_type A B. + Proof. + intros. solve_typing. + Qed. + + Lemma sum_match_typed n Γ A B C e e1 e2 : + type_wf n A → + type_wf n B → + type_wf n C → + TY n; Γ ⊢ e : sum_type A B → + TY n; <["x1" := A]> Γ ⊢ e1 : C → + TY n; <["x2" := B]> Γ ⊢ e2 : C → + TY n; Γ ⊢ match_expr e e1 e2 : C. + Proof. + intros. solve_typing. + Qed. + + + (** Exercise 3 (LN Exercise 25): church encoding, list types *) + + (* a) translate the type of lists into De Bruijn. *) + Definition list_type (A : type) : type := + ∀: #0 → (A.[ren (+1)] → #0 → #0) → #0. + + (* b) Implement nil and cons. *) + Definition nil_val : val := Λ, λ: "e" "c", "e". + Definition cons_val (v1 v2 : val) : val := Λ, λ: "e" "c", "c" v1 (v2 <> "e" "c"). + Definition cons_expr (e1 e2 : expr) : expr := + let: "p" := (e1, e2) in Λ, λ: "e" "c", "c" (Fst "p") ((Snd "p") <> "e" "c"). + + (* c) Define typing rules and prove them *) + Lemma nil_typed n Γ A : + type_wf n A → + TY n; Γ ⊢ nil_val : list_type A. + Proof. + intros. solve_typing. + Qed. + + Lemma cons_typed n Γ (e1 e2 : expr) A : + type_wf n A → + TY n; Γ ⊢ e2 : list_type A → + TY n; Γ ⊢ e1 : A → + TY n; Γ ⊢ cons_expr e1 e2 : list_type A. + Proof. + intros. repeat solve_typing. + Qed. + + (* d) Define a function head of type list A → A + 1 *) + Definition head : val := + λ: "l", "l" <> (InjR #LitUnit) (λ: "h" <>, InjL "h"). + + Lemma head_typed n Γ A : + type_wf n A → + TY n; Γ ⊢ head: (list_type A → (A + Unit)). + Proof. + intros. solve_typing. + Qed. + + (* e) Define a function [tail] of type list A → list A *) + Definition split : val := + λ: "l", "l" <> ((InjR #LitUnit), nil_val) + (λ: "h" "r", match: (Fst "r") with InjL "h'" => (InjL "h", let: "r'" := Snd "r" in cons_expr "h'" "r'") + | InjR <> => (InjL "h", Snd "r") + end). + Definition tail : val := + λ: "l", Snd (split "l"). + + Lemma tail_typed n Γ A : + type_wf n A → + TY n; Γ ⊢ tail: (list_type A → list_type A). + Proof. + intros. repeat solve_typing. + Admitted. + +End church_encodings. + +Section free_theorems. + + (** Exercise 4 (LN Exercise 27): Free Theorems I *) + (* a) State a free theorem for the type ∀ α, β. α → β → α × β *) + Lemma free_thm_1 : + ∀ f : val, + TY 0; ∅ ⊢ f : (∀: ∀: #1 → #0 → #1 × #0) → + ∀ (v1 v2 : val), is_closed [] v1 → is_closed [] v2 → + big_step (f <> <> v1 v2) (v1, v2)%V. + Proof. + intros f [Htycl Hty]%sem_soundness v1 v2 Hcl1 Hcl2. + specialize (Hty ∅ δ_any). simp type_interp in Hty. + destruct Hty as (v & Hb & Hv). + { constructor. } + + simp type_interp in Hv. destruct Hv as (e & -> & ? & Hv). + specialize_sem_type Hv with (λ v, v = v1) as τ1. + { naive_solver. } + simp type_interp in Hv. destruct Hv as (ve0 & ? & Hv). + + simp type_interp in Hv. destruct Hv as (e2 & -> & ? & Hv). + specialize_sem_type Hv with (λ v, v = v2) as τ2. + { naive_solver. } + simp type_interp in Hv. destruct Hv as (ve1 & ? & Hv). + + simp type_interp in Hv. destruct Hv as (x & e0 & -> & ? & Hv). + specialize (Hv v1). simp type_interp in Hv. simpl in Hv. + destruct Hv as (ve2 & ? & Hv); first done. + + simp type_interp in Hv. destruct Hv as (x' & e1 & -> & ? & Hv). + specialize (Hv v2). simp type_interp in Hv. simpl in Hv. + destruct Hv as (ve3 & ? & Hv); first done. + + simp type_interp in Hv. destruct Hv as (v1' & v2' & -> & Hv1 & Hv2). + simp type_interp in Hv1. simpl in Hv1. subst v1'. + simp type_interp in Hv2. simpl in Hv2. subst v2'. + + bs_step_det. + by rewrite subst_map_empty in Hb. + Qed. + + (* b) State a free theorem for the type ∀ α, β. α × β → α *) + Lemma free_thm_2 : + ∀ f : val, + TY 0; ∅ ⊢ f : (∀: ∀: #1 × #0 → #1) → + ∀ (v1 v2 : val), is_closed [] v1 → is_closed [] v2 → + big_step (f <> <> (v1, v2)%E) v1. + Proof. + intros f [Htycl Hty]%sem_soundness v1 v2 Hcl1 Hcl2. + specialize (Hty ∅ δ_any). simp type_interp in Hty. + destruct Hty as (v & Hb & Hv). + { constructor. } + + simp type_interp in Hv. destruct Hv as (? & -> & ? & Hv). + specialize_sem_type Hv with (λ v, v = v1) as τ1. + { naive_solver. } + simp type_interp in Hv. destruct Hv as (? & ? & Hv). + + simp type_interp in Hv. destruct Hv as (? & -> & ? & Hv). + specialize_sem_type Hv with (λ v, v = v2) as τ2. + { naive_solver. } + simp type_interp in Hv. destruct Hv as (? & ? & Hv). + + simp type_interp in Hv. destruct Hv as (? & ? & -> & ? & Hv). + specialize (Hv (v1, v2)%V). simp type_interp in Hv. simpl in Hv. + destruct Hv as (ve & ? & Hv). + { exists v1, v2. split_and!; first done. + all: simp type_interp; simpl; done. + } + + simp type_interp in Hv. simpl in Hv; subst ve. + rewrite subst_map_empty in Hb. + bs_step_det. + Qed. + + (* c) State a free theorem for the type ∀ α, β. α → β *) + Lemma free_thm_3 : + ∀ f : val, + TY 0; ∅ ⊢ f : (∀: ∀: #1 → #0) → + False. + Proof. + intros f [Htycl Hty]%sem_soundness. + specialize (Hty ∅ δ_any). simp type_interp in Hty. + destruct Hty as (v & Hb & Hv). + { constructor. } + + simp type_interp in Hv. destruct Hv as (? & -> & ? & Hv). + specialize_sem_type Hv with (λ v, v = #0) as τ1. + { naive_solver. } + simp type_interp in Hv. destruct Hv as (? & ? & Hv). + + simp type_interp in Hv. destruct Hv as (? & -> & ? & Hv). + specialize_sem_type Hv with (λ v, False) as τ2. + { naive_solver. } + simp type_interp in Hv. destruct Hv as (? & ? & Hv). + + simp type_interp in Hv. destruct Hv as (? & ? & -> & ? & Hv). + specialize (Hv #0). simp type_interp in Hv. simpl in Hv. + destruct Hv as (ve & ? & Hv). { done. } + + (* Oh no! *) + simp type_interp in Hv. simpl in Hv. done. + Qed. + + + (** Exercise 5 (LN Exercise 28): Free Theorems II *) + Lemma free_theorem_either : + ∀ f : val, + TY 0; ∅ ⊢ f : (∀: #0 → #0 → #0) → + ∀ (v1 v2 : val), is_closed [] v1 → is_closed [] v2 → + big_step (f <> v1 v2) v1 ∨ big_step (f <> v1 v2) v2. + Proof. + intros f [Htycl Hty]%sem_soundness v1 v2 Hcl1 Hcl2. + specialize (Hty ∅ δ_any). simp type_interp in Hty. + destruct Hty as (v & Hb & Hv). + { constructor. } + + simp type_interp in Hv. destruct Hv as (? & -> & ? & Hv). + specialize_sem_type Hv with (λ v, v = v1 ∨ v = v2) as τ. + { naive_solver. } + simp type_interp in Hv. destruct Hv as (? & ? & Hv). + + simp type_interp in Hv. destruct Hv as (? & ? & -> & ? & Hv). + specialize (Hv v1). simp type_interp in Hv. simpl in Hv. + destruct Hv as (ve & ? & Hv). { by left. } + + simp type_interp in Hv. destruct Hv as (? & ? & -> & ? & Hv). + specialize (Hv v2). simp type_interp in Hv. simpl in Hv. + destruct Hv as (ve & ? & Hv). { by right. } + + simp type_interp in Hv. simpl in Hv. + + rewrite subst_map_empty in Hb. + destruct Hv as [-> | ->]; [left | right]; bs_step_det. + Qed. + + (** Exercise 6 (LN Exercise 29): Free Theorems III *) + (* Hint: you might want to use the fact that our reduction is deterministic. *) + Lemma big_step_det e v1 v2 : + big_step e v1 → big_step e v2 → v1 = v2. + Proof. + induction 1 in v2 |-*; inversion 1; subst; eauto 2. + all: naive_solver. + Qed. + + Lemma free_theorems_magic : + ∀ (A A1 A2 : type) (f g : val), + type_wf 0 A → type_wf 0 A1 → type_wf 0 A2 → + is_closed [] f → is_closed [] g → + TY 0; ∅ ⊢ f : (∀: (A1 → A2 → #0) → #0) → + TY 0; ∅ ⊢ g : (A1 → A2 → A) → + ∀ v, big_step (f <> g) v → + ∃ (v1 v2 : val), big_step (g v1 v2) v. + Proof. + (* Hint: you may find the following lemmas useful: + - [sem_val_rel_cons] + - [type_wf_closed] + - [val_rel_is_closed] + - [big_step_preserve_closed] + *) + intros A A1 A2 f g HwfA HwfA1 HwfA2 Hclf Hclg [Htyfcl Htyf]%sem_soundness [Htygcl Htyg]%sem_soundness v Hb. + + specialize (Htyf ∅ δ_any). simp type_interp in Htyf. + destruct Htyf as (vf & Hbf & Hvf). + { constructor. } + + specialize (Htyg ∅ δ_any). simp type_interp in Htyg. + destruct Htyg as (vg & Hbg & Hvg). + { constructor. } + + rewrite subst_map_empty in Hbf. rewrite subst_map_empty in Hbg. + apply big_step_val in Hbf. apply big_step_val in Hbg. + subst vf vg. + + (* if we know that big_step is deterministic *) + (* We pick the interpretation [(λ v, ∃ v1 v2, big_step (g v1 v2) v)]. + Then we can equate the existential we get from Hvf with v, + since big step is deterministic. + + We need to show that g satisfies this interpretation. + For that, we already get v1: A1, v2:A2. + So we use the Hvg fact to get a : A with g v1 v2 ↓ a. + With that we can show the semantic interpretation. + *) + + simp type_interp in Hvf. destruct Hvf as (ef & -> & ? & Hvf). + specialize_sem_type Hvf with (λ v, + ∃ (v1 v2 : val), is_closed [] v1 ∧ is_closed [] v2 ∧ big_step (g v1 v2) v) as τ. + { intros v' (v1 & v2 & ? & ? & Hb'). + eapply big_step_preserve_closed. + 2: apply Hb'. + simpl. rewrite !andb_True. done. + } + simp type_interp in Hvf. destruct Hvf as (ve & ? & Hvf). + simp type_interp in Hvf. destruct Hvf as (? & ef' & -> & ? & Hvf). + + specialize (Hvf g). simp type_interp in Hvf. + destruct Hvf as (ve2 & Hbe2 & Hvf). + { simp type_interp in Hvg. destruct Hvg as (xg0 & eg0 & -> & ? & Hvg). + eexists _, _. split_and!; [done | done | ]. + intros v1 Hv1. + + specialize (Hvg v1). simp type_interp in Hvg. + destruct Hvg as (? & ? & Hvg). + { eapply sem_val_rel_cons. rewrite type_wf_closed; done. } + + simp type_interp in Hvg. destruct Hvg as (xg1 & eg1 & -> & ? & Hvg). + simp type_interp. eexists _. split; first done. + simp type_interp. eexists _, _. split_and!; [done | done | ]. + intros v2 Hv2. + + specialize (Hvg v2). simp type_interp in Hvg. + destruct Hvg as (? & ? & Hvg). + { eapply sem_val_rel_cons. rewrite type_wf_closed; done. } + + simp type_interp. eexists. split; first done. + simp type_interp. simpl. + + exists v1, v2. split_and!. + - eapply val_rel_closed; done. + - eapply val_rel_closed; done. + - bs_step_det. + } + simp type_interp in Hvf. simpl in Hvf. + destruct Hvf as (v1 & v2 & ? & ? & Hbs). + exists v1, v2. + assert (ve2 = v) as ->; last done. + eapply big_step_det; last apply Hb. + bs_step_det. + Qed. + +End free_theorems. diff --git a/theories/type_systems/systemf/exercises05.v b/theories/type_systems/systemf/exercises05.v new file mode 100644 index 0000000..b5b2415 --- /dev/null +++ b/theories/type_systems/systemf/exercises05.v @@ -0,0 +1,169 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.ts.systemf Require Import lang notation parallel_subst types tactics. +From semantics.ts.systemf Require logrel binary_logrel existential_invariants. + +(** * Exercise Sheet 5 *) + +Implicit Types + (e : expr) + (v : val) + (A B : type) +. + +(** ** Exercise 3 (LN Exercise 23): Existential Fun *) +Section existential. + (** Since extending our language with records would be tedious, + we encode records using nested pairs. + + For instance, we would represent the record type + { add : Int → Int → Int; sub : Int → Int → Int; neg : Int → Int } + as (Int → Int → Int) × (Int → Int → Int) × (Int → Int). + + Similarly, we would represent the record value + { add := λ: "x" "y", "x" + "y"; + sub := λ: "x" "y", "x" - "y"; + neg := λ: "x", #0 - "x" + } + as the nested pair + ((λ: "x" "y", "x" + "y", (* add *) + λ: "x" "y", "x" - "y"), (* sub *) + λ: "x", #0 - "x"). (* neg *) + + *) + + (** We will also assume a recursion combinator. We have not formally added it to our language, but we could do so. *) + Context (Fix : string → string → expr → val). + Notation "'fix:' f x := e" := (Fix f x e)%E + (at level 200, f, x at level 1, e at level 200, + format "'[' 'fix:' f x := '/ ' e ']'") : val_scope. + Notation "'fix:' f x := e" := (Fix f x e)%E + (at level 200, f, x at level 1, e at level 200, + format "'[' 'fix:' f x := '/ ' e ']'") : expr_scope. + Context (fix_typing : ∀ n Γ (f x: string) (A B: type) (e: expr), + type_wf n A → + type_wf n B → + f ≠ x → + TY n; <[x := A]> (<[f := (A → B)%ty]> Γ) ⊢ e : B → + TY n; Γ ⊢ (fix: f x := e) : (A → B)). + + Definition ISET : type :=#0. (* TODO: your definition *) + + (* We represent sets as functions of type ((Int → Bool) × Int × Int), + storing the mapping, the minimum value, and the maximum value. *) + + + Definition iset : val :=#0. (* TODO: your definition *) + + Lemma iset_typed n Γ : TY n; Γ ⊢ iset : ISET. + Proof. + (* HINT: use repeated solve_typing with an explicit apply fix_typing inbetween *) + (* TODO: exercise *) + Admitted. + + + Definition ISETE : type :=#0. (* TODO: your definition *) + + Definition add_equality : val :=#0. (* TODO: your definition *) + + Lemma add_equality_typed n Γ : TY n; Γ ⊢ add_equality : (ISET → ISETE)%ty. + Proof. + repeat solve_typing. + (* Qed. *) + (* TODO: exercise *) + Admitted. + + +End existential. + +Section ex4. +Import logrel existential_invariants. +(** ** Exercise 4 (LN Exercise 30): Evenness *) +(* Consider the following existential type: *) +Definition even_type : type := + ∃: (#0 × (* zero *) + (#0 → #0) × (* add2 *) + (#0 → Int) (* toint *) + )%ty. + +(* and consider the following implementation of [even_type]: *) +Definition even_impl : val := + pack (#0, + λ: "z", #2 + "z", + λ: "z", "z" + ). +(* We want to prove that [toint] will only every yield even numbers. *) +(* For that purpose, assume that we have a function [even] that decides even parity available: *) +Context (even_dec : val). +Context (even_dec_typed : ∀ n Γ, TY n; Γ ⊢ even_dec : (Int → Bool)). + +(* a) Change [even_impl] to [even_impl_instrumented] such that [toint] asserts evenness of the argument before returned. +You may use the [assert] expression defined in existential_invariants.v. +*) + +Definition even_impl_instrumented : val :=#0. (* TODO: your definition *) + +(* b) Prove that [even_impl_instrumented] is safe. You may assume that even works as intended, + but be sure to state this here. *) + + +Lemma even_impl_instrumented_safe δ: + 𝒱 even_type δ even_impl_instrumented. +Proof. + (* TODO: exercise *) +Admitted. + +End ex4. + +(** ** Exercise 5 (LN Exercise 31): Abstract sums *) +Section ex5. +Import logrel existential_invariants. +Definition sum_ex_type (A B : type) : type := + ∃: ((A.[ren (+1)] → #0) × + (B.[ren (+1)] → #0) × + (∀: #1 → (A.[ren (+2)] → #0) → (B.[ren (+2)] → #0) → #0) + )%ty. + +Definition sum_ex_impl : val := + pack (λ: "x", (#1, "x"), + λ: "x", (#2, "x"), + Λ, λ: "x" "f1" "f2", if: Fst "x" = #1 then "f1" (Snd "x") else "f2" (Snd "x") + ). + +Lemma sum_ex_safe A B δ: + 𝒱 (sum_ex_type A B) δ sum_ex_impl. +Proof. + (* TODO: exercise *) +Admitted. + +End ex5. + +(** For Exercise 6 and 7, see binary_logrel.v *) + +(** ** Exercise 8 (LN Exercise 35): Contextual equivalence *) +Section ex8. +Import binary_logrel. +Definition sum_ex_impl' : val := + pack ((λ: "x", InjL "x"), + (λ: "x", InjR "x"), + (Λ, λ: "x" "f1" "f2", Case "x" "f1" "f2") + ). + +Lemma sum_ex_impl'_typed n Γ A B : + type_wf n A → + type_wf n B → + TY n; Γ ⊢ sum_ex_impl' : sum_ex_type A B. +Proof. + intros. + eapply (typed_pack _ _ _ (A + B)%ty). + all: asimpl; solve_typing. +Qed. + +Lemma sum_ex_impl_equiv n Γ A B : + ctx_equiv n Γ sum_ex_impl' sum_ex_impl (sum_ex_type A B). +Proof. + (* TODO: exercise *) +Admitted. + + +End ex8. diff --git a/theories/type_systems/systemf/existential_invariants.v b/theories/type_systems/systemf/existential_invariants.v new file mode 100644 index 0000000..235bb51 --- /dev/null +++ b/theories/type_systems/systemf/existential_invariants.v @@ -0,0 +1,140 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.lib Require Export debruijn. +From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep tactics. +From semantics.ts.systemf Require logrel binary_logrel. +From Equations Require Import Equations. + +(** * Existential types and invariants *) +Implicit Types + (Δ : nat) + (Γ : typing_context) + (v : val) + (α : var) + (e : expr) + (A : type). + +(** Here, we take the approach of encoding [assert], + instead of adding it as a primitive to the language. + This saves us from adding it to all of the existing proofs. + But clearly it has the same reduction behavior. + *) + +Definition assert (e : expr) : expr := + if: e then #LitUnit else (#0 #0). +Lemma assert_true : rtc contextual_step (assert #true) #(). +Proof. + econstructor. + { eapply base_contextual_step. constructor. } + constructor. +Qed. +Lemma assert_false : rtc contextual_step (assert #false) (#0 #0). +Proof. + econstructor. { eapply base_contextual_step. econstructor. } + constructor. +Qed. + +Definition Or (e1 e2 : expr) : expr := + if: e1 then #true else e2. +Definition And (e1 e2 : expr) : expr := + if: e1 then e2 else #false. +Notation "e1 '||' e2" := (Or e1 e2) : expr_scope. +Notation "e1 '&&' e2" := (And e1 e2) : expr_scope. + +(** *** BIT *) +(* ∃ α, { bit : α, flip : α → α, get : α → bool } *) +Definition BIT : type := ∃: (#0 × (#0 → #0)) × (#0 → Bool). + +Definition MyBit : val := + pack (#0, (* bit *) + λ: "x", #1 - "x", (* flip *) + λ: "x", #0 < "x"). (* get *) + +Lemma MyBit_typed n Γ : + TY n; Γ ⊢ MyBit : BIT. +Proof. eapply (typed_pack _ _ _ Int); solve_typing. Qed. + +Definition MyBit_instrumented : val := + pack (#0, (* bit *) + λ: "x", assert (("x" = #0) || ("x" = #1));; #1 - "x", (* flip *) + λ: "x", assert (("x" = #0) || ("x" = #1));; #0 < "x"). (* get *) + +Definition MyBoolBit : val := + pack (#false, (* bit *) + λ: "x", UnOp NegOp "x", (* flip *) + λ: "x", "x"). (* get *) + +Lemma MyBoolBit_typed n Γ : + TY n; Γ ⊢ MyBoolBit : BIT. +Proof. + eapply (typed_pack _ _ _ Bool); solve_typing. + simpl. econstructor. +Qed. + + + +Section unary_mybit. + Import logrel. + + Lemma MyBit_instrumented_sem_typed δ : + 𝒱 BIT δ MyBit_instrumented. + Proof. + unfold BIT. simp type_interp. + eexists. split; first done. + pose_sem_type (λ x, x = #0 ∨ x = #1) as τ. + { intros v [-> | ->]; done. } + exists τ. + simp type_interp. + eexists _, _. split; first done. + split. + - simp type_interp. eexists _, _. split; first done. split. + + simp type_interp. simpl. by left. + + simp type_interp. eexists _, _. split; first done. split; first done. + intros v'. simp type_interp; simpl. + (* Note: this part of the proof is a bit different from the paper version, as we directly do a case split. *) + intros [-> | ->]. + * exists #1. split; last simp type_interp; simpl; eauto. + bs_steps_det. eapply bs_if_true; bs_steps_det. + eapply bs_if_true; bs_steps_det. + * exists #0. split; last simp type_interp; simpl; eauto. + bs_steps_det. eapply bs_if_true; bs_steps_det. + eapply bs_if_false; bs_steps_det. + - simp type_interp. eexists _, _. split; first done. split; first done. + intros v'. simp type_interp; simpl. intros [-> | ->]. + * exists #false. split; last simp type_interp; simpl; eauto. + bs_steps_det. eapply bs_if_true; bs_steps_det. eapply bs_if_true; bs_steps_det. + * exists #true. split; last simp type_interp; simpl; eauto. + bs_steps_det. eapply bs_if_true; bs_steps_det. eapply bs_if_false; bs_steps_det. + Qed. + +End unary_mybit. + + +Section binary_mybit. + Import binary_logrel. + + Lemma MyBit_MyBoolBit_sem_typed δ : + 𝒱 BIT δ MyBit MyBoolBit. + Proof. + unfold BIT. simp type_interp. + eexists _, _. split_and!; try done. + pose_sem_type (λ v w, (v = #0 ∧ w = #false) ∨ (v = #1 ∧ w = #true)) as τ. + { intros v w [[-> ->] | [-> ->]]; done. } + exists τ. + simp type_interp. + eexists _, _, _, _. split_and!; try done. + simp type_interp. + eexists _, _, _, _. split_and!; try done. + - simp type_interp. simpl. naive_solver. + - simp type_interp. eexists _, _, _, _. split_and!; try done. + intros v w. simp type_interp. simpl. + intros [[-> ->]|[-> ->]]; simpl; eexists _, _; split_and!; eauto; simpl. + all: simp type_interp; simpl; naive_solver. + - simp type_interp. eexists _, _, _, _. split_and!; try done. + intros v w. simp type_interp. simpl. + intros [[-> ->]|[-> ->]]; simpl. + all: eexists _, _; split_and!; eauto; simpl. + all: simp type_interp; eauto. + Qed. + +End binary_mybit. diff --git a/theories/type_systems/systemf/logrel_sol.v b/theories/type_systems/systemf/logrel_sol.v new file mode 100644 index 0000000..1d21bbc --- /dev/null +++ b/theories/type_systems/systemf/logrel_sol.v @@ -0,0 +1,763 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.lib Require Export facts. +From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep. +From Equations Require Export Equations. + + +(** * Logical relation for SystemF *) + +Implicit Types + (Δ : nat) + (Γ : typing_context) + (v : val) + (α : var) + (e : expr) + (A : type). + +(* *** Definition of the logical relation. *) +(* In Coq, we need to make argument why the logical relation is well-defined + precise: + In particular, we need to show that the mutual recursion between the value + relation and the expression relation, which are defined in terms of each + other, terminates. We therefore define a termination measure [mut_measure] + that makes sure that for each recursive call, we either decrease the size of + the type or switch from the expression case to the value case. + + We use the Equations package to define the logical relation, as it's tedious + to make the termination argument work with Coq's built-in support for + recursive functions---but under the hood, Equations also just encodes it as + a Coq Fixpoint. + *) +Inductive val_or_expr : Type := +| inj_val : val → val_or_expr +| inj_expr : expr → val_or_expr. + +(* The [type_size] function essentially computes the size of the "type tree". *) +(* Note that we have added some additional primitives to make our (still + simple) language more expressive. *) +Equations type_size (A : type) : nat := + type_size Int := 1; + type_size Bool := 1; + type_size Unit := 1; + type_size (A → B) := type_size A + type_size B + 1; + type_size (#α) := 1; + type_size (∀: A) := type_size A + 2; + type_size (∃: A) := type_size A + 2; + type_size (A × B) := type_size A + type_size B + 1; + type_size (A + B) := max (type_size A) (type_size B) + 1. +(* The definition of the expression relation uses the value relation -- therefore, it needs to be larger, and we add [1]. *) +Equations mut_measure (ve : val_or_expr) (t : type) : nat := + mut_measure (inj_val _) t := type_size t; + mut_measure (inj_expr _) t := 1 + type_size t. + +(** A semantic type consists of a value-predicate and a proof of closedness *) +Record sem_type := mk_ST { + sem_type_car :> val → Prop; + sem_type_closed_val v : sem_type_car v → is_closed [] (of_val v); + }. +(** Two tactics we will use later on. + [pose_sem_type P as N] defines a semantic type at name [N] with the value predicate [P]. + [specialize_sem_type S with P as N] specializes a universal quantifier over sem types in [S] with + a semantic type with predicate [P], giving it the name [N]. + *) +(* slightly complicated formulation to make the proof term [p] opaque and prevent it from polluting the context *) +Tactic Notation "pose_sem_type" uconstr(P) "as" ident(N) := + let p := fresh "__p" in + unshelve refine ((λ p, let N := (mk_ST P p) in _) _); first (simpl in p); cycle 1. +Tactic Notation "specialize_sem_type" constr(S) "with" uconstr(P) "as" ident(N) := + pose_sem_type P as N; last specialize (S N). + +(** We represent type variable assignments [δ] as lists of semantic types. + The variable #n (in De Bruijn representation) is mapped to the [n]-th element of the list. + *) +Definition tyvar_interp := nat → sem_type. +Implicit Types + (δ : tyvar_interp) + (τ : sem_type). + +(** The logical relation *) +Equations type_interp (c : val_or_expr) (t : type) δ : Prop by wf (mut_measure c t) := { + type_interp (inj_val v) Int δ => + ∃ z : Z, v = #z ; + type_interp (inj_val v) Bool δ => + ∃ b : bool, v = #b ; + type_interp (inj_val v) Unit δ => + v = #LitUnit ; + type_interp (inj_val v) (A × B) δ => + ∃ v1 v2 : val, v = (v1, v2)%V ∧ type_interp (inj_val v1) A δ ∧ type_interp (inj_val v2) B δ; + type_interp (inj_val v) (A + B) δ => + (∃ v' : val, v = InjLV v' ∧ type_interp (inj_val v') A δ) ∨ + (∃ v' : val, v = InjRV v' ∧ type_interp (inj_val v') B δ); + type_interp (inj_val v) (A → B) δ => + ∃ x e, v = LamV x e ∧ is_closed (x :b: nil) e ∧ + ∀ v', + type_interp (inj_val v') A δ → + type_interp (inj_expr (subst' x (of_val v') e)) B δ; + (** Type variable case *) + type_interp (inj_val v) (#α) δ => + (δ α).(sem_type_car) v; + (** ∀ case *) + type_interp (inj_val v) (∀: A) δ => + ∃ e, v = TLamV e ∧ is_closed [] e ∧ + ∀ τ, type_interp (inj_expr e) A (τ .: δ); + (** ∃ case *) + type_interp (inj_val v) (∃: A) δ => + ∃ v', v = PackV v' ∧ + ∃ τ : sem_type, type_interp (inj_val v') A (τ .: δ); + + type_interp (inj_expr e) t δ => + ∃ v, big_step e v ∧ type_interp (inj_val v) t δ +}. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. + simp mut_measure. simp type_size. + destruct A; repeat simp mut_measure; repeat simp type_size; lia. +Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. + +(** Value relation and expression relation *) +Notation sem_val_rel A δ v := (type_interp (inj_val v) A δ). +Notation sem_expr_rel A δ e := (type_interp (inj_expr e) A δ). + +Notation 𝒱 A δ v := (sem_val_rel A δ v). +Notation ℰ A δ v := (sem_expr_rel A δ v). + + +(* *** Semantic typing of contexts *) +Implicit Types + (θ : gmap string expr). +Inductive sem_context_rel (δ : tyvar_interp) : typing_context → (gmap string expr) → Prop := + | sem_context_rel_empty : sem_context_rel δ ∅ ∅ + | sem_context_rel_insert Γ θ v x A : + 𝒱 A δ v → + sem_context_rel δ Γ θ → + sem_context_rel δ (<[x := A]> Γ) (<[x := of_val v]> θ). + +Notation 𝒢 := sem_context_rel. + + + +(* Semantic typing judgement *) +Definition sem_typed Δ Γ e A := + is_closed (elements (dom Γ)) e ∧ + ∀ θ δ, 𝒢 δ Γ θ → ℰ A δ (subst_map θ e). +Notation "'TY' Δ ; Γ ⊨ e : A" := (sem_typed Δ Γ e A) (at level 74, e, A at next level). + + +Lemma val_rel_closed v δ A: + 𝒱 A δ v → is_closed [] (of_val v). +Proof. + induction A as [ | | | | | A IHA | | A IH1 B IH2 | A IH1 B IH2] in v, δ |-*; simp type_interp. + - eapply sem_type_closed_val. + - intros [z ->]. done. + - intros [b ->]. done. + - intros ->. done. + - intros (e & -> & ? & _). done. + - intros (v' & -> & (τ & Hinterp)). simpl. by eapply IHA. + - intros (x & e & -> & ? & _). done. + - intros (v1 & v2 & -> & ? & ?). simpl. apply andb_True. eauto. + - intros [(v' & -> & ?) | (v' & -> & ?)]; simpl; eauto. +Qed. + +(** Interpret a syntactic type *) +Program Definition interp_type A δ : sem_type := {| + sem_type_car := fun v => 𝒱 A δ v; +|}. +Next Obligation. by eapply val_rel_closed. Qed. + + +(* We start by proving a couple of helper lemmas that will be useful later. *) + +Lemma sem_expr_rel_of_val A δ v : + ℰ A δ (of_val v) → 𝒱 A δ v. +Proof. + simp type_interp. + intros (v' & ->%big_step_val & Hv'). + apply Hv'. +Qed. +Lemma val_inclusion A δ v: + 𝒱 A δ v → ℰ A δ v. +Proof. + intros H. simp type_interp. eauto using big_step_of_val. +Qed. + + +Lemma sem_context_rel_closed δ Γ θ: + 𝒢 δ Γ θ → subst_is_closed [] θ. +Proof. + induction 1. + - done. + - intros y e. rewrite lookup_insert_Some. + intros [[-> <-]|[Hne Hlook]]. + + by eapply val_rel_closed. + + eapply IHsem_context_rel; last done. +Qed. + + +(* This is essentially an inversion lemma for 𝒢 *) +Lemma sem_context_rel_vals δ Γ θ x A : + 𝒢 δ Γ θ → + Γ !! x = Some A → + ∃ e v, θ !! x = Some e ∧ to_val e = Some v ∧ 𝒱 A δ v. +Proof. + induction 1 as [|Γ θ v y B Hvals Hctx IH]. + - naive_solver. + - rewrite lookup_insert_Some. intros [[-> ->]|[Hne Hlook]]. + + do 2 eexists. split; first by rewrite lookup_insert. + split; first by eapply to_of_val. done. + + eapply IH in Hlook as (e & w & Hlook & He & Hval). + do 2 eexists; split; first by rewrite lookup_insert_ne. + split; first done. done. +Qed. + +Lemma sem_context_rel_dom δ Γ θ : + 𝒢 δ Γ θ → dom Γ = dom θ. +Proof. + induction 1. + - by rewrite !dom_empty. + - rewrite !dom_insert. congruence. +Qed. + + +Section boring_lemmas. + (** The lemmas in this section are all quite boring and expected statements, + but are quite technical to prove due to De Bruijn binders. + We encourage you to skip over the proofs of these lemmas. + *) + + Lemma sem_val_rel_ext B δ δ' v : + (∀ n v, δ n v ↔ δ' n v) → + 𝒱 B δ v ↔ 𝒱 B δ' v. + Proof. + induction B in δ, δ', v |-*; simpl; simp type_interp; eauto; intros Hiff. + - f_equiv; intros e. f_equiv. f_equiv. + eapply forall_proper; intros τ. + simp type_interp. f_equiv. intros w. + f_equiv. etransitivity; last apply IHB; first done. + intros [|m] ?; simpl; eauto. + - f_equiv; intros w. f_equiv. f_equiv. intros τ. + etransitivity; last apply IHB; first done. + intros [|m] ?; simpl; eauto. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv. eapply forall_proper. intros x. + eapply if_iff; first eauto. + simp type_interp. f_equiv. intros ?. f_equiv. + eauto. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv; eauto. + - f_equiv; f_equiv; intros ?; f_equiv; eauto. + Qed. + + + Lemma sem_val_rel_move_ren B δ σ v : + 𝒱 B (λ n, δ (σ n)) v ↔ 𝒱 (rename σ B) δ v. + Proof. + induction B in σ, δ, v |-*; simpl; simp type_interp; eauto. + - f_equiv; intros e. f_equiv. f_equiv. + eapply forall_proper; intros τ. + simp type_interp. f_equiv. intros w. + f_equiv. etransitivity; last apply IHB. + eapply sem_val_rel_ext; intros [|n] u; asimpl; done. + - f_equiv; intros w. f_equiv. f_equiv. intros τ. + etransitivity; last apply IHB. + eapply sem_val_rel_ext; intros [|n] u. + + simp type_interp. done. + + simpl. rewrite /up. simpl. done. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv. eapply forall_proper. intros x. + eapply if_iff; first done. + simp type_interp. f_equiv. intros ?. f_equiv. + done. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv; done. + - f_equiv; f_equiv; intros ?; f_equiv; done. + Qed. + + + Lemma sem_val_rel_move_subst B δ σ v : + 𝒱 B (λ n, interp_type (σ n) δ) v ↔ 𝒱 (B.[σ]) δ v. + Proof. + induction B in σ, δ, v |-*; simpl; simp type_interp; eauto. + - f_equiv; intros e. f_equiv. f_equiv. + eapply forall_proper; intros τ. + simp type_interp. f_equiv. intros w. + f_equiv. etransitivity; last apply IHB. + eapply sem_val_rel_ext; intros [|n] u. + + simp type_interp. done. + + simpl. rewrite /up. simpl. + etransitivity; last eapply sem_val_rel_move_ren. + simpl. done. + - f_equiv; intros w. f_equiv. f_equiv. intros τ. + etransitivity; last apply IHB. + eapply sem_val_rel_ext; intros [|n] u. + + simp type_interp. done. + + simpl. rewrite /up. simpl. + etransitivity; last eapply sem_val_rel_move_ren. + simpl. done. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv. eapply forall_proper. intros x. + eapply if_iff; first done. + simp type_interp. f_equiv. intros ?. f_equiv. + done. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv; done. + - f_equiv; f_equiv; intros ?; f_equiv; done. + Qed. + + Lemma sem_val_rel_move_single_subst A B δ v : + 𝒱 B (interp_type A δ .: δ) v ↔ 𝒱 (B.[A/]) δ v. + Proof. + rewrite -sem_val_rel_move_subst. eapply sem_val_rel_ext. + intros [| n] w; simpl; done. + Qed. + + Lemma sem_val_rel_cons A δ v τ : + 𝒱 A δ v ↔ 𝒱 A.[ren (+1)] (τ .: δ) v. + Proof. + rewrite -sem_val_rel_move_subst; simpl. + eapply sem_val_rel_ext; done. + Qed. + + Lemma sem_context_rel_cons Γ δ θ τ : + 𝒢 δ Γ θ → + 𝒢 (τ .: δ) (⤉ Γ) θ. + Proof. + induction 1 as [ | Γ θ v x A Hv Hctx IH]; simpl. + - rewrite fmap_empty. constructor. + - rewrite fmap_insert. constructor; last done. + rewrite -sem_val_rel_cons. done. + Qed. +End boring_lemmas. + +(** ** Compatibility lemmas *) + +Lemma compat_int Δ Γ z : TY Δ; Γ ⊨ (Lit $ LitInt z) : Int. +Proof. + split; first done. + intros θ δ _. simp type_interp. + exists #z. split. { simpl. constructor. } + simp type_interp. eauto. +Qed. + +Lemma compat_bool Δ Γ b : TY Δ; Γ ⊨ (Lit $ LitBool b) : Bool. +Proof. + split; first done. + intros θ δ _. simp type_interp. + exists #b. split. { simpl. constructor. } + simp type_interp. eauto. +Qed. + +Lemma compat_unit Δ Γ : TY Δ; Γ ⊨ (Lit $ LitUnit) : Unit. +Proof. + split; first done. + intros θ δ _. simp type_interp. + exists #LitUnit. split. { simpl. constructor. } + simp type_interp. eauto. +Qed. + +Lemma compat_var Δ Γ x A : + Γ !! x = Some A → + TY Δ; Γ ⊨ (Var x) : A. +Proof. + intros Hx. split. + { eapply bool_decide_pack, elem_of_elements, elem_of_dom_2, Hx. } + intros θ δ Hctx; simpl. + eapply sem_context_rel_vals in Hx as (e & v & He & Heq & Hv); last done. + rewrite He. simp type_interp. exists v. split; last done. + rewrite -(of_to_val _ _ Heq). + by apply big_step_of_val. +Qed. + +Lemma compat_app Δ Γ e1 e2 A B : + TY Δ; Γ ⊨ e1 : (A → B) → + TY Δ; Γ ⊨ e2 : A → + TY Δ; Γ ⊨ (e1 e2) : B. +Proof. + intros [Hfuncl Hfun] [Hargcl Harg]. split. + { simpl. eauto. } + intros θ δ Hctx; simpl. + + specialize (Hfun _ _ Hctx). simp type_interp in Hfun. destruct Hfun as (v1 & Hbs1 & Hv1). + simp type_interp in Hv1. destruct Hv1 as (x & e & -> & Hv1). + specialize (Harg _ _ Hctx). simp type_interp in Harg. + destruct Harg as (v2 & Hbs2 & Hv2). + + apply Hv1 in Hv2. + simp type_interp in Hv2. destruct Hv2 as (v & Hbsv & Hv). + + simp type_interp. + exists v. split; last done. + eauto. +Qed. + +(* Compatibility for [lam] unfortunately needs a very technical helper lemma. *) +Lemma lam_closed δ Γ θ (x : string) A e : + closed (elements (dom (<[x:=A]> Γ))) e → + 𝒢 δ Γ θ → + closed [] (Lam x (subst_map (delete x θ) e)). +Proof. + intros Hcl Hctxt. + eapply subst_map_closed. + - eapply is_closed_weaken; first done. + rewrite dom_delete dom_insert (sem_context_rel_dom δ Γ θ) //. + intros y. destruct (decide (x = y)); set_solver. + - intros x' e' Hx. + eapply (is_closed_weaken []); last set_solver. + eapply sem_context_rel_closed; first eassumption. + eapply map_subseteq_spec; last done. + apply map_delete_subseteq. +Qed. +Lemma compat_lam Δ Γ x e A B : + TY Δ; (<[ x := A ]> Γ) ⊨ e : B → + TY Δ; Γ ⊨ (Lam (BNamed x) e) : (A → B). +Proof. + intros [Hbodycl Hbody]. split. + { simpl. eapply is_closed_weaken; first eassumption. set_solver. } + intros θ Hctxt. simpl. simp type_interp. + eexists. + split; first by eauto. + simp type_interp. + eexists _, _. split; first reflexivity. + split; first by eapply lam_closed. + intros v' Hv'. + specialize (Hbody (<[ x := of_val v']> θ)). + simpl. rewrite subst_subst_map; last by eapply sem_context_rel_closed. + apply Hbody. + apply sem_context_rel_insert; done. +Qed. + +Lemma compat_lam_anon Δ Γ e A B : + TY Δ; Γ ⊨ e : B → + TY Δ; Γ ⊨ (Lam BAnon e) : (A → B). +Proof. + intros [Hbodycl Hbody]. split; first done. + intros θ Hctxt. simpl. simp type_interp. + eexists. + split; first by eauto. + simp type_interp. + eexists _, _. split; first reflexivity. + split. + { simpl. eapply subst_map_closed; simpl. + - by erewrite <-sem_context_rel_dom. + - by eapply sem_context_rel_closed. } + naive_solver. +Qed. + +Lemma compat_int_binop Δ Γ op e1 e2 : + bin_op_typed op Int Int Int → + TY Δ; Γ ⊨ e1 : Int → + TY Δ; Γ ⊨ e2 : Int → + TY Δ; Γ ⊨ (BinOp op e1 e2) : Int. +Proof. + intros Hop [He1cl He1] [He2cl He2]. + split; first naive_solver. + + intros θ δ Hctx. simpl. + simp type_interp. + specialize (He1 _ _ Hctx). specialize (He2 _ _ Hctx). + simp type_interp in He1. simp type_interp in He2. + + destruct He1 as (v1 & Hb1 & Hv1). + destruct He2 as (v2 & Hb2 & Hv2). + simp type_interp in Hv1, Hv2. + destruct Hv1 as (z1 & ->). destruct Hv2 as (z2 & ->). + + inversion Hop; subst op. + + exists #(z1 + z2)%Z. split. + - econstructor; done. + - exists (z1 + z2)%Z. done. + + exists #(z1 - z2)%Z. split. + - econstructor; done. + - exists (z1 - z2)%Z. done. + + exists #(z1 * z2)%Z. split. + - econstructor; done. + - exists (z1 * z2)%Z. done. +Qed. + +Lemma compat_int_bool_binop Δ Γ op e1 e2 : + bin_op_typed op Int Int Bool → + TY Δ; Γ ⊨ e1 : Int → + TY Δ; Γ ⊨ e2 : Int → + TY Δ; Γ ⊨ (BinOp op e1 e2) : Bool. +Proof. + intros Hop [He1cl He1] [He2cl He2]. + split; first naive_solver. + + intros θ δ Hctx. simpl. + simp type_interp. + specialize (He1 _ _ Hctx). specialize (He2 _ _ Hctx). + simp type_interp in He1. simp type_interp in He2. + + destruct He1 as (v1 & Hb1 & Hv1). + destruct He2 as (v2 & Hb2 & Hv2). + simp type_interp in Hv1, Hv2. + destruct Hv1 as (z1 & ->). destruct Hv2 as (z2 & ->). + + inversion Hop; subst op. + + exists #(bool_decide (z1 < z2))%Z. split. + - econstructor; done. + - by eexists _. + + exists #(bool_decide (z1 ≤ z2))%Z. split. + - econstructor; done. + - by eexists _. + + exists #(bool_decide (z1 = z2))%Z. split. + - econstructor; done. + - eexists _. done. +Qed. + +Lemma compat_unop Δ Γ op A B e : + un_op_typed op A B → + TY Δ; Γ ⊨ e : A → + TY Δ; Γ ⊨ (UnOp op e) : B. +Proof. + intros Hop [Hecl He]. + split; first naive_solver. + intros θ δ Hctx. simpl. + simp type_interp. specialize (He _ _ Hctx). + simp type_interp in He. + + destruct He as (v & Hb & Hv). + inversion Hop; subst; simp type_interp in Hv. + - destruct Hv as (b & ->). + exists #(negb b). split. + + econstructor; done. + + by eexists _. + - destruct Hv as (z & ->). + exists #(-z)%Z. split. + + econstructor; done. + + by eexists _. +Qed. + +Lemma compat_tlam Δ Γ e A : + TY S Δ; (⤉ Γ) ⊨ e : A → + TY Δ; Γ ⊨ (Λ, e) : (∀: A). +Proof. + intros [Hecl He]. split. + { simpl. by erewrite <-dom_fmap. } + intros θ δ Hctx. simpl. + simp type_interp. + exists (Λ, subst_map θ e)%V. + split; first constructor. + + simp type_interp. + eexists _. split_and!; first done. + { simpl. eapply subst_map_closed; simpl. + - erewrite <-sem_context_rel_dom; last eassumption. + by erewrite <-dom_fmap. + - by eapply sem_context_rel_closed. } + intros τ. eapply He. + by eapply sem_context_rel_cons. +Qed. + +Lemma compat_tapp Δ Γ e A B : + type_wf Δ B → + TY Δ; Γ ⊨ e : (∀: A) → + TY Δ; Γ ⊨ (e <>) : (A.[B/]). +Proof. + intros Hwf [Hecl He]. + split; first naive_solver. + intros θ δ Hctx. simpl. + simp type_interp. + + specialize (He _ _ Hctx). simp type_interp in He. + destruct He as (v & Hb & Hv). + simp type_interp in Hv. + destruct Hv as (e1 & -> & Cl & He1). + + set (τ := interp_type B δ). + specialize (He1 τ). + simp type_interp in He1. destruct He1 as (v & Hb2 & Hv). + exists v. split. { econstructor; done. } + apply sem_val_rel_move_single_subst. done. +Qed. + +Lemma compat_pack Δ Γ e n A B : + type_wf n B → + type_wf (S n) A → + TY n; Γ ⊨ e : A.[B/] → + TY n; Γ ⊨ (pack e) : (∃: A). +Proof. +(* This will be an exercise for you next week :) *) +Admitted. + + +Lemma compat_unpack n Γ A B e e' x : +type_wf n B → +TY n; Γ ⊨ e : (∃: A) → +TY S n; <[x:=A]> (⤉Γ) ⊨ e' : B.[ren (+1)] → +TY n; Γ ⊨ (unpack e as BNamed x in e') : B. +Proof. +(* This will be an exercise for you next week :) *) +Admitted. + +Lemma compat_if n Γ e0 e1 e2 A : + TY n; Γ ⊨ e0 : Bool → + TY n; Γ ⊨ e1 : A → + TY n; Γ ⊨ e2 : A → + TY n; Γ ⊨ (if: e0 then e1 else e2) : A. +Proof. + intros [He0cl He0] [He1cl He1] [He2cl He2]. + split; first naive_solver. + intros θ δ Hctx. simpl. + simp type_interp. + specialize (He0 _ _ Hctx). simp type_interp in He0. + specialize (He1 _ _ Hctx). simp type_interp in He1. + specialize (He2 _ _ Hctx). simp type_interp in He2. + + destruct He0 as (v0 & Hb0 & Hv0). simp type_interp in Hv0. destruct Hv0 as (b & ->). + destruct He1 as (v1 & Hb1 & Hv1). + destruct He2 as (v2 & Hb2 & Hv2). + + destruct b. + - exists v1. split; first by repeat econstructor. done. + - exists v2. split; first by repeat econstructor. done. +Qed. + +Lemma compat_pair Δ Γ e1 e2 A B : + TY Δ; Γ ⊨ e1 : A → + TY Δ; Γ ⊨ e2 : B → + TY Δ; Γ ⊨ (e1, e2) : A × B. +Proof. + intros [He1cl He1] [He2cl He2]. + split; first naive_solver. + intros θ δ Hctx. simpl. + simp type_interp. + specialize (He1 _ _ Hctx). simp type_interp in He1. + destruct He1 as (v1 & Hb1 & Hv1). + specialize (He2 _ _ Hctx). simp type_interp in He2. + destruct He2 as (v2 & Hb2 & Hv2). + exists (v1, v2)%V. split; first eauto. + simp type_interp. exists v1, v2. done. +Qed. + +Lemma compat_fst Δ Γ e A B : + TY Δ; Γ ⊨ e : A × B → + TY Δ; Γ ⊨ Fst e : A. +Proof. + intros [Hecl He]. split; first naive_solver. + intros θ δ Hctx. simpl. + simp type_interp. + specialize (He _ _ Hctx). simp type_interp in He. + destruct He as (v & Hb & Hv). + simp type_interp in Hv. destruct Hv as (v1 & v2 & -> & Hv1 & Hv2). + exists v1. split; first eauto. done. +Qed. + +Lemma compat_snd Δ Γ e A B : + TY Δ; Γ ⊨ e : A × B → + TY Δ; Γ ⊨ Snd e : B. +Proof. + intros [Hecl He]. split; first naive_solver. + intros θ δ Hctx. simpl. + simp type_interp. + specialize (He _ _ Hctx). simp type_interp in He. + destruct He as (v & Hb & Hv). + simp type_interp in Hv. destruct Hv as (v1 & v2 & -> & Hv1 & Hv2). + exists v2. split; first eauto. done. +Qed. + +Lemma compat_injl Δ Γ e A B : + TY Δ; Γ ⊨ e : A → + TY Δ; Γ ⊨ InjL e : A + B. +Proof. + intros [Hecl He]. split; first naive_solver. + intros θ δ Hctx. simpl. + simp type_interp. + specialize (He _ _ Hctx). simp type_interp in He. + destruct He as (v & Hb & Hv). + exists (InjLV v). split; first eauto. + simp type_interp. eauto. +Qed. + +Lemma compat_injr Δ Γ e A B : + TY Δ; Γ ⊨ e : B → + TY Δ; Γ ⊨ InjR e : A + B. +Proof. + intros [Hecl He]. split; first naive_solver. + intros θ δ Hctx. simpl. + simp type_interp. + specialize (He _ _ Hctx). simp type_interp in He. + destruct He as (v & Hb & Hv). + exists (InjRV v). split; first eauto. + simp type_interp. eauto. +Qed. + +Lemma compat_case Δ Γ e e1 e2 A B C : + TY Δ; Γ ⊨ e : B + C → + TY Δ; Γ ⊨ e1 : (B → A) → + TY Δ; Γ ⊨ e2 : (C → A) → + TY Δ; Γ ⊨ Case e e1 e2 : A. +Proof. + intros [Hecl He] [He1cl He1] [He2cl He2]. + split; first naive_solver. + intros θ δ Hctx. simpl. + simp type_interp. + specialize (He _ _ Hctx). simp type_interp in He. + destruct He as (v & Hb & Hv). + simp type_interp in Hv. destruct Hv as [(v' & -> & Hv') | (v' & -> & Hv')]. + - specialize (He1 _ _ Hctx). simp type_interp in He1. + destruct He1 as (v & Hb' & Hv). + simp type_interp in Hv. destruct Hv as (x & e' & -> & Cl & Hv). + apply Hv in Hv'. simp type_interp in Hv'. destruct Hv' as (v & Hb'' & Hv''). + exists v. split; last done. + econstructor; first done. + econstructor; [done | apply big_step_of_val; done | done]. + - specialize (He2 _ _ Hctx). simp type_interp in He2. + destruct He2 as (v & Hb' & Hv). + simp type_interp in Hv. destruct Hv as (x & e' & -> & Cl & Hv). + apply Hv in Hv'. simp type_interp in Hv'. destruct Hv' as (v & Hb'' & Hv''). + exists v. split; last done. + econstructor; first done. + econstructor; [done | apply big_step_of_val; done | done]. +Qed. + +Lemma sem_soundness Δ Γ e A : + TY Δ; Γ ⊢ e : A → + TY Δ; Γ ⊨ e : A. +Proof. + induction 1 as [ | | | | | | | | | | | | n Γ e1 e2 op A B C Hop ? ? ? ? | | | | | | | ]. + - by apply compat_var. + - by apply compat_lam. + - by apply compat_lam_anon. + - by apply compat_tlam. + - apply compat_tapp; done. + - eapply compat_pack; done. + - eapply compat_unpack; done. + - apply compat_int. + - by eapply compat_bool. + - by eapply compat_unit. + - by eapply compat_if. + - by eapply compat_app. + - inversion Hop; subst. + 1-3: by apply compat_int_binop. + 1-3: by apply compat_int_bool_binop. + - by eapply compat_unop. + - by apply compat_pair. + - by eapply compat_fst. + - by eapply compat_snd. + - by eapply compat_injl. + - by eapply compat_injr. + - by eapply compat_case. +Qed. + +(* dummy delta which we can use if we don't care *) +Program Definition any_type : sem_type := {| sem_type_car := λ v, is_closed [] v |}. +Definition δ_any : var → sem_type := λ _, any_type. + +Lemma termination e A : + (TY 0; ∅ ⊢ e : A)%ty → + ∃ v, big_step e v. +Proof. + intros [Hsemcl Hsem]%sem_soundness. + specialize (Hsem ∅ δ_any). + simp type_interp in Hsem. + rewrite subst_map_empty in Hsem. + destruct Hsem as (v & Hbs & _); last eauto. + constructor. +Qed. diff --git a/theories/type_systems/systemf/types.v b/theories/type_systems/systemf/types.v index d6ffb7e..a8c46fd 100644 --- a/theories/type_systems/systemf/types.v +++ b/theories/type_systems/systemf/types.v @@ -613,10 +613,10 @@ Proof. eexists. eapply base_contextual_step. eapply TBetaS. + destruct H1 as [e' H1]. eexists. eauto. - (* pack *) - (* FIXME this will be an exercise for you soon :) *) + (* TODO this will be an exercise for you soon :) *) admit. - (* unpack *) - (* FIXME this will be an exercise for you soon :) *) + (* TODO this will be an exercise for you soon :) *) admit. - (* int *)left. done. - (* bool*) left. done. @@ -804,7 +804,7 @@ Proof. eapply type_lam_inversion in Hty as (A & Heq & Hty). injection Heq as ->. by eapply typed_subst_type_closed. - (* unpack *) - (* FIXME: this will be an exercise for you soon :) *) + (* TODO: this will be an exercise for you soon :) *) admit. - (* unop *) eapply unop_inversion in Hty as (A1 & Hop & Hty).