Commit 6d35b4e3 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

Revert "ex5 template"

This reverts commit 86353384.
parent 86353384
......@@ -65,4 +65,3 @@ theories/systemf/existential_invariants.v
#theories/stlc/cbn_logrel.v
#theories/systemf/exercices04.v
#theories/systemf/exercises04_sol.v
#theories/systemf/exercises05.v
From stdpp Require Import gmap base relations.
From iris Require Import prelude.
From semantics.systemf Require Import lang notation parallel_subst types logrel tactics.
From semantics.systemf Require Import existential_invariants.
(** * Exercise Sheet 5 *)
Implicit Types
(e : expr)
(v : val)
(A B : type)
.
(** ** Exercise 3: 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. (* FIXME: 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. (* FIXME: your definition *)
Lemma iset_typed n Γ : TY n; Γ iset : ISET.
Proof.
(* FIXME *)
(*Qed.*)
Admitted.
Definition ISETE : type :=
#0 (* FIXME *).
Definition add_equality : val :=
#0. (* FIXME *)
Lemma add_equality_typed n Γ : TY n; Γ add_equality : (ISET ISETE)%ty.
Proof.
repeat solve_typing.
(*Qed.*)
Admitted.
End existential.
Section ex4.
(** ** Exercise 4: 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.
*)
Definition even_impl_instrumented : val :=
#0. (* FIXME *)
(* 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.
(* FIXME *)
(*Qed.*)
Admitted.
End ex4.
(** ** Exercise 5: Abstract sums *)
Definition sum_ex_type (A B : type) : type :=
∃: ((A #0) ×
(B #0) ×
(∀: #1 (A #0) (B #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 δ:
type_wf 0 A
type_wf 0 B
𝒱 (sum_ex_type A B) δ sum_ex_impl.
Proof.
(* FIXME *)
Admitted.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment