From fb0a3219b5de10ac0de942d806902af46bb7388c Mon Sep 17 00:00:00 2001
From: mueck <mueck@mpi-sws.org>
Date: Thu, 2 Nov 2023 16:03:25 +0100
Subject: [PATCH] Release exercises02 -- Coq code for the last exercise will be
 released soon

---
 _CoqProject                              |   3 +
 theories/type_systems/stlc/exercises02.v | 273 +++++++++++++++++++++++
 theories/type_systems/stlc/lang.v        |  19 ++
 theories/type_systems/stlc/types.v       | 235 +++++++++++++++++++
 theories/type_systems/stlc/untyped.v     | 221 ++++++++++++++++++
 5 files changed, 751 insertions(+)
 create mode 100644 theories/type_systems/stlc/exercises02.v
 create mode 100644 theories/type_systems/stlc/types.v
 create mode 100644 theories/type_systems/stlc/untyped.v

diff --git a/_CoqProject b/_CoqProject
index 5a2249c..9328d94 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,9 +15,12 @@ theories/lib/sets.v
 # STLC
 theories/type_systems/stlc/lang.v
 theories/type_systems/stlc/notation.v
+theories/type_systems/stlc/untyped.v
+theories/type_systems/stlc/types.v
 
 # By removing the # below, you can add the exercise sheets to make
 #theories/type_systems/warmup/warmup.v
 #theories/type_systems/warmup/warmup_sol.v
 #theories/type_systems/stlc/exercises01.v
 #theories/type_systems/stlc/exercises01_sol.v
+#theories/type_systems/stlc/exercises02.v
diff --git a/theories/type_systems/stlc/exercises02.v b/theories/type_systems/stlc/exercises02.v
new file mode 100644
index 0000000..a759308
--- /dev/null
+++ b/theories/type_systems/stlc/exercises02.v
@@ -0,0 +1,273 @@
+From stdpp Require Import gmap base relations tactics.
+From iris Require Import prelude.
+From semantics.ts.stlc Require Import lang notation.
+From semantics.ts.stlc Require untyped types.
+
+
+(** README: Please also download the assigment sheet as a *.pdf from here:
+            https://cms.sic.saarland/semantics_ws2324/materials/
+            It contains additional explanation and excercises. **)
+
+(** ** Exercise 1: Prove that the structural and contextual semantics are equivalent. *)
+(** You will find it very helpful to separately derive the structural rules of the
+  structural semantics for the contextual semantics. *)
+
+Lemma contextual_step_beta x e e':
+  is_val e' → contextual_step ((λ: x, e) e') (subst' x e' e).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma contextual_step_app_r (e1 e2 e2': expr) :
+  contextual_step e2 e2' →
+  contextual_step (e1 e2) (e1 e2').
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma contextual_step_app_l (e1 e1' e2: expr) :
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (e1 e2) (e1' e2).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma contextual_step_plus_red (n1 n2 n3: Z) :
+  (n1 + n2)%Z = n3 →
+  contextual_step (n1 + n2)%E n3.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma contextual_step_plus_r e1 e2 e2' :
+  contextual_step e2 e2' →
+  contextual_step (Plus e1 e2) (Plus e1 e2').
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma contextual_step_plus_l e1 e1' e2 :
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (Plus e1 e2) (Plus e1' e2).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+(** We register these lemmas as hints for [eauto]. *)
+#[global]
+Hint Resolve contextual_step_beta contextual_step_app_l contextual_step_app_r contextual_step_plus_red contextual_step_plus_l contextual_step_plus_r : core.
+
+Lemma step_contextual_step e1 e2: step e1 e2 → contextual_step e1 e2.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+(** Now the other direction. *)
+(* You may find it helpful to introduce intermediate lemmas. *)
+
+
+Lemma contextual_step_step e1 e2:
+  contextual_step e1 e2 → step e1 e2.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+(** ** Exercise 2: Scott encodings *)
+Section scott.
+  (* take a look at untyped.v for usefull lemmas and definitions *)
+  Import semantics.ts.stlc.untyped.
+
+  (** Scott encoding of Booleans *)
+  Definition true_scott : val := 0(* TODO *).
+  Definition false_scott : val := 0(* TODO *).
+
+  Lemma true_red (v1 v2 : val) :
+    closed [] v1 →
+    closed [] v2 →
+    rtc step (true_scott v1 v2) v1.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma false_red (v1 v2 : val) :
+    closed [] v1 →
+    closed [] v2 →
+    rtc step (false_scott v1 v2) v2.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  (** Scott encoding of Pairs *)
+  Definition pair_scott : val := 0(* TODO *).
+
+  Definition fst_scott : val := 0(* TODO *).
+  Definition snd_scott : val := 0(* TODO *).
+
+  Lemma fst_red (v1 v2 : val) :
+    is_closed [] v1 →
+    is_closed [] v2 →
+    rtc step (fst_scott (pair_scott v1 v2)) v1.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma snd_red (v1 v2 : val) :
+    is_closed [] v1 →
+    is_closed [] v2 →
+    rtc step (snd_scott (pair_scott v1 v2)) v2.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+End scott.
+
+Import semantics.ts.stlc.types.
+
+(** ** Exercise 3: type erasure *)
+(** Source terms *)
+Inductive src_expr :=
+| ELitInt (n: Z)
+(* Base lambda calculus *)
+| EVar (x : string)
+| ELam (x : binder) (A: type) (e : src_expr)
+| EApp (e1 e2 : src_expr)
+(* Base types and their operations *)
+| EPlus (e1 e2 : src_expr).
+
+(** The erasure function *)
+Fixpoint erase (E: src_expr) : expr :=
+0 (* TODO *).
+
+Reserved Notation "Γ '⊢S' e : A" (at level 74, e, A at next level).
+Inductive src_typed : typing_context → src_expr → type → Prop :=
+| src_typed_var Γ x A :
+    Γ !! x = Some A →
+    Γ ⊢S (EVar x) : A
+| src_typed_lam Γ x E A B :
+    (<[ x := A]> Γ) ⊢S E : B →
+    Γ ⊢S (ELam (BNamed x) A E) : (A → B)
+| src_typed_int Γ z :
+    Γ ⊢S (ELitInt z) : Int
+| src_typed_app Γ E1 E2 A B :
+    Γ ⊢S E1 : (A → B) →
+    Γ ⊢S E2 : A →
+    Γ ⊢S EApp E1 E2 : B
+| src_typed_add Γ E1 E2 :
+    Γ ⊢S E1 : Int →
+    Γ ⊢S E2 : Int →
+    Γ ⊢S EPlus E1 E2 : Int
+where "Γ '⊢S' E : A" := (src_typed Γ E%E A%ty) : FType_scope.
+#[export] Hint Constructors src_typed : core.
+
+Lemma type_erasure_correctness Γ E A:
+  (Γ ⊢S E : A)%ty → (Γ ⊢ erase E : A)%ty.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+(** ** Exercise 4: Unique Typing *)
+Lemma src_typing_unique Γ E A B:
+  (Γ ⊢S E : A)%ty → (Γ ⊢S E : B)%ty → A = B.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+(** TODO: Is runtime typing (Curry-style) also unique? Prove it or give a counterexample. *)
+
+
+(** ** Exercise 5: Type Inference *)
+
+Fixpoint type_eq A B :=
+  match A, B with
+  | Int, Int => true
+  | Fun A B, Fun A' B' => type_eq A A' && type_eq B B'
+  | _, _ => false
+  end.
+
+Lemma type_eq_iff A B: type_eq A B ↔ A = B.
+Proof.
+  induction A in B |-*; destruct B; simpl; naive_solver.
+Qed.
+
+Notation ctx := (gmap string type).
+Fixpoint infer_type (Γ: ctx) E :=
+  match E with
+  | EVar x => Γ !! x
+  | ELam (BNamed x) A E =>
+    match infer_type (<[x := A]> Γ) E with
+    | Some B => Some (Fun A B)
+    | None => None
+    end
+  (* TODO: complete the definition for the remaining cases *)
+  | ELitInt l => None (* TODO *)
+  | EApp E1 E2 => None (* TODO *)
+  | EPlus E1 E2 => None (* TODO *)
+  | ELam BAnon A E => None
+  end.
+
+(** Prove both directions of the correctness theorem. *)
+Lemma infer_type_typing Γ E A:
+  infer_type Γ E = Some A → (Γ ⊢S E : A)%ty.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma typing_infer_type Γ E A:
+  (Γ ⊢S E : A)%ty → infer_type Γ E = Some A.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+(** ** Exercise 6: untypable, safe term *)
+
+(* The exercise asks you to:
+  "Give one example if there is such an expression, otherwise prove their non-existence."
+  So either finish one section or the other.
+*)
+
+Section give_example.
+  Definition ust : expr := 0 (* TODO *).
+
+  Lemma ust_safe e':
+    rtc step ust e' → is_val e' ∨ reducible e'.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma ust_no_type Γ A:
+    ¬ (Γ ⊢ ust : A)%ty.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+End give_example.
+
+Section prove_non_existence.
+  Lemma no_ust :
+  ∀ e, (∀ e', rtc step e e' → is_val e' ∨ reducible e') → ∃ A, (∅ ⊢ e : A)%ty.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+End prove_non_existence.
\ No newline at end of file
diff --git a/theories/type_systems/stlc/lang.v b/theories/type_systems/stlc/lang.v
index b668d78..ee27fad 100644
--- a/theories/type_systems/stlc/lang.v
+++ b/theories/type_systems/stlc/lang.v
@@ -319,3 +319,22 @@ Qed.
 
 Lemma subst_closed_nil e x es : closed [] e → subst x es e = e.
 Proof. intros. apply subst_closed with []; set_solver. Qed.
+
+Lemma val_no_step e e':
+  step e e' → is_val e → False.
+Proof.
+  by destruct 1.
+Qed.
+
+Lemma val_no_step' (v : val) (e : expr) :
+  step (of_val v) e -> False.
+Proof.
+  intros H. eapply (val_no_step _ _ H).
+  apply is_val_val.
+Qed.
+
+Ltac val_no_step :=
+  match goal with
+  | [H: step ?e1 ?e2 |- _] =>
+    solve [exfalso; eapply (val_no_step _ _ H); done]
+  end.
\ No newline at end of file
diff --git a/theories/type_systems/stlc/types.v b/theories/type_systems/stlc/types.v
new file mode 100644
index 0000000..67ec84d
--- /dev/null
+++ b/theories/type_systems/stlc/types.v
@@ -0,0 +1,235 @@
+From stdpp Require Import base relations tactics.
+From iris Require Import prelude.
+From semantics.ts.stlc Require Import lang notation.
+From semantics.lib Require Import sets maps.
+
+(** ** Syntactic typing *)
+(** In the Coq formalization, we exclusively define runtime typing (Curry-style). *)
+(** It will be an exercise to consider Church-style typing. *)
+
+Inductive type : Set :=
+  | Int
+  | Fun (A B : type).
+
+Definition typing_context := gmap string type.
+Implicit Types
+  (Γ : typing_context)
+  (v : val)
+  (e : expr)
+  (A : type)
+  (x: string).
+
+(** We define notation for types in a new scope with delimiter [ty].
+  See below for an example. *)
+Declare Scope FType_scope.
+Delimit Scope FType_scope with ty.
+Bind Scope FType_scope with type.
+Infix "→" := Fun : FType_scope.
+Notation "(→)" := Fun (only parsing) : FType_scope.
+
+(** Typing rules *)
+(** We need to reserve the notation beforehand to already use it when defining the
+   typing rules. *)
+Reserved Notation "Γ ⊢ e : A" (at level 74, e, A at next level).
+Inductive syn_typed : typing_context → expr → type → Prop :=
+  | typed_var Γ x A :
+      (* lookup the variable in the context *)
+      Γ !! x = Some A →
+      Γ ⊢ (Var x) : A
+  | typed_lam Γ x e A B :
+      (* add a new type assignment to the context *)
+     (<[ x := A]> Γ) ⊢ e : B →
+      Γ ⊢ (Lam (BNamed x) e) : (A → B)
+  | typed_int Γ z :
+      Γ ⊢ (LitInt z) : Int
+  | typed_app Γ e1 e2 A B :
+      Γ ⊢ e1 : (A → B) →
+      Γ ⊢ e2 : A →
+      Γ ⊢ e1 e2 : B
+  | typed_add Γ e1 e2 :
+      Γ ⊢ e1 : Int →
+      Γ ⊢ e2 : Int →
+      Γ ⊢ e1 + e2 : Int
+where "Γ ⊢ e : A" := (syn_typed Γ e%E A%ty) : FType_scope.
+(** Add constructors to [eauto]'s hint database. *)
+#[export] Hint Constructors syn_typed : core.
+Local Open Scope FType_scope.
+
+(** a small example *)
+Goal ∅ ⊢ (λ: "x", 1 + "x")%E : (Int → Int).
+Proof. eauto. Qed.
+
+(** We derive some inversion lemmas -- this is cleaner than directly
+  using the [inversion] tactic everywhere.*)
+Lemma var_inversion Γ (x: string) A: Γ ⊢ x : A → Γ !! x = Some A.
+Proof. inversion 1; subst; auto. Qed.
+
+Lemma lam_inversion Γ (x: binder) e C:
+  Γ ⊢ (λ: x, e) : C →
+  ∃ A B y, C = (A → B)%ty ∧ x = BNamed y ∧ <[y:=A]> Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma lit_int_inversion Γ (n: Z) A: Γ ⊢ n : A → A = Int.
+Proof. inversion 1; subst; auto. Qed.
+
+Lemma app_inversion Γ e1 e2 B:
+  Γ ⊢ e1 e2 : B →
+  ∃ A,  Γ ⊢ e1 : (A → B) ∧  Γ ⊢ e2 : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma plus_inversion Γ e1 e2 B:
+  Γ ⊢ e1 + e2 : B →
+  B = Int ∧ Γ ⊢ e1 : Int ∧ Γ ⊢ e2 : Int.
+Proof. inversion 1; subst; eauto. Qed.
+
+
+Lemma syn_typed_closed Γ e A X :
+  Γ ⊢ e : A →
+  (∀ x, x ∈ dom Γ → x ∈ X) →
+  is_closed X e.
+Proof.
+  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.
+    intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
+    apply elem_of_cons. right. eapply Hx. by apply elem_of_dom.
+  }
+  (* everything else *)
+  all: repeat match goal with
+              | |- Is_true (_ && _)  => apply andb_True; split
+              end.
+  all: naive_solver.
+Qed.
+
+Lemma typed_weakening Γ Δ e A:
+  Γ ⊢ e : A →
+  Γ ⊆ Δ →
+  Δ ⊢ e : A.
+Proof.
+  induction 1 as [| Γ x e A B Htyp IH | | | ] in Δ; intros Hsub; eauto.
+  - econstructor. by eapply lookup_weaken.
+  - econstructor. eapply IH. by eapply insert_mono.
+Qed.
+
+(** Preservation of typing under substitution *)
+Lemma typed_substitutivity e e' Γ x A B :
+  ∅ ⊢ e' : A →
+  <[x := A]> Γ ⊢ e : B →
+  Γ ⊢ subst x e' e : B.
+Proof.
+  intros He'. revert B Γ; induction e as [y | y | | |]; intros B Γ; simpl.
+  - intros Hp%var_inversion; destruct decide; subst; eauto.
+    + rewrite lookup_insert in Hp. injection Hp as ->.
+      eapply typed_weakening; first done. apply map_empty_subseteq.
+    + rewrite lookup_insert_ne in Hp; last done. auto.
+  - intros (C & D & z & -> & -> & Hty)%lam_inversion.
+    econstructor. destruct decide as [|Heq]; simplify_eq.
+    + by rewrite insert_insert in Hty.
+    + rewrite insert_commute in Hty; last naive_solver. eauto.
+  - intros (C & Hty1 & Hty2)%app_inversion; eauto.
+  - intros ->%lit_int_inversion. eauto.
+  - intros (-> & Hty1 & Hty2)%plus_inversion; eauto.
+Qed.
+
+(** Canonical value lemmas *)
+Lemma canonical_values_arr Γ e A B:
+  Γ ⊢ e : (A → B) →
+  is_val e →
+  ∃ x e', e = (λ: x, e')%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_int Γ e:
+  Γ ⊢ e : Int →
+  is_val e →
+  ∃ n: Z, e = n.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+
+(** Progress lemma *)
+Lemma typed_progress e A:
+  ∅ ⊢ e : A → is_val e ∨ contextual_reducible e.
+Proof.
+  remember ∅ as Γ. induction 1 as [| | | Γ e1 e2 A B Hty IH1 _ IH2 | Γ e1 e2 Hty1 IH1 Hty2 IH2].
+  - subst. naive_solver.
+  - left. done.
+  - left. done.
+  - destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+    + eapply canonical_values_arr in Hty as (x & e & ->); last done.
+      right. eexists.
+      eapply base_contextual_step, BetaS; eauto.
+    + right. eapply is_val_spec in H2 as [v Heq].
+      replace e2 with (of_val v); last by eapply of_to_val.
+      destruct H1 as [e1' Hstep].
+      eexists. eapply (fill_contextual_step (AppLCtx HoleCtx v)). done.
+    + right. destruct H2 as [e2' H2].
+      eexists. eapply (fill_contextual_step (AppRCtx e1 HoleCtx)). done.
+  - destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+    + right. eapply canonical_values_int in Hty1 as [n1 ->]; last done.
+      eapply canonical_values_int in Hty2 as [n2 ->]; last done.
+      eexists. eapply base_contextual_step. eapply PlusS; eauto.
+    + right. eapply is_val_spec in H2 as [v Heq].
+      replace e2 with (of_val v); last by eapply of_to_val.
+      destruct H1 as [e1' Hstep].
+      eexists. eapply (fill_contextual_step (PlusLCtx HoleCtx v)). done.
+    + right. destruct H2 as [e2' H2].
+      eexists. eapply (fill_contextual_step (PlusRCtx e1 HoleCtx)). done.
+Qed.
+
+(** Contextual typing *)
+Definition ectx_typing (K: ectx) (A B: type) :=
+  ∀ e, ∅ ⊢ e : A → ∅ ⊢ (fill K e) : B.
+
+Lemma fill_typing_decompose K e A:
+  ∅ ⊢ fill K e : A →
+  ∃ B, ∅ ⊢ e : B ∧ ectx_typing K B A.
+Proof.
+  unfold ectx_typing; induction K in e,A |-*; simpl; eauto.
+  all: inversion 1; subst; edestruct IHK as [B [Hit Hty]]; eauto.
+Qed.
+
+Lemma fill_typing_compose K e A B:
+  ∅ ⊢ e : B →
+  ectx_typing K B A →
+  ∅ ⊢ fill K e : A.
+Proof.
+  intros H1 H2; by eapply H2.
+Qed.
+
+(** Base preservation *)
+Lemma typed_preservation_base_step e e' A:
+  ∅ ⊢ e : A →
+  base_step e e' →
+  ∅ ⊢ e' : A.
+Proof.
+  intros Hty Hstep. destruct Hstep as [| e1 e2 n1 n2 n3 Heq1 Heq2 Heval]; subst.
+  - eapply app_inversion in Hty as (B & Hty1 & Hty2).
+    eapply lam_inversion in Hty1 as (B' & A' & y & Heq1 & Heq2 & Hty).
+    simplify_eq. eapply typed_substitutivity; eauto.
+  - eapply plus_inversion in Hty as (-> & Hty1 & Hty2).
+    econstructor.
+Qed.
+
+(** Preservation *)
+Lemma typed_preservation e e' A:
+  ∅ ⊢ e : A →
+  contextual_step e e' →
+  ∅ ⊢ e' : A.
+Proof.
+  intros Hty Hstep. destruct Hstep as [K e1 e2 -> -> Hstep].
+  eapply fill_typing_decompose in Hty as [B [H1 H2]].
+  eapply fill_typing_compose; last done.
+  by eapply typed_preservation_base_step.
+Qed.
+
+Lemma typed_safety e1 e2 A:
+  ∅ ⊢ e1 : A →
+  rtc contextual_step e1 e2 →
+  is_val e2 ∨ contextual_reducible e2.
+Proof.
+  induction 2; eauto using typed_progress, typed_preservation.
+Qed.
diff --git a/theories/type_systems/stlc/untyped.v b/theories/type_systems/stlc/untyped.v
new file mode 100644
index 0000000..c38d85e
--- /dev/null
+++ b/theories/type_systems/stlc/untyped.v
@@ -0,0 +1,221 @@
+From stdpp Require Import base relations tactics.
+From iris Require Import prelude.
+From semantics.lib Require Import sets maps.
+From semantics.ts.stlc Require Import lang notation.
+
+(** The following two lemmas will be helpful in the sequel.
+  They just lift multiple reduction steps (via [rtc]) to application.
+ *)
+Lemma steps_app_r (e1 e2 e2' : expr) :
+  rtc step e2 e2' →
+  rtc step (e1 e2) (e1 e2').
+Proof.
+  induction 1 as [ e | e e' e'' Hstep Hsteps IH].
+  - reflexivity.
+  - eapply (rtc_l _ _ (e1 e')).
+    { by eapply StepAppR. }
+    done.
+Qed.
+
+Lemma steps_app_l (e1 e1' e2 : expr) :
+  is_val e2 →
+  rtc step e1 e1' →
+  rtc step (e1 e2) (e1' e2).
+Proof.
+  intros Hv.
+  induction 1 as [ e | e e' e'' Hstep Hsteps IH].
+  - reflexivity.
+  - eapply (rtc_l _ _ (e' e2)).
+    { by eapply StepAppL. }
+    done.
+Qed.
+
+
+(** * Untyped λ calculus *)
+
+(** We do not re-define the language to remove primitive addition -- instead, we just
+  restrict our usage in this file to variables, application, and lambdas.
+ *)
+
+
+Definition I_val : val := λ: "x", "x".
+Definition F_val : val := λ: "x" "y", "x".
+Definition S_val : val := λ: "x" "y", "y".
+Definition ω : val := λ: "x", "x" "x".
+Definition Ω : expr := ω ω.
+
+
+(** Ω reduces to itself! *)
+Lemma Omega_step : step Ω Ω.
+Proof.
+  apply StepBeta. done.
+Qed.
+
+(** ** Scott encodings *)
+
+Definition zero : val := λ: "x" "y", "x".
+
+Definition succ (n : val) : val := λ: "x" "y", "y" n.
+(** [Succ] can be seen as a constructor: it takes [n] at the level of the language. *)
+Definition Succ : val := λ: "n" "x" "y", "y" "n".
+
+Fixpoint enc_nat (n : nat) : val :=
+  match n with
+  | 0 => zero
+  | S n => succ (enc_nat n)
+  end.
+
+Lemma enc_nat_closed n :
+  closed [] (enc_nat n).
+Proof.
+  induction n as [ | n IH].
+  - done.
+  - simpl. by apply closed_weaken_nil.
+Qed.
+
+Lemma enc_0_red (z s : val) :
+  is_closed [] z →
+  rtc step (enc_nat 0 z s) z.
+Proof.
+  intros Hcl.
+  eapply rtc_l.
+  { econstructor; first auto. econstructor. auto. }
+  simpl. eapply rtc_l.
+  { econstructor. auto. }
+  simpl. rewrite subst_closed_nil; done.
+Qed.
+
+Lemma enc_S_red n (z s : val) :
+  rtc step (enc_nat (S n) z s) (s (enc_nat n)).
+Proof.
+  simpl. eapply rtc_l.
+  { econstructor; first auto. econstructor. auto. }
+  simpl. eapply rtc_l.
+  { econstructor. auto. }
+  simpl. rewrite (subst_closed_nil (enc_nat n)); last apply enc_nat_closed.
+  rewrite subst_closed_nil; last apply enc_nat_closed.
+  reflexivity.
+Qed.
+
+Lemma Succ_red n : step (Succ (enc_nat n)) (enc_nat (S n)).
+Proof. econstructor. apply is_val_val. Qed.
+
+Lemma Succ_red_n n : rtc step (Nat.iter n Succ zero) (enc_nat n).
+Proof.
+  induction n as [ | n IH].
+  - reflexivity.
+  - simpl.
+    etrans.
+    { simpl. eapply steps_app_r. apply IH. }
+    eapply rtc_l.
+    { apply Succ_red. }
+    reflexivity.
+Qed.
+
+(** ** Recursion *)
+Definition Fix' : val := λ: "z" "y", "y" (λ: "x", "z" "z" "y" "x").
+Definition Fix (s : val) : val := λ: "x", Fix' Fix' s "x".
+Arguments Fix : simpl never.
+
+Local Hint Immediate is_val_val : core.
+
+(** We prove that it satisfies the recursive unfolding *)
+Lemma Fix_step (s r : val) :
+  is_closed [] s →
+  rtc step (Fix s r) (s ((Fix s))%E r).
+Proof.
+  intros Hclosed.
+  eapply rtc_l.
+  { econstructor. auto. }
+  eapply rtc_l.
+  { simpl. econstructor; first by auto.
+    econstructor. { rewrite subst_closed_nil; auto. }
+    econstructor. done.
+  }
+  simpl. rewrite subst_closed_nil; last done.
+  eapply rtc_l.
+  { econstructor; first by auto.
+    econstructor. auto.
+  }
+  simpl. reflexivity.
+Qed.
+
+(** Example usage: addition on Scott-encoded numbers *)
+Definition add_step : val := λ: "r", λ: "n" "m", "n" "m" (λ: "p", Succ ("r" "p" "m")).
+Definition add := Fix add_step.
+
+(** We are now going to prove it correct:
+ [add (enc_nat n) (enc_nat m)) ≻* (enc_nat (n + m))]
+
+ First, we prove that it satisfies the expected defining equations for Peano addition.
+ *)
+
+Lemma add_step_0 m : rtc step (add (enc_nat 0) (enc_nat m)) (enc_nat m).
+Proof.
+  (* use the unfolding equation of the fixpoint combinator *)
+  etrans.
+  { eapply steps_app_l; first by auto.
+    eapply Fix_step. done.
+  }
+  (* subst it into the [add_step] function *)
+  eapply rtc_l.
+  { econstructor; auto. econstructor; auto. econstructor. auto. }
+  simpl.
+  (* subst in the zero *)
+  eapply rtc_l.
+  { econstructor; auto. econstructor. done. }
+  simpl.
+  (* subst in the m *)
+  eapply rtc_l.
+  { econstructor; auto. }
+  simpl.
+
+  (* do a step *)
+  etrans.
+  { apply (enc_0_red (enc_nat m) (λ: "p", Succ (Fix add_step "p" (enc_nat m)))).
+    apply enc_nat_closed.
+  }
+  reflexivity.
+Qed.
+
+Lemma add_step_S n m : rtc step (add (enc_nat (S n)) (enc_nat m)) (Succ (add (enc_nat n) (enc_nat m))).
+Proof.
+  (* use the unfolding equation of the fixpoint combinator *)
+  etrans.
+  { eapply steps_app_l; first by auto.
+    eapply Fix_step. done.
+  }
+  (* subst it into the [add_step] function *)
+  eapply rtc_l.
+  { econstructor; auto. econstructor; auto. econstructor. auto. }
+  simpl.
+  (* subst in the zero *)
+  eapply rtc_l.
+  { econstructor; auto. econstructor. done. }
+  simpl.
+  (* subst in the m *)
+  eapply rtc_l.
+  { econstructor; auto. }
+  simpl.
+  (* do a step *)
+  etrans.
+  { rewrite subst_closed_nil; last apply enc_nat_closed.
+    apply (enc_S_red n (enc_nat m) (λ: "p", Succ (Fix add_step "p" (enc_nat m)))).
+  }
+
+  eapply rtc_l.
+  { econstructor. auto. }
+  simpl.
+  rewrite subst_closed_nil; last apply enc_nat_closed.
+  reflexivity.
+Qed.
+
+Lemma add_correct n m : rtc step (add (enc_nat n) (enc_nat m)) (enc_nat (n + m)).
+Proof.
+  induction n as [ | n IH].
+  - apply add_step_0.
+  - etrans. { apply add_step_S. }
+    etrans. { apply steps_app_r. apply IH. }
+    eapply rtc_l. { apply Succ_red. }
+    reflexivity.
+Qed.