From b967e73f061e885da14b06f198d6b5257429067a Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Tue, 14 Nov 2023 22:30:15 +0100 Subject: [PATCH] Catch up on stlc_extended --- theories/type_systems/stlc_extended/bigstep.v | 2 +- theories/type_systems/stlc_extended/ctxstep.v | 24 +-- theories/type_systems/stlc_extended/logrel.v | 156 +++++++++++++-- theories/type_systems/stlc_extended/types.v | 187 +++++++++++++++--- 4 files changed, 318 insertions(+), 51 deletions(-) diff --git a/theories/type_systems/stlc_extended/bigstep.v b/theories/type_systems/stlc_extended/bigstep.v index 61c940d..7158e8a 100644 --- a/theories/type_systems/stlc_extended/bigstep.v +++ b/theories/type_systems/stlc_extended/bigstep.v @@ -32,7 +32,7 @@ Inductive big_step : expr → val → Prop := big_step (Fst e) v1 | bs_snd (e : expr) (v1 v2: val): big_step e (PairV v1 v2) → - big_step (Fst e) v1 + big_step (Snd e) v2 (* Inj *) | bs_inj_l e v : big_step e v → diff --git a/theories/type_systems/stlc_extended/ctxstep.v b/theories/type_systems/stlc_extended/ctxstep.v index d3761d9..fa360e3 100644 --- a/theories/type_systems/stlc_extended/ctxstep.v +++ b/theories/type_systems/stlc_extended/ctxstep.v @@ -12,24 +12,20 @@ Inductive base_step : expr → expr → Prop := e2 = (LitInt n2) → (n1 + n2)%Z = n3 → base_step (Plus e1 e2) (LitInt n3) - | FstS e v1 v2: + | FstS v1 v2: is_val v1 → is_val v2 → - e = (Pair v1 v2) → - base_step (Fst e) v1 - | SndS e v1 v2: + base_step (Fst (Pair v1 v2)) v1 + | SndS v1 v2: is_val v1 → is_val v2 → - e = (Pair v1 v2) → - base_step (Snd e) v2 - | CaseLS v_inj v e1 e2: - is_val v_inj → - v_inj = (InjL v) → - base_step (Case v_inj e1 e2) (App e1 v) - | CaseRS v_inj v e1 e2: - is_val v_inj → - v_inj = (InjR v) → - base_step (Case v_inj e1 e2) (App e2 v) + base_step (Snd (Pair v1 v2)) v2 + | CaseLS v e1 e2: + is_val v → + base_step (Case (InjL v) e1 e2) (App e1 v) + | CaseRS v e1 e2: + is_val v → + base_step (Case (InjR v) e1 e2) (App e2 v) . #[export] Hint Constructors base_step : core. diff --git a/theories/type_systems/stlc_extended/logrel.v b/theories/type_systems/stlc_extended/logrel.v index 7a3b32e..a621952 100644 --- a/theories/type_systems/stlc_extended/logrel.v +++ b/theories/type_systems/stlc_extended/logrel.v @@ -35,11 +35,14 @@ Equations type_interp (ve : val_or_expr) (t : type) : Prop by wf (mut_measure ve type_interp (inj_val v) Int => ∃ z : Z, v = #z ; type_interp (inj_val v) (A × B) => - (* TODO: add type interpretation *) - False; + ∃ v₁ v₂, + v = @PairV v₁ v₂ + ∧ type_interp (inj_val v₁) A + ∧ type_interp (inj_val v₂) B + ; type_interp (inj_val v) (A + B) => - (* TODO: add type interpretation *) - False; + (∃ v₁, v = @InjLV v₁ ∧ type_interp (inj_val v₁) A) + ∨ (∃ v₂, v = @InjRV v₂ ∧ type_interp (inj_val v₂) B); type_interp (inj_val v) (A → B) => ∃ x e, v = @LamV x e ∧ closed (x :b: nil) e ∧ ∀ v', @@ -58,12 +61,11 @@ Next Obligation. Qed. (* Uncomment the following once you have amended the type interpretation to solve the new obligations: *) -(* + 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. -*) Notation sem_val_rel t v := (type_interp (inj_val v) t). @@ -115,8 +117,18 @@ Proof. induction A in v |-*; simp type_interp. - intros [z ->]. done. - intros (x & e & -> & Hcl & _). done. - (* TODO: exercise *) -Admitted. + - intros (v1 & v2 & -> & Hv1 & Hv2). + unfold closed. + simpl. + apply andb_True. + split. + by apply (IHA1 _ Hv1). + by apply (IHA2 _ Hv2). + - intro H. + case H; intros (v' & -> & Hv'). + + exact (IHA1 _ Hv'). + + exact (IHA2 _ Hv'). +Qed. Lemma sem_context_rel_closed Γ θ: 𝒢 Γ θ → subst_closed [] θ. @@ -202,8 +214,8 @@ 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 (elements (dom (<[x:=A]> Γ))) e → + 𝒢 Γ θ → closed [] (Lam x (subst_map (delete x θ) e)). Proof. intros Hcl Hctxt. @@ -234,6 +246,7 @@ Proof. apply Hbody. apply sem_context_rel_insert; done. Qed. + Lemma compat_lam_anon Γ e A B : Γ ⊨ e : B → Γ ⊨ (Lam BAnon e) : (A → B). @@ -274,8 +287,119 @@ Proof. Qed. +Lemma compat_pair Γ e_lhs e_rhs A B: + Γ ⊨ e_lhs: A → + Γ ⊨ e_rhs: B → + Γ ⊨ (e_lhs, e_rhs): A × B. +Proof. + intros [Hcl_lhs He_lhs]. + intros [Hcl_rhs He_rhs]. + split. + (* The closedness can be handled by naive_solver *) + { + unfold closed. + naive_solver. + } + + (* Use the same θ and H_ctx everywhere: *) + intros θ H_ctx. + specialize (He_lhs _ H_ctx). + specialize (He_rhs _ H_ctx). + (* Apply the definition of E[A × B] and E[A], E[B] *) + simp type_interp in *. + destruct He_lhs as (v_lhs & Hbs_lhs & Hv_lhs). + destruct He_rhs as (v_rhs & Hbs_rhs & Hv_rhs). + + (* We now just need to provide a value satisfying our requirements *) + exists (PairV v_lhs v_rhs). + split. + - (* Prove that our expression steps towards the value *) + simpl. + econstructor. + assumption. + assumption. + - (* Next prove that our value is a correct member of V[A × B] *) + simp type_interp. (* Can't just split here :> *) + eauto. (* Trivial from then on *) +Qed. +Lemma compat_fst_snd {Γ e_pair A B}: + Γ ⊨ e_pair: A × B → + Γ ⊨ (Fst e_pair): A ∧ Γ ⊨ (Snd e_pair): B. +Proof. + intros [Hcl He]. + split. + all: split; first (unfold closed; naive_solver). + all: intros θ H_ctx; specialize (He _ H_ctx). + all: simp type_interp in *; destruct He as (v & Hbs & Hv). + all: simp type_interp in Hv; destruct Hv as (v₁ & v₂ & -> & Hv₁ & Hv₂). + 1: exists v₁. + 2: exists v₂. + (* Solve the big_step *) + all: simpl; split; first (econstructor; eauto). + all: assumption. +Qed. +Lemma compat_inj {Γ e_inj} A B: + Γ ⊨ e_inj: A → + Γ ⊨ (InjL e_inj): A + B ∧ Γ ⊨ (InjR e_inj): B + A. +Proof. + intros [Hcl He]. + split. + all: split; first (unfold closed; naive_solver). + all: intros θ H_ctx; specialize (He _ H_ctx). + all: simp type_interp in *; destruct He as (v & Hbs & Hv). + 1: exists (InjLV v). + 2: exists (InjRV v). + + all: simpl; split; first (econstructor; eauto). + - simp type_interp; left; eauto. + - simp type_interp; right; eauto. +Qed. + +Lemma compat_case {Γ e_inj e_lhs e_rhs A B C}: + Γ ⊨ e_inj: A + B → + Γ ⊨ e_lhs: (A → C) → + Γ ⊨ e_rhs: (B → C) → + Γ ⊨ (Case e_inj e_lhs e_rhs): C. +Proof. + intros [Hcl_inj He_inj] [Hcl_lhs He_lhs] [Hcl_rhs He_rhs]. + split; first (unfold closed; naive_solver). + + intros θ H_ctx; + specialize (He_inj _ H_ctx); + specialize (He_lhs _ H_ctx); + specialize (He_rhs _ H_ctx). + + (* All the hypotheses! *) + simp type_interp in *; + destruct He_inj as (v_inj & Hbs_inj & Hv_inj); + destruct He_lhs as (v_lhs & Hbs_lhs & Hv_lhs); + destruct He_rhs as (v_rhs & Hbs_rhs & Hv_rhs). + simp type_interp in *; + destruct Hv_lhs as (x_lhs & fn_lhs & -> & Hcl_lhs2 & IHe_lhs); + destruct Hv_rhs as (x_rhs & fn_rhs & -> & Hcl_rhs2 & IHe_rhs). + + case Hv_inj as [[v_lhs [-> Hv_lhs]] | [v_rhs [-> Hv_rhs]]]. + 1: specialize (IHe_lhs _ Hv_lhs); + simp type_interp in IHe_lhs; + destruct IHe_lhs as (v_res & Hbs_res & Hv_res). + 2: specialize (IHe_rhs _ Hv_rhs); + simp type_interp in IHe_rhs; + destruct IHe_rhs as (v_res & Hbs_res & Hv_res). + + all: exists v_res. + all: simpl; split; last assumption. + + - eapply bs_case_l. + exact Hbs_inj. + econstructor; eauto. + apply big_step_of_val; reflexivity. + - eapply bs_case_r. + exact Hbs_inj. + econstructor; eauto. + apply big_step_of_val; reflexivity. +Qed. Lemma sem_soundness Γ e A : (Γ ⊢ e : A)%ty → @@ -288,9 +412,14 @@ Proof. - apply compat_int. - by eapply compat_app. - by apply compat_add. - (* add compatibility lemmas for the new rules here. *) - (* TODO: exercise *) -Admitted. + - by apply compat_pair. + - (* "Cool theorem prover you got" — this comment was made by the Lean gang *) + exact (proj1 (compat_fst_snd IHsyn_typed)). + - exact (proj2 (compat_fst_snd IHsyn_typed)). + - exact (proj1 (compat_inj _ _ IHsyn_typed)). + - exact (proj2 (compat_inj _ _ IHsyn_typed)). + - by eapply compat_case. +Qed. Lemma termination e A : @@ -304,4 +433,3 @@ Proof. destruct Hsem as (v & Hbs & _); last eauto. constructor. Qed. - diff --git a/theories/type_systems/stlc_extended/types.v b/theories/type_systems/stlc_extended/types.v index 51317d5..9541a36 100644 --- a/theories/type_systems/stlc_extended/types.v +++ b/theories/type_systems/stlc_extended/types.v @@ -47,7 +47,27 @@ Inductive syn_typed : typing_context → expr → type → Prop := Γ ⊢ e1 : Int → Γ ⊢ e2 : Int → Γ ⊢ e1 + e2 : Int - (* TODO: provide the new typing rules *) + | typed_pair Γ e_lhs e_rhs A B: + Γ ⊢ e_lhs : A → + Γ ⊢ e_rhs : B → + Γ ⊢ (Pair e_lhs e_rhs) : A × B + | typed_fst Γ e_pair A B: + Γ ⊢ e_pair: A × B → + Γ ⊢ (Fst e_pair): A + | typed_snd Γ e_pair A B: + Γ ⊢ e_pair: A × B → + Γ ⊢ (Snd e_pair): B + | typed_injl Γ e_inj A B: + Γ ⊢ e_inj : A → + Γ ⊢ (InjL e_inj) : A + B + | typed_injr Γ e_inj A B: + Γ ⊢ e_inj : B → + Γ ⊢ (InjR e_inj) : A + B + | typed_case Γ e_inj e_lhs e_rhs A B C: + Γ ⊢ e_inj: A + B → + Γ ⊢ e_lhs: (A → C) → + Γ ⊢ e_rhs: (B → C) → + Γ ⊢ (Case e_inj e_lhs e_rhs): C where "Γ ⊢ e : A" := (syn_typed Γ e%E A%ty). #[export] Hint Constructors syn_typed : core. @@ -60,8 +80,7 @@ Lemma syn_typed_closed Γ e A X : (∀ x, x ∈ dom Γ → x ∈ X) → is_closed X e. Proof. - (* TODO: you will need to add the new cases, i.e. "|"'s to the intro pattern. The proof then should go through *) - induction 1 as [ | ?????? IH | | | | ] in X |-*; simpl; intros Hx; try done. + induction 1 as [ | ?????? IH | | | | | | | | | | ] in X |-*; simpl; intros Hx; try done. { (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. } { (* lam *) apply IH. intros y. rewrite elem_of_dom lookup_insert_is_Some. @@ -81,8 +100,7 @@ Lemma typed_weakening Γ Δ e A: Γ ⊆ Δ → Δ ⊢ e : A. Proof. - (* TODO: here you will need to add the new cases to the intro pattern as well. The proof then should go through *) - induction 1 as [| Γ x e A B Htyp IH | | | | ] in Δ |-*; intros Hsub; eauto. + induction 1 as [| Γ x e A B Htyp IH | | | | | | | | | | ] in Δ |-*; intros Hsub; eauto. - (* var *) econstructor. by eapply lookup_weaken. - (* lam *) econstructor. eapply IH; eauto. by eapply insert_mono. Qed. @@ -115,13 +133,54 @@ Proof. inversion 1; subst; eauto. Qed. They will be very useful for the proofs below! *) +Lemma pair_inversion Γ e_lhs e_rhs C: + Γ ⊢ (Pair e_lhs e_rhs) : C → + ∃ A B, C = (A × B)%ty ∧ Γ ⊢ e_lhs : A ∧ Γ ⊢ e_rhs : B. +Proof. + inversion 1; subst; eauto. +Qed. + +Lemma fst_inversion Γ e_pair A: + Γ ⊢ (Fst e_pair) : A → + ∃ B, Γ ⊢ e_pair : A × B. +Proof. + inversion 1; subst; eauto. +Qed. + +Lemma snd_inversion Γ e_pair B: + Γ ⊢ (Snd e_pair) : B → + ∃ A, Γ ⊢ e_pair : A × B. +Proof. + inversion 1; subst; eauto. +Qed. + +Lemma injl_inversion Γ e_inj C: + Γ ⊢ (InjL e_inj): C → + ∃ A B, C = (A + B)%ty ∧ Γ ⊢ e_inj: A. +Proof. + inversion 1; subst; eauto. +Qed. + +Lemma injr_inversion Γ e_inj C: + Γ ⊢ (InjR e_inj): C → + ∃ A B, C = (A + B)%ty ∧ Γ ⊢ e_inj: B. +Proof. + inversion 1; subst; eauto. +Qed. + +Lemma case_inversion Γ e_inj e_lhs e_rhs C: + Γ ⊢ (Case e_inj e_lhs e_rhs): C → + ∃ A B, Γ ⊢ e_inj: (A+B)%ty ∧ Γ ⊢ e_lhs: (A → C)%ty ∧ Γ ⊢ e_rhs: (B → C)%ty. +Proof. + inversion 1; subst; eauto. +Qed. Lemma typed_substitutivity e e' Γ (x: string) A B : ∅ ⊢ e' : A → (<[x := A]> Γ) ⊢ e : B → Γ ⊢ lang.subst x e' e : B. Proof. - intros He'. revert B Γ; induction e as [y | y | | | | | | | | | ]; intros B Γ; simpl. + intros He'. revert B Γ; induction e as [y | y | | | | | | | | | ]; intros B Γ; simpl. - intros Hp % var_inversion. destruct (decide (x = y)). + subst. rewrite lookup_insert in Hp. injection Hp as ->. @@ -140,13 +199,23 @@ Proof. - intros (C & Hty1 & Hty2) % app_inversion. eauto. - inversion 1; subst; auto. - intros (-> & Hty1 & Hty2)%plus_inversion; eauto. - - (* TODO *) admit. - - (* TODO *) admit. - - (* TODO *) admit. - - (* TODO *) admit. - - (* TODO *) admit. - - (* TODO *) admit. -Admitted. + - intros Hty%pair_inversion. + destruct Hty as (A' & B' & -> & Hty1 & Hty2). + eauto. + - intros (A' & Hty)%fst_inversion. + econstructor. + exact (IHe _ _ Hty). + - intros (B' & Hty)%snd_inversion; eauto. + - intros (A' & B' & -> & Hty)%injl_inversion. + econstructor. + exact (IHe _ _ Hty). + - intros (A' & B' & -> & Hty)%injr_inversion; eauto. + - intros (A' & B' & Hty_inj & Hty_lhs & Hty_rhs)%case_inversion. + econstructor. + apply IHe1; exact Hty_inj. + apply IHe2; exact Hty_lhs. + apply IHe3; exact Hty_rhs. +Qed. (** Canonical values *) Lemma canonical_values_arr Γ e A B: @@ -165,15 +234,37 @@ Proof. inversion 1; simpl; naive_solver. Qed. -(* TODO: add canonical forms lemmas for the new types *) +Ltac is_val_to_val v H := + rewrite (is_val_spec _) in H; destruct H as [v H]; apply of_to_val in H; symmetry in H. + +Lemma canonical_values_prod Γ e A B : + Γ ⊢ e : A × B → + is_val e → + ∃ e1 e2, e = (e1, e2)%E ∧ is_val e1 ∧ is_val e2. +Proof. + inversion 1; simpl; naive_solver. +Qed. + +Lemma canonical_values_sum Γ e A B : + Γ ⊢ e : A + B → + is_val e → + (∃ e', e = InjL e' ∧ is_val e') ∨ (∃ e', e = InjR e' ∧ is_val e'). +Proof. + inversion 1; simpl; naive_solver. +Qed. (** Progress *) Lemma typed_progress e A: ∅ ⊢ e : A → is_val e ∨ reducible e. Proof. remember ∅ as Γ. - (* TODO: you will need to extend the intro pattern *) - induction 1 as [| | | | Γ e1 e2 A B Hty IH1 _ IH2 | Γ e1 e2 Hty1 IH1 Hty2 IH2]. + induction 1 as [| | | | Γ e1 e2 A B Hty IH1 _ IH2 | Γ e1 e2 Hty1 IH1 Hty2 IH2 | Γ ? ? ? ? Hty_lhs IH_lhs Hty_rhs IH_rhs | + Γ e A B Hty IH | + Γ e A B Hty IH | + Γ e A B Hty IH | + Γ e A B Hty IH | + Γ e e1 e2 A B C Htye IHe Htye1 IHe1 Htye2 IHe2 + ]. - subst. naive_solver. - left. done. - left. done. @@ -194,13 +285,47 @@ Proof. subst. eexists; eapply base_contextual_step. eauto. + right. destruct H1 as [e1' Hstep]. eexists. eauto. + right. destruct H2 as [e2' H2]. eexists. eauto. - -(* FIXME: prove the new cases *) -Admitted. + - destruct (IH_rhs HeqΓ) as [Hval_rhs | Hval_rhs]; + first destruct (IH_lhs HeqΓ) as [Hval_lhs | Hval_lhs]. + + left. constructor; assumption. + + right. + destruct Hval_lhs as [e_lhs' Hstep]. + eexists; eapply contextual_step_pair_l. + assumption. + exact Hstep. + + right. + destruct Hval_rhs as [e_rhs' Hstep]. + eexists; exact (contextual_step_pair_r _ _ _ Hstep). + - (* fst *) + destruct (IH HeqΓ) as [H | H]. + + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done. + right. eexists. eapply base_contextual_step. eapply FstS; assumption. + + right. destruct H as [e' H]. eexists. eauto. + - (* snd *) + destruct (IH HeqΓ) as [H | H]. + + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done. + right. eexists. eapply base_contextual_step. eapply SndS; assumption. + + right. destruct H as [e' H]. eexists. eauto. + - (* injl *) + destruct (IH HeqΓ) as [H | H]. + + left. done. + + right. destruct H as [e' H]. eexists. eauto. + - (* injr *) + destruct (IH HeqΓ) as [H | H]. + + left. done. + + right. destruct H as [e' H]. eexists. eauto. + - (* case *) + right. destruct (IHe HeqΓ) as [H1|H1]. + + eapply canonical_values_sum in Htye as [(e' & -> & ?) | (e' & -> & ?)]; last done. + * eexists. eapply base_contextual_step. econstructor. done. + * eexists. eapply base_contextual_step. econstructor. done. + + destruct H1 as [e' H1]. eexists. eauto. +Qed. Definition ectx_typing (K: ectx) (A B: type) := ∀ e, ∅ ⊢ e : A → ∅ ⊢ (fill K e) : B. +(* This is actually a pretty strong lemma: if ⊢ K[e]: A, then ∃B, ⊢e:B and ∀e',⊢e':B→K[e']: A *) Lemma fill_typing_decompose K e A: ∅ ⊢ fill K e : A → ∃ B, ∅ ⊢ e : B ∧ ectx_typing K B A. @@ -231,9 +356,27 @@ Proof. injection Heq as -> ->. eapply typed_substitutivity; eauto. - eapply plus_inversion in Hty as (-> & Hty1 & Hty2). constructor. - -(* TODO: extend this for the new cases *) -Admitted. + - eapply fst_inversion in Hty as (B & Hty). + eapply pair_inversion in Hty as (A' & B' & H_inj & H1 & H2). + injection H_inj; intros HA HB; subst. + assumption. + - eapply snd_inversion in Hty as (B & Hty). + eapply pair_inversion in Hty as (A' & B' & H_inj & H1 & H2). + injection H_inj; intros HA HB; subst. + assumption. + - eapply case_inversion in Hty as (A' & B' & Hty_inj & Hty_lhs & Hty_rhs). + eapply injl_inversion in Hty_inj as (A'' & B'' & Heq & Hty_inj). + injection Heq as -> ->. + eapply typed_app. + exact Hty_lhs. + exact Hty_inj. + - eapply case_inversion in Hty as (A' & B' & Hty_inj & Hty_lhs & Hty_rhs). + eapply injr_inversion in Hty_inj as (A'' & B'' & Heq & Hty_inj). + injection Heq as -> ->. + eapply typed_app. + exact Hty_rhs. + exact Hty_inj. +Qed. Lemma typed_preservation e e' A: ∅ ⊢ e : A →