theories/type_systems/stlc/exercises01.v

@@ -57,44 +57,80 @@ Qed. *)
 Lemma step_det e e' e'':
   step e e' → step e e'' → e' = e''.
 Proof.
-  intro H_step.
+  intros H_step H_step'.
-  revert e''.
+
-  (* intro H_step'. *)
+  (*
-  induction H_step as [
+    `induction` here seems to introduce incorrect induction hypothesis for IH_λ, IH_v, IH_a, IH_b. Those try to prove that e' = e'', when I need them to prove other equalities later introduced by `inversion H_step`.
-    name e_λ e_v
+
-    | e_fn e_fn' e_v H_val H_fn_step IH
+    When swapping `inversion H_step` and `induction e`,
-    | e_fn e_arg e_arg' H_arg_step IH
+    the number of things to prove jumps to 30, and I do not know how to quickly prove the incorrect ones.
-    | n1 n2 n_sum H_plus
+    `inversion e` doesn't introduce any induction hypothesis, so it is also out of the question.
-    | e_l e_l' e_r H_val H_l_step IH
+  *)
-    | e_l e_r e_r' H_r_step IH
+  induction e as [
-  ]; subst.
+    name |
-  all: intros e' H_step'; inversion H_step'; subst; try val_no_step.
+    name body |
-  - reflexivity.
+    e_λ IH_λ e_v IH_v |
-  - by rewrite (IH e1').
+    n |
-  - by rewrite (IH e2').
+    a IH_a b IH_b
-  - reflexivity.
+  ].
-  - by rewrite (IH e1').
+  - inversion H_step.
-  - by rewrite (IH e2').
+  - inversion H_step.
-Qed.
+  - inversion H_step.
+    {
+      rewrite <-H in H_step'.
+      inversion H_step'.
+      - reflexivity.
+      - inversion H7.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - rewrite <-H4 in H3.
+        inversion H3.
+      - admit.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - val_no_step.
+      - val_no_step.
+      - admit.
+    }
+  - inversion H_step.
+  - inversion H_step.
+    {
+      rewrite <-H in H_step'.
+      rewrite <-H1 in H_step'.
+      inversion H_step'.
+      - rewrite <-H6.
+        rewrite <-H2.
+        reflexivity.
+      - val_no_step.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - rewrite <-H4 in H3.
+        val_no_step.
+      - admit.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - rewrite <-H5 in H2.
+        val_no_step.
+      - val_no_step.
+      - admit.
+    }
+Admitted.
+
 
 (** Exercise 3 (LN Exercise 2): Call-by-name Semantics *)
 Inductive cbn_step : expr → expr → Prop :=
-  | CBNStepBeta x e e' :
+  | CBNStepBeta x e e'  :
       cbn_step (App (Lam x e) e') (subst' x e' e)
-  | CBNStepApp e_l e_l' e_v :
+      (* TODO: add more constructors *)
-      cbn_step e_l e_l' →
+.
-      cbn_step (App e_l e_v) (App e_l' e_v)
-  | CBNStepPlusR e1 e2 e2' :
-      cbn_step e2 e2' →
-      cbn_step (Plus e1 e2) (Plus e1 e2')
-  | CBNStepPlusL e1 e1' v :
-      is_val v →
-      cbn_step e1 e1' →
-      cbn_step (Plus e1 v) (Plus e1' v)
-  | CBNStepPlusInt n1 n2 n_sum :
-      (n1 + n2)%Z = n_sum →
-      cbn_step (Plus (LitInt n1) (LitInt n2)) (LitInt n_sum).
-
 
 (* We make the eauto tactic aware of the constructors of cbn_step *)
 #[global] Hint Constructors cbn_step : core.
@@ -102,38 +138,15 @@ Inductive cbn_step : expr → expr → Prop :=
 Lemma different_results :
   ∃ (e: expr) (e1 e2: expr), rtc cbn_step e e1 ∧ rtc step e e2 ∧ is_val e1 ∧ is_val e2 ∧ e1 ≠ e2.
 Proof.
-  exists (App (λ: "res", (λ: "x", "res")) (App (λ: "y", "y") 0)).
+  (* TODO: exercise *)
-  exists (λ: "x", (App (λ: "y", "y") 0))%E.
+Admitted.
-  exists (λ: "x", (0))%E.
-  split.
-  {
-    apply rtc_once.
-    apply CBNStepBeta.
-  }
-  split.
-  {
-    apply (rtc_l _ _ (App (λ: "res", (λ: "x", "res")) 0)).
-    apply StepAppR.
-    apply StepBeta.
-    unfold is_val; intuition.
-    apply rtc_once.
-    apply StepBeta.
-    unfold is_val; intuition.
-  }
-  split.
-  unfold is_val; intuition.
-  split.
-  unfold is_val; intuition.
-  discriminate.
-Qed.
 
 
 Lemma val_no_cbn_step e e':
   cbn_step e e' → is_val e →  False.
 Proof.
-  destruct 1.
+  (* TODO: exercise *)
-  all: intuition.
+Admitted.
-Qed.
 
 
 (* Same tactic as [val_no_step] but for cbn_step.*)
@@ -146,14 +159,10 @@ Ltac val_no_cbn_step :=
 Lemma cbn_step_det e e' e'':
   cbn_step e e' → cbn_step e e'' → e' = e''.
 Proof.
-  intro H_step.
+  (* TODO: exercise *)
-  revert e''.
+Admitted.
-  induction H_step; subst; intros e'' H_step'; inversion H_step'; subst; try val_no_cbn_step.
+
-  all: try reflexivity.
+
-  - by rewrite (IHH_step e_l'0).
-  - by rewrite (IHH_step e2'0).
-  - by rewrite (IHH_step e1'0).
-Qed.
 
 (** Exercise 4 (LN Exercise 3): Reflexive Transitive Closure *)
 Section rtc.
@@ -166,29 +175,20 @@ Section rtc.
   Lemma rtc_reflexive R : Reflexive (rtc R).
   Proof.
     unfold Reflexive.
-    apply rtc_base.
+    (* TODO: exercise *)
-  Qed.
+  Admitted.
 
   Lemma rtc_transitive R : Transitive (rtc R).
   Proof.
     unfold Transitive.
-    intros x y z lhs.
+    (* TODO: exercise *)
-    induction lhs as [| u v w H_uv H_vw IH].
+  Admitted.
-    - intuition.
+
-    - intro H_wz.
-      apply IH in H_wz as H_vz.
-      apply (rtc_step _ u v z).
-      assumption.
-      exact H_vz.
-  Qed.
 
   Lemma rtc_subrel (R: X → X → Prop) (x y : X): R x y → rtc R x y.
   Proof.
-    intro H.
+    (* TODO: exercise *)
-    apply (rtc_step _ x y y).
+  Admitted.
-    assumption.
-    exact (rtc_reflexive _ _).
-  Qed.
 
 
   Section typeclass.
@@ -224,7 +224,7 @@ Qed.
 Section stdpp.
   (* In fact, [rtc] is so common that it is already provided by the [stdpp] library! *)
   Import stdpp.relations.
-  (* Print rtc. *)
+  Print rtc.
 
   (* The typeclass instances are also already registered. *)
   Goal rtc step (LitInt 42) (LitInt 42).
@@ -235,46 +235,26 @@ End stdpp.
 Lemma plus_right e1 e2 e2':
   rtc step e2 e2' → rtc step (Plus e1 e2) (Plus e1 e2').
 Proof.
-  intro H.
+  (* TODO: exercise *)
-  induction H.
+Admitted.
-  reflexivity.
+
-  eapply rtc_step.
-  (* eauto knows how to instance the results of step :) *)
-  eauto.
-  eauto.
-Qed.
 
 Lemma plus_left e1 e1' n:
   rtc step e1 e1' → rtc step (Plus e1 (LitInt n)) (Plus e1' (LitInt n)).
 Proof.
-  intro H.
+  (* TODO: exercise *)
-  induction H.
+Admitted.
-  reflexivity.
+
-  eapply rtc_step; eauto.
-  apply StepPlusL.
-  unfold is_val; intuition.
-  assumption.
-Qed.
 
 (* The exercise: *)
 Lemma plus_to_consts e1 e2 n m:
   rtc step e1 (LitInt n) → rtc step e2 (LitInt m) → rtc step (e1 + e2)%E (LitInt (n + m)%Z).
 Proof.
-  intro H_n.
+  (* TODO: exercise *)
-  intro H_m.
+Admitted.
+
+
 
-  etransitivity.
-  (* First, reduce the rhs *)
-  apply plus_right.
-  apply H_m.
-  etransitivity.
-  (* Then, reduce the lhs *)
-  apply plus_left.
-  apply H_n.
-  (* Finally, reduce the addition using StepPlusRed *)
-  apply rtc_subrel.
-  eauto.
-Qed.
 
 (* Now that you have an understanding of how rtc works, we can make eauto aware of it. *)
 #[local] Hint Constructors rtc : core.
@@ -288,310 +268,54 @@ Abort.
 
 (** Exercise 5 (LN Exercise 4): Big-step vs small-step semantics *)
 
-Lemma rtc_appr e1 e2 v :
-  rtc step e2 (of_val v) → rtc step (App e1 e2) (App e1 (of_val v)).
-Proof.
-  induction 1; eauto.
-Qed.
-
-Lemma rtc_appl e1 e1' v :
-  rtc step e1 e1' → is_val v → rtc step (App e1 v) (App e1' v).
-Proof.
-  induction 1; eauto.
-Qed.
 
 Lemma big_step_steps e v :
   big_step e v → rtc step e (of_val v).
 Proof.
-  intro H_big.
+  (* TODO: exercise *)
-  induction H_big; try reflexivity.
+Admitted.
-  unfold of_val.
+
-  unfold of_val in IHH_big1.
-  unfold of_val in IHH_big2.
-  apply plus_to_consts; assumption.
-  (* First, reduce the argument *)
-  transitivity (App e1 (of_val v2)).
-  apply rtc_appr.
-  assumption.
-  (* Then, reduce the function to a lambda *)
-  transitivity (App (Lam x e) (of_val v2)).
-  apply rtc_appl.
-  apply IHH_big1.
-  exact (is_val_of_val _).
-  (* Perform the β-substitution *)
-  apply (rtc_step _ _ (subst' x (of_val v2) e)).
-  eauto.
-  (* Finish the proof using the induction hypothesis *)
-  apply IHH_big3.
-Qed.
 
-Lemma is_val_to_of_val {e} :
-  is_val e → ∃ (v: val), e = of_val v.
-Proof.
-  intro H.
-  destruct (is_val_spec e) as [ H_val' _ ].
-  destruct (H_val' H) as [ e_v H_val ].
-  exists e_v.
-  symmetry.
-  by apply of_to_val.
-Qed.
 
 Lemma steps_big_step e (v: val):
   rtc step e v → big_step e v.
 Proof.
-  intro H.
+  (* Note how there is a coercion (automatic conversion) hidden in the
-  remember (of_val v) eqn:H_val in H.
+   * statement of this lemma: *)
-  induction H; subst.
+  Set Printing Coercions.
-  apply big_step_vals.
+  (* It is sometimes very useful to temporarily print coercions if rewrites or
-  remember ((IHrtc (eq_refl (of_val v)))) as IH.
+   * destructs do not behave as expected. *)
-  clear HeqIH.
+  Unset Printing Coercions.
-  clear IHrtc.
+  (* TODO: exercise *)
-  (* This is ridiculous. *)
+Admitted.
-  revert H0.
-  revert IH.
-  revert v.
-  induction H; intros v IH H_rtc.
-  - destruct (is_val_to_of_val H) as [ e'_v H_val ].
-    rewrite H_val.
-    eapply bs_app.
-    apply bs_lam.
-    apply big_step_vals.
-    rewrite <-H_val.
-    assumption.
-  - inversion IH; subst.
-    eapply bs_app.
-    apply IHstep.
-    exact H3.
-    apply big_step_steps.
-    all: eauto.
-  - inversion IH; subst.
-    eapply bs_app.
-    exact H2.
-    apply IHstep.
-    exact H3.
-    apply big_step_steps.
-    all: eauto.
-  - inversion IH; subst.
-    eauto.
-  - inversion IH; subst.
-    assert (big_step e1 (LitIntV z1)).
-    {
-      apply IHstep.
-      assumption.
-      apply big_step_steps.
-      assumption.
-    }
-    eauto.
-  - inversion IH; subst.
-    assert (big_step e2 (LitIntV z2)).
-    {
-      apply IHstep.
-      assumption.
-      apply big_step_steps.
-      assumption.
-    }
-    eauto.
-Qed.
 
 
 
 (** Exercise 6 (LN Exercise 5): left-to-right evaluation *)
-Inductive ltr_step : expr → expr → Prop :=
+Inductive ltr_step : expr → expr → Prop := .
-  | LTRStepBeta x e e' :
-    is_val e' →
-    ltr_step (App (Lam x e) e') (subst' x e' e)
-  | LTRStepAppL e1 e1' e2 :
-    ltr_step e1 e1' →
-    ltr_step (App e1 e2) (App e1' e2)
-  | LTRStepAppR e1 e2 e2' :
-    is_val e1 →
-    ltr_step e2 e2' →
-    ltr_step (App e1 e2) (App e1 e2')
-  | LTRStepPlusRed (n1 n2 n3: Z) :
-    (n1 + n2)%Z = n3 →
-    ltr_step (Plus (LitInt n1) (LitInt n2)) (LitInt n3)
-  | LTRStepPlusL e1 e1' e2 :
-    ltr_step e1 e1' →
-    ltr_step (Plus e1 e2) (Plus e1' e2)
-  | LTRStepPlusR e1 e2 e2' :
-    is_val e1 →
-    ltr_step e2 e2' →
-    ltr_step (Plus e1 e2) (Plus e1 e2')
-.
 
 #[global] Hint Constructors ltr_step : core.
 
 Lemma different_steps_ltr_step :
   ∃ (e: expr) (e1 e2: expr), ltr_step e e1 ∧ step e e2 ∧ e1 ≠ e2.
 Proof.
-  exists ((1+1) + (1+1))%E.
+  (* TODO: exercise *)
-  exists (2 + (1+1))%E.
+Admitted.
-  exists ((1+1) + 2)%E.
-  auto.
-Qed.
-
-Lemma ltr_plus_right n e2 e2':
-  rtc ltr_step e2 e2' → rtc ltr_step (Plus (LitInt n) e2) (Plus (LitInt n) e2').
-Proof.
-  induction 1; eauto.
-  eapply rtc_step.
-  apply LTRStepPlusR.
-  unfold is_val; intuition.
-  exact H.
-  assumption.
-Qed.
-
-Lemma ltr_plus_left e1 e1' e2:
-  rtc ltr_step e1 e1' → rtc ltr_step (Plus e1 e2) (Plus e1' e2).
-Proof.
-  induction 1; eauto.
-Qed.
-
-Lemma ltr_plus_to_consts e1 e2 n m:
-  rtc ltr_step e1 (LitInt n)
-  → rtc ltr_step e2 (LitInt m)
-  → rtc ltr_step (e1 + e2)%E (LitInt (n + m)%Z).
-Proof.
-  intros H_n H_m.
-
-  (* First, reduce the lhs *)
-  etransitivity.
-  apply ltr_plus_left.
-  apply H_n.
-  etransitivity.
-  (* Then, reduce the rhs *)
-  apply ltr_plus_right.
-  apply H_m.
-  (* Finally, reduce the addition using LTRStepPlusRed *)
-  apply rtc_subrel.
-  eauto.
-Qed.
 
 
-Lemma ltr_rtc_appr e1 e_fn v :
-  rtc ltr_step e_fn (of_val v) → is_val e1 → rtc ltr_step (App e1 e_fn) (App e1 (of_val v)).
-Proof.
-  induction 1; eauto.
-Qed.
 
-Lemma ltr_rtc_appl e1 e1' e2 :
-  rtc ltr_step e1 e1' → rtc ltr_step (App e1 e2) (App e1' e2).
-Proof.
-  induction 1; eauto.
-Qed.
 
 Lemma big_step_ltr_steps e v :
   big_step e v → rtc ltr_step e (of_val v).
 Proof.
-  intro H_big.
+  (* TODO: exercise *)
-  induction H_big; try reflexivity.
+Admitted.
-  unfold of_val.
+
-  unfold of_val in IHH_big1.
+
-  unfold of_val in IHH_big2.
+
-  apply ltr_plus_to_consts; assumption.
-  (* First, reduce the argument *)
-  transitivity (App (Lam x e) e2).
-  apply ltr_rtc_appl.
-  assumption.
-  (* Then, reduce the function to a lambda *)
-  transitivity (App (Lam x e) (of_val v2)).
-  apply ltr_rtc_appr.
-  assumption.
-  unfold is_val; intuition.
-  (* Perform the β-substitution *)
-  apply (rtc_step _ _ (subst' x (of_val v2) e)).
-  eauto.
-  (* Finish the proof using the induction hypothesis *)
-  apply IHH_big3.
-Qed.
 
 Lemma ltr_steps_big_step e (v: val):
   rtc ltr_step e v → big_step e v.
 Proof.
-  intro H.
+  (* TODO: exercise *)
-  remember (of_val v) eqn:H_val in H.
+Admitted.
-  induction H; subst.
-  apply big_step_vals.
-  remember ((IHrtc (eq_refl (of_val v)))) as IH.
-  clear HeqIH.
-  clear IHrtc.
-  (* This is ridiculous. *)
-  revert H0.
-  revert IH.
-  revert v.
-  induction H; intros v IH H_rtc.
-  - destruct (is_val_to_of_val H) as [ e'_v H_val ].
-    rewrite H_val.
-    eapply bs_app.
-    apply bs_lam.
-    apply big_step_vals.
-    rewrite <-H_val.
-    assumption.
-  - inversion IH; subst.
-    eapply bs_app.
-    apply IHltr_step.
-    exact H2.
-    apply big_step_ltr_steps.
-    all: eauto.
-  - inversion IH; subst.
-    eapply bs_app.
-    exact H3.
-    apply IHltr_step.
-    exact H4.
-    apply big_step_ltr_steps.
-    all: eauto.
-  - inversion IH; subst.
-    eauto.
-  - inversion IH; subst.
-    assert (big_step e1 (LitIntV z1)).
-    {
-      apply IHltr_step.
-      assumption.
-      apply big_step_ltr_steps.
-      assumption.
-    }
-    eauto.
-  - inversion IH; subst.
-    assert (big_step e2 (LitIntV z2)).
-    {
-      apply IHltr_step.
-      assumption.
-      apply big_step_ltr_steps.
-      assumption.
-    }
-    eauto.
-Qed.
-
-Theorem steps_iff_ltr_steps e v :
-  rtc step e (of_val v) ↔ rtc ltr_step e (of_val v).
-Proof.
-  split.
-  - intro H.
-    apply big_step_ltr_steps.
-    apply steps_big_step.
-    assumption.
-  - intro H.
-    apply big_step_steps.
-    apply ltr_steps_big_step.
-    assumption.
-Qed.
-
-(*
-  This result is unlike languages like javascript, where mutation cause a dependence on the execution order:
-
-  ```
-  let x = 0;
-  function hof() {
-    x *= 2;
-    return (_) => x;
-  }
-  function inc() {
-    x += 1;
-    return x;
-  }
-
-  console.log((hof())(inc()));
-  // prints 1 if hof() is called before inc() (current behavior)
-  // prints 2 if inc() is called before hof()
-  ```
-*)