Solve most of exercise sheet 1

theories/type_systems/stlc/exercises01.v

@@ -57,80 +57,44 @@ Qed. *)
 Lemma step_det e e' e'':
   step e e' → step e e'' → e' = e''.
 Proof.
-  intros H_step H_step'.
+  intro H_step.
-
+  revert e''.
-  (*
+  (* intro H_step'. *)
-    `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`.
+  induction H_step as [
-
+    name e_λ e_v
-    When swapping `inversion H_step` and `induction e`,
+    | e_fn e_fn' e_v H_val H_fn_step IH
-    the number of things to prove jumps to 30, and I do not know how to quickly prove the incorrect ones.
+    | e_fn e_arg e_arg' H_arg_step IH
-    `inversion e` doesn't introduce any induction hypothesis, so it is also out of the question.
+    | n1 n2 n_sum H_plus
-  *)
+    | e_l e_l' e_r H_val H_l_step IH
-  induction e as [
+    | e_l e_r e_r' H_r_step IH
-    name |
+  ]; subst.
-    name body |
+  all: intros e' H_step'; inversion H_step'; subst; try val_no_step.
-    e_λ IH_λ e_v IH_v |
+  - reflexivity.
-    n |
+  - by rewrite (IH e1').
-    a IH_a b IH_b
+  - by rewrite (IH e2').
-  ].
+  - reflexivity.
-  - inversion H_step.
+  - by rewrite (IH e1').
-  - inversion H_step.
+  - by rewrite (IH e2').
-  - inversion H_step.
+Qed.
-    {
-      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)
-      (* TODO: add more constructors *)
+  | CBNStepApp e_l e_l' e_v :
-.
+      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.
@@ -138,15 +102,38 @@ 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.
-  (* TODO: exercise *)
+  exists (App (λ: "res", (λ: "x", "res")) (App (λ: "y", "y") 0)).
-Admitted.
+  exists (λ: "x", (App (λ: "y", "y") 0))%E.
+  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.
-  (* TODO: exercise *)
+  destruct 1.
-Admitted.
+  all: intuition.
+Qed.
 
 
 (* Same tactic as [val_no_step] but for cbn_step.*)
@@ -159,10 +146,14 @@ Ltac val_no_cbn_step :=
 Lemma cbn_step_det e e' e'':
   cbn_step e e' → cbn_step e e'' → e' = e''.
 Proof.
-  (* TODO: exercise *)
+  intro H_step.
-Admitted.
+  revert e''.
-
+  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.
@@ -175,20 +166,29 @@ Section rtc.
   Lemma rtc_reflexive R : Reflexive (rtc R).
   Proof.
     unfold Reflexive.
-    (* TODO: exercise *)
+    apply rtc_base.
-  Admitted.
+  Qed.
 
   Lemma rtc_transitive R : Transitive (rtc R).
   Proof.
     unfold Transitive.
-    (* TODO: exercise *)
+    intros x y z lhs.
-  Admitted.
+    induction lhs as [| u v w H_uv H_vw IH].
-
+    - 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.
-    (* TODO: exercise *)
+    intro H.
-  Admitted.
+    apply (rtc_step _ x y y).
+    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,26 +235,46 @@ End stdpp.
 Lemma plus_right e1 e2 e2':
   rtc step e2 e2' → rtc step (Plus e1 e2) (Plus e1 e2').
 Proof.
-  (* TODO: exercise *)
+  intro H.
-Admitted.
+  induction H.
-
+  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.
-  (* TODO: exercise *)
+  intro H.
-Admitted.
+  induction H.
-
+  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.
-  (* TODO: exercise *)
+  intro H_n.
-Admitted.
+  intro H_m.
-
-
 
+  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.
@@ -268,51 +288,222 @@ 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.
-  (* TODO: exercise *)
+  intro H_big.
-Admitted.
+  induction H_big; try reflexivity.
-
+  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.
-  (* Note how there is a coercion (automatic conversion) hidden in the
+  intro H.
-   * statement of this lemma: *)
+  remember (of_val v) eqn:H_val in H.
-  Set Printing Coercions.
+  induction H; subst.
-  (* It is sometimes very useful to temporarily print coercions if rewrites or
+  apply big_step_vals.
-   * destructs do not behave as expected. *)
+  remember ((IHrtc (eq_refl (of_val v)))) as IH.
-  Unset Printing Coercions.
+  clear HeqIH.
-  (* TODO: exercise *)
+  clear IHrtc.
-Admitted.
+  (* 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 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.
-  (* TODO: exercise *)
+  exists ((1+1) + (1+1))%E.
-Admitted.
+  exists (2 + (1+1))%E.
-
+  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 big_step_ltr_steps e v :
+Lemma ltr_plus_to_consts e1 e2 n m:
-  big_step e v → rtc ltr_step e (of_val v).
+  rtc ltr_step e1 (LitInt n)
+  → rtc ltr_step e2 (LitInt m)
+  → rtc ltr_step (e1 + e2)%E (LitInt (n + m)%Z).
 Proof.
-  (* TODO: exercise *)
+  intros H_n H_m.
-Admitted.
 
+  (* 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.
+  induction H_big; try reflexivity.
+  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.