Catch up on stlc_extended

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 →

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.

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.
-

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 →