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

church

parent 448f705d
......@@ -39,8 +39,7 @@ theories/systemf/notation.v
theories/systemf/types.v
theories/systemf/tactics.v
theories/systemf/bigstep.v
theories/systemf/church_encodings.v
# By removing the # below, you can add the exercise sheets to make
# theories/warmup/sheet0.v
......
From stdpp Require Import gmap base relations.
From iris Require Import prelude.
From semantics.lib Require Export debruijn.
From semantics.systemf Require Import lang notation types bigstep tactics.
(** * Church encodings *)
Implicit Types
(Δ : nat)
(Γ : typing_context)
(v : val)
(α : var)
(e : expr)
(A : type).
Definition empty_type : type := ∀: #0.
(** *** Unit *)
Definition unit_type : type := ∀: #0 #0.
Definition unit_inh : val := Λ, λ: "x", "x".
Lemma unit_wf n : type_wf n unit_type.
Proof. eapply type_wf_mono; first repeat econstructor. lia. Qed.
Lemma unit_inh_typed n Γ : TY n; Γ unit_inh : unit_type.
Proof. solve_typing. Qed.
#[export] Hint Resolve unit_wf : core.
#[export] Hint Resolve unit_inh_typed : core.
(** *** Bool *)
Definition bool_type : type := ∀: #0 #0 #0.
Arguments bool_type : simpl never.
Definition bool_true : val := Λ, λ: "t" "f", "t".
Definition bool_false : val := Λ, λ: "t" "f", "f".
Definition bool_if e e1 e2 : expr := (e <> (λ: <>, e1)%E (λ: <>, e2)%E) unit_inh.
Arguments bool_if : simpl never.
Lemma bool_true_typed n Γ : TY n; Γ bool_true : bool_type.
Proof. solve_typing. Qed.
#[export] Hint Resolve bool_true_typed : core.
Lemma bool_false_typed n Γ: TY n; Γ bool_false : bool_type.
Proof. solve_typing. Qed.
#[export] Hint Resolve bool_false_typed : core.
Lemma bool_if_typed n Γ e e1 e2 A :
type_wf n A
TY n; Γ e1 : A
TY n; Γ e2 : A
TY n; Γ e : bool_type
TY n; Γ bool_if e e1 e2 : A.
Proof.
intros Hwf He1 He2 He. econstructor; last eauto.
econstructor; cycle 1.
{ econstructor; first done. apply unit_wf. }
econstructor; cycle 1.
{ econstructor; first done. apply unit_wf. }
eapply (typed_tapp _ _ (#0 #0 #0)%ty); first done.
eauto.
Qed.
#[export] Hint Resolve bool_if_typed : core.
Lemma bool_if_true_red e1 e2 v :
is_closed [] e1
big_step e1 v
big_step (bool_if bool_true e1 e2)%E v.
Proof.
intros. bs_step_det.
Qed.
Lemma bool_if_false_red e1 e2 v :
is_closed [] e2
big_step e2 v
big_step (bool_if bool_false e1 e2)%E v.
Proof.
intros. bs_step_det.
Qed.
(** *** Product types *)
(* Using De Bruijn indices, we need to be a bit careful:
The binder introduced by [∀:] should not be visible in [A] and [B].
Therefore, we need to shift [A] and [B] up by one, using the renaming substitution [ren].
*)
Definition product_type (A B : type) : type := ∀: (A.[ren (+1)] B.[ren (+1)] #0) #0.
Definition pair_val (p : string) (v1 v2 : expr) : val := Λ, λ: p, p v1 v2.
Definition pair_expr (x1 x2 p : string) (e1 e2 : expr) : expr :=
let: x2 := e2 in
let: x1 := e1 in
pair_val p x1 x2.
Definition proj1_expr (x y : string) (e : expr) : expr := e <> (λ: x y, x)%E.
Definition proj2_expr (x y : string) (e : expr) : expr := e <> (λ: x y, y)%E.
(** Throughout all of these lemmas we need to make some of the Barendregt assumptions about variables explicit... *)
Lemma proj1_red p x y v1 v2 :
p x
x y
is_closed [] v1
is_closed [] v2
big_step (proj1_expr x y (pair_val p v1 v2)) v1.
Proof.
intros ?? Hcl1 Hcl2. bs_steps_det.
Qed.
Lemma proj2_red x y p v1 v2 :
p x
x y
is_closed [] v1
is_closed [] v2
big_step (proj2_expr x y (pair_val p v1 v2)) v2.
Proof.
intros ?? Hcl1 Hcl2. bs_steps_det.
Qed.
Lemma pair_red p x1 x2 e1 e2 v1 v2 :
x1 x2
x2 p
x1 p
is_closed [] v2
is_closed [] e1
big_step e1 v1
big_step e2 v2
big_step (pair_expr x1 x2 p e1 e2) (pair_val p v1 v2).
Proof.
intros. bs_steps_det.
Qed.
Lemma proj1_typed x y n Γ e A B :
x y
type_wf n A
type_wf n B
TY n; Γ e : product_type A B
TY n; Γ proj1_expr x y e : A.
Proof.
intros ? HwfA HwfB Hty. unfold proj1_expr.
eapply (typed_app _ _ _ _ (A B A)). 2: solve_typing.
replace_type ((A.[ren (+1)] B.[ren (+1)] #0) #0).[A/]%ty.
econstructor; done.
Qed.
Lemma proj2_typed x y n Γ e A B :
x y
type_wf n A
type_wf n B
TY n; Γ e : product_type A B
TY n; Γ proj2_expr x y e : B.
Proof.
intros ? HwfA HwfB Hty. unfold proj2_expr.
eapply (typed_app _ _ _ _ (A B B)).
2: solve_typing.
replace_type ((A.[ren (+1)] B.[ren (+1)] #0) #0).[B/]%ty.
econstructor; done.
Qed.
Lemma pair_expr_typed n Γ x1 x2 p e1 e2 A B :
p x2
p x1
x1 x2
Γ !! x2 = None
type_wf n A
type_wf n B
TY n; Γ e1 : A
TY n; Γ e2 : B
TY n; Γ pair_expr x1 x2 p e1 e2 : product_type A B.
Proof.
intros ???? HwfA HwfB Hty1 Hty2.
solve_typing.
eapply typed_weakening; [done | | lia]. apply insert_subseteq. done.
Qed.
(** *** Church numerals *)
Definition nat_type : type := ∀: #0 (#0 #0) #0.
Definition zero_val : val := Λ, λ: "z" "s", "z".
Definition num_val (n : nat) : val := Λ, λ: "z" "s", Nat.iter n (App "s") "z".
Definition succ_val : val := λ: "n", Λ, λ: "z" "s", "s" ("n" <> "z" "s").
Definition iter_val : val := λ: "n" "z" "s", "n" <> "z" "s".
Lemma zero_typed Γ n : TY n; Γ zero_val : nat_type.
Proof. solve_typing. Qed.
Lemma num_typed Γ n m : TY n; Γ num_val m : nat_type.
Proof.
solve_typing.
induction m as [ | m IH]; simpl.
- solve_typing.
- solve_typing.
Qed.
Lemma succ_typed Γ n :
TY n; Γ succ_val : (nat_type nat_type).
Proof.
solve_typing.
rewrite fmap_insert. asimpl.
eapply (typed_tapp _ _ (#0 (#0 #0) #0)%ty #0); solve_typing.
Qed.
Lemma iter_typed n Γ C :
type_wf n C
TY n; Γ iter_val : (nat_type C (C C) C).
Proof.
intros Hwf. solve_typing.
eapply (typed_tapp _ _ (#0 (#0 #0) #0)%ty C); solve_typing.
Qed.
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