release exercise 05

_CoqProject

@@ -46,6 +46,8 @@ theories/type_systems/systemf/parallel_subst.v
 theories/type_systems/systemf/logrel.v
 theories/type_systems/systemf/logrel_sol.v
 theories/type_systems/systemf/free_theorems.v
+theories/type_systems/systemf/binary_logrel.v
+theories/type_systems/systemf/existential_invariants.v
 
 # By removing the # below, you can add the exercise sheets to make
 #theories/type_systems/warmup/warmup.v
@@ -60,3 +62,4 @@ theories/type_systems/systemf/free_theorems.v
 #theories/type_systems/systemf/exercises03_sol.v
 #theories/type_systems/systemf/exercises04.v
 #theories/type_systems/systemf/exercises04_sol.v
+#theories/type_systems/systemf/exercises05.v

theories/type_systems/systemf/exercises05.v

@@ -0,0 +1,169 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.ts.systemf Require Import lang notation parallel_subst types tactics.
+From semantics.ts.systemf Require logrel binary_logrel existential_invariants.
+
+(** * Exercise Sheet 5 *)
+
+Implicit Types
+  (e : expr)
+  (v : val)
+  (A B : type)
+.
+
+(** ** Exercise 3 (LN Exercise 23): Existential Fun *)
+Section existential.
+  (** Since extending our language with records would be tedious,
+    we encode records using nested pairs.
+
+   For instance, we would represent the record type
+   { add : Int → Int → Int; sub : Int → Int → Int; neg : Int → Int }
+   as (Int → Int → Int) × (Int → Int → Int) × (Int → Int).
+
+   Similarly, we would represent the record value
+   { add := λ: "x" "y", "x" + "y";
+     sub := λ: "x" "y", "x" - "y";
+     neg := λ: "x", #0 - "x"
+   }
+  as the nested pair
+  ((λ: "x" "y", "x" + "y",    (* add *)
+    λ: "x" "y", "x" - "y"),   (* sub *)
+    λ: "x", #0 - "x").        (* neg *)
+
+  *)
+
+  (** We will also assume a recursion combinator. We have not formally added it to our language, but we could do so. *)
+  Context (Fix : string → string → expr → val).
+  Notation "'fix:' f x := e" := (Fix f x e)%E
+    (at level 200, f, x at level 1, e at level 200,
+     format "'[' 'fix:'  f  x   :=  '/  ' e ']'") : val_scope.
+  Notation "'fix:' f x := e" := (Fix f x e)%E
+    (at level 200, f, x at level 1, e at level 200,
+     format "'[' 'fix:'  f  x   :=  '/  ' e ']'") : expr_scope.
+  Context (fix_typing : ∀ n Γ (f x: string) (A B: type) (e: expr),
+    type_wf n A →
+    type_wf n B →
+    f ≠ x →
+    TY n; <[x := A]> (<[f := (A → B)%ty]> Γ) ⊢ e : B →
+    TY n; Γ ⊢ (fix: f x := e) : (A → B)).
+
+  Definition ISET : type :=#0. (* TODO: your definition *)
+
+  (* We represent sets as functions of type ((Int → Bool) × Int × Int),
+    storing the mapping, the minimum value, and the maximum value. *)
+  
+
+  Definition iset : val :=#0. (* TODO: your definition *)
+
+  Lemma iset_typed n Γ : TY n; Γ ⊢ iset : ISET.
+  Proof.
+    (* HINT: use repeated solve_typing with an explicit apply fix_typing inbetween *)
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Definition ISETE : type :=#0. (* TODO: your definition *)
+
+  Definition add_equality : val :=#0. (* TODO: your definition *)
+
+  Lemma add_equality_typed n Γ : TY n; Γ ⊢ add_equality : (ISET → ISETE)%ty.
+  Proof.
+    repeat solve_typing.
+  (* Qed. *)
+    (* TODO: exercise *)
+  Admitted.
+
+
+End existential.
+
+Section ex4.
+Import logrel existential_invariants.
+(** ** Exercise 4 (LN Exercise 30): Evenness *)
+(* Consider the following existential type: *)
+Definition even_type : type :=
+  ∃: (#0 ×              (* zero *)
+      (#0 → #0) ×       (* add2 *)
+      (#0 → Int)        (* toint *)
+  )%ty.
+
+(* and consider the following implementation of [even_type]: *)
+Definition even_impl : val :=
+  pack (#0,
+        λ: "z", #2 + "z",
+        λ: "z", "z"
+       ).
+(* We want to prove that [toint] will only every yield even numbers. *)
+(* For that purpose, assume that we have a function [even] that decides even parity available: *)
+Context (even_dec : val).
+Context (even_dec_typed : ∀ n Γ, TY n; Γ ⊢ even_dec : (Int → Bool)).
+
+(* a) Change [even_impl] to [even_impl_instrumented] such that [toint] asserts evenness of the argument before returned.
+You may use the [assert] expression defined in existential_invariants.v.
+*)
+
+Definition even_impl_instrumented : val :=#0. (* TODO: your definition *)
+
+(* b) Prove that [even_impl_instrumented] is safe. You may assume that even works as intended,
+  but be sure to state this here. *)
+
+
+Lemma even_impl_instrumented_safe δ:
+  𝒱 even_type δ even_impl_instrumented.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+End ex4.
+
+(** ** Exercise 5 (LN Exercise 31): Abstract sums *)
+Section ex5.
+Import logrel existential_invariants.
+Definition sum_ex_type (A B : type) : type :=
+  ∃: ((A.[ren (+1)] → #0) ×
+      (B.[ren (+1)] → #0) ×
+      (∀: #1 → (A.[ren (+2)] → #0) → (B.[ren (+2)] → #0) → #0)
+     )%ty.
+
+Definition sum_ex_impl : val :=
+  pack (λ: "x", (#1, "x"),
+        λ: "x", (#2, "x"),
+        Λ, λ: "x" "f1" "f2", if: Fst "x" = #1 then "f1" (Snd "x") else "f2" (Snd "x")
+       ).
+
+Lemma sum_ex_safe A B δ:
+  𝒱 (sum_ex_type A B) δ sum_ex_impl.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+End ex5.
+
+(** For Exercise 6 and 7, see binary_logrel.v *)
+
+(** ** Exercise 8 (LN Exercise 35): Contextual equivalence *)
+Section ex8.
+Import binary_logrel.
+Definition sum_ex_impl' : val :=
+  pack ((λ: "x", InjL "x"),
+        (λ: "x", InjR "x"),
+        (Λ, λ: "x" "f1" "f2", Case "x" "f1" "f2")
+       ).
+
+Lemma sum_ex_impl'_typed n Γ A B :
+  type_wf n A →
+  type_wf n B →
+  TY n; Γ ⊢ sum_ex_impl' : sum_ex_type A B.
+Proof.
+  intros.
+  eapply (typed_pack _ _ _ (A + B)%ty).
+  all: asimpl; solve_typing.
+Qed.
+
+Lemma sum_ex_impl_equiv n Γ A B :
+  ctx_equiv n Γ sum_ex_impl' sum_ex_impl (sum_ex_type A B).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+End ex8.

theories/type_systems/systemf/existential_invariants.v

@@ -0,0 +1,140 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.lib Require Export debruijn.
+From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep tactics.
+From semantics.ts.systemf Require logrel binary_logrel.
+From Equations Require Import Equations.
+
+(** * Existential types and invariants *)
+Implicit Types
+  (Δ : nat)
+  (Γ : typing_context)
+  (v : val)
+  (α : var)
+  (e : expr)
+  (A : type).
+
+(** Here, we take the approach of encoding [assert],
+  instead of adding it as a primitive to the language.
+  This saves us from adding it to all of the existing proofs.
+  But clearly it has the same reduction behavior.
+ *)
+
+Definition assert (e : expr) : expr :=
+  if: e then #LitUnit else (#0 #0).
+Lemma assert_true : rtc contextual_step (assert #true) #().
+Proof.
+  econstructor.
+  { eapply base_contextual_step. constructor. }
+  constructor.
+Qed.
+Lemma assert_false : rtc contextual_step (assert #false) (#0 #0).
+Proof.
+  econstructor. { eapply base_contextual_step. econstructor. }
+  constructor.
+Qed.
+
+Definition Or (e1 e2 : expr) : expr :=
+  if: e1 then #true else e2.
+Definition And (e1 e2 : expr) : expr :=
+  if: e1 then e2 else #false.
+Notation "e1 '||' e2" := (Or e1 e2) : expr_scope.
+Notation "e1 '&&' e2" := (And e1 e2) : expr_scope.
+
+(** *** BIT *)
+(* ∃ α, { bit : α, flip : α → α, get : α → bool } *)
+Definition BIT : type := ∃: (#0 × (#0 → #0)) × (#0 → Bool).
+
+Definition MyBit : val :=
+  pack (#0,                  (* bit *)
+        λ: "x", #1 - "x",    (* flip *)
+        λ: "x", #0 < "x").   (* get *)
+
+Lemma MyBit_typed n Γ :
+  TY n; Γ ⊢ MyBit : BIT.
+Proof. eapply (typed_pack _ _ _ Int); solve_typing. Qed.
+
+Definition MyBit_instrumented : val :=
+  pack (#0,                                                     (* bit *)
+        λ: "x", assert (("x" = #0) || ("x" = #1));; #1 - "x",   (* flip *)
+        λ: "x", assert (("x" = #0) || ("x" = #1));; #0 < "x").  (* get *)
+
+Definition MyBoolBit : val :=
+  pack (#false,                  (* bit *)
+        λ: "x", UnOp NegOp "x",    (* flip *)
+        λ: "x", "x").   (* get *)
+
+Lemma MyBoolBit_typed n Γ :
+  TY n; Γ ⊢ MyBoolBit : BIT.
+Proof.
+  eapply (typed_pack _ _ _ Bool); solve_typing.
+  simpl. econstructor.
+Qed.
+
+
+
+Section unary_mybit.
+  Import logrel.
+
+  Lemma MyBit_instrumented_sem_typed δ :
+    𝒱 BIT δ MyBit_instrumented.
+  Proof.
+    unfold BIT. simp type_interp.
+    eexists. split; first done.
+    pose_sem_type (λ x, x = #0 ∨ x = #1) as τ.
+    { intros v [-> | ->]; done. }
+    exists τ.
+    simp type_interp.
+    eexists _, _. split; first done.
+    split.
+    - simp type_interp. eexists _, _. split; first done. split.
+      + simp type_interp. simpl. by left.
+      + simp type_interp. eexists _, _. split; first done. split; first done.
+        intros v'. simp type_interp; simpl.
+        (* Note: this part of the proof is a bit different from the paper version, as we directly do a case split. *)
+        intros [-> | ->].
+        * exists #1. split; last simp type_interp; simpl; eauto.
+          bs_steps_det. eapply bs_if_true; bs_steps_det.
+          eapply bs_if_true; bs_steps_det.
+        * exists #0. split; last simp type_interp; simpl; eauto.
+          bs_steps_det. eapply bs_if_true; bs_steps_det.
+          eapply bs_if_false; bs_steps_det.
+    - simp type_interp. eexists _, _. split; first done. split; first done.
+      intros v'. simp type_interp; simpl. intros [-> | ->].
+      * exists #false. split; last simp type_interp; simpl; eauto.
+        bs_steps_det. eapply bs_if_true; bs_steps_det. eapply bs_if_true; bs_steps_det.
+      * exists #true. split; last simp type_interp; simpl; eauto.
+        bs_steps_det. eapply bs_if_true; bs_steps_det. eapply bs_if_false; bs_steps_det.
+  Qed.
+
+End unary_mybit.
+
+
+Section binary_mybit.
+  Import binary_logrel.
+
+  Lemma MyBit_MyBoolBit_sem_typed δ :
+    𝒱 BIT δ MyBit MyBoolBit.
+  Proof.
+    unfold BIT. simp type_interp.
+    eexists _, _. split_and!; try done.
+    pose_sem_type (λ v w, (v = #0 ∧ w = #false) ∨ (v = #1 ∧ w = #true)) as τ.
+    { intros v w [[-> ->] | [-> ->]]; done. }
+    exists τ.
+    simp type_interp.
+    eexists _, _, _, _. split_and!; try done.
+    simp type_interp.
+    eexists _, _, _, _. split_and!; try done.
+    - simp type_interp. simpl. naive_solver.
+    - simp type_interp. eexists _, _, _, _. split_and!; try done.
+      intros v w. simp type_interp. simpl.
+      intros [[-> ->]|[-> ->]]; simpl; eexists _, _; split_and!; eauto; simpl.
+      all: simp type_interp; simpl; naive_solver.
+    - simp type_interp. eexists _, _, _, _. split_and!; try done.
+      intros v w. simp type_interp. simpl.
+      intros [[-> ->]|[-> ->]]; simpl.
+      all: eexists _, _; split_and!; eauto; simpl.
+      all: simp type_interp; eauto.
+  Qed.
+
+End binary_mybit.