|
|
@ -5,51 +5,54 @@ From semantics.ts.systemf Require Import lang notation types tactics.
|
|
|
|
(** Exercise 3 (LN Exercise 22): Universal Fun *)
|
|
|
|
(** Exercise 3 (LN Exercise 22): Universal Fun *)
|
|
|
|
|
|
|
|
|
|
|
|
Definition fun_comp : val :=
|
|
|
|
Definition fun_comp : val :=
|
|
|
|
#0 (* TODO *).
|
|
|
|
Λ, Λ, Λ, (λ: "f" "g" "x", "g" ("f" "x")).
|
|
|
|
Definition fun_comp_type : type :=
|
|
|
|
Definition fun_comp_type : type :=
|
|
|
|
#0 (* TODO *).
|
|
|
|
(∀: ∀: ∀: (#0 → #1) → (#1 → #2) → (#0 → #2)).
|
|
|
|
Lemma fun_comp_typed :
|
|
|
|
Lemma fun_comp_typed :
|
|
|
|
TY 0; ∅ ⊢ fun_comp : fun_comp_type.
|
|
|
|
TY 0; ∅ ⊢ fun_comp : fun_comp_type.
|
|
|
|
Proof.
|
|
|
|
Proof.
|
|
|
|
(* should be solved by solve_typing. *)
|
|
|
|
solve_typing.
|
|
|
|
(* TODO: exercise *)
|
|
|
|
Qed.
|
|
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Definition swap_args : val :=
|
|
|
|
Definition swap_args : val :=
|
|
|
|
#0 (* TODO *).
|
|
|
|
Λ, Λ, Λ, (λ: "f", (λ: "x" "y", "f" "y" "x")).
|
|
|
|
Definition swap_args_type : type :=
|
|
|
|
Definition swap_args_type : type :=
|
|
|
|
#0 (* TODO *).
|
|
|
|
(∀: ∀: ∀: (#0 → #1 → #2) → (#1 → #0 → #2)).
|
|
|
|
Lemma swap_args_typed :
|
|
|
|
Lemma swap_args_typed :
|
|
|
|
TY 0; ∅ ⊢ swap_args : swap_args_type.
|
|
|
|
TY 0; ∅ ⊢ swap_args : swap_args_type.
|
|
|
|
Proof.
|
|
|
|
Proof.
|
|
|
|
(* should be solved by solve_typing. *)
|
|
|
|
solve_typing.
|
|
|
|
(* TODO: exercise *)
|
|
|
|
Qed.
|
|
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Definition lift_prod : val :=
|
|
|
|
Definition lift_prod : val :=
|
|
|
|
#0 (* TODO *).
|
|
|
|
Λ, Λ, Λ, Λ, (λ: "f" "g", (λ: "pair",
|
|
|
|
|
|
|
|
(Pair ("f" (Fst "pair")) ("g" (Snd "pair")))
|
|
|
|
|
|
|
|
)).
|
|
|
|
Definition lift_prod_type : type :=
|
|
|
|
Definition lift_prod_type : type :=
|
|
|
|
#0 (* TODO *).
|
|
|
|
(∀: ∀: ∀: ∀: (#0 → #1) → (#2 → #3) → ((#0 × #2) → (#1 × #3))).
|
|
|
|
Lemma lift_prod_typed :
|
|
|
|
Lemma lift_prod_typed :
|
|
|
|
TY 0; ∅ ⊢ lift_prod : lift_prod_type.
|
|
|
|
TY 0; ∅ ⊢ lift_prod : lift_prod_type.
|
|
|
|
Proof.
|
|
|
|
Proof.
|
|
|
|
(* should be solved by solve_typing. *)
|
|
|
|
solve_typing.
|
|
|
|
(* TODO: exercise *)
|
|
|
|
Qed.
|
|
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Definition lift_sum : val :=
|
|
|
|
Definition lift_sum : val :=
|
|
|
|
#0 (* TODO *).
|
|
|
|
Λ, Λ, Λ, Λ, (λ: "f" "g", (λ: "inj",
|
|
|
|
|
|
|
|
(match: "inj" with
|
|
|
|
|
|
|
|
InjL "x" => (InjL ("f" "x"))
|
|
|
|
|
|
|
|
| InjR "x" => (InjR ("g" "x"))
|
|
|
|
|
|
|
|
end)
|
|
|
|
|
|
|
|
)).
|
|
|
|
Definition lift_sum_type : type :=
|
|
|
|
Definition lift_sum_type : type :=
|
|
|
|
#0 (* TODO *).
|
|
|
|
(∀: ∀: ∀: ∀: (#0 → #1) → (#2 → #3) → ((#0 + #2) → (#1 + #3))).
|
|
|
|
Lemma lift_sum_typed :
|
|
|
|
Lemma lift_sum_typed :
|
|
|
|
TY 0; ∅ ⊢ lift_sum : lift_sum_type.
|
|
|
|
TY 0; ∅ ⊢ lift_sum : lift_sum_type.
|
|
|
|
Proof.
|
|
|
|
Proof.
|
|
|
|
(* should be solved by solve_typing. *)
|
|
|
|
solve_typing.
|
|
|
|
(* TODO: exercise *)
|
|
|
|
Qed.
|
|
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** Exercise 5 (LN Exercise 18): Named to De Bruijn *)
|
|
|
|
(** Exercise 5 (LN Exercise 18): Named to De Bruijn *)
|
|
|
@ -73,28 +76,84 @@ Notation "∃: x , τ" :=
|
|
|
|
(PTExists x τ%pty)
|
|
|
|
(PTExists x τ%pty)
|
|
|
|
(at level 100, τ at level 200) : PType_scope.
|
|
|
|
(at level 100, τ at level 200) : PType_scope.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
|
|
|
|
De Bruijn representation of the following types:
|
|
|
|
|
|
|
|
∀α. α:
|
|
|
|
|
|
|
|
∀.#0
|
|
|
|
|
|
|
|
∀α. α → α:
|
|
|
|
|
|
|
|
∀.#0->#0
|
|
|
|
|
|
|
|
∀α, β. α → (β → α) → α:
|
|
|
|
|
|
|
|
∀.∀. #1 -> (#0 -> #1) -> #1
|
|
|
|
|
|
|
|
∀α. (∀β. β → α) → (∀β, δ. β → δ → α):
|
|
|
|
|
|
|
|
∀. (∀. #0 -> #1) -> (∀. ∀. #1 -> #0 -> #2)
|
|
|
|
|
|
|
|
∀α, β. (β → (∀α. α → β)) → α:
|
|
|
|
|
|
|
|
∀. ∀. (#0 -> (∀. #0 -> #1)) -> #1
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Named representation of the following types:
|
|
|
|
|
|
|
|
∀. ∀. #0:
|
|
|
|
|
|
|
|
∀α,β. β
|
|
|
|
|
|
|
|
∀. (∀. #1 → #0):
|
|
|
|
|
|
|
|
∀α. ∀β. α→β
|
|
|
|
|
|
|
|
∀. ∀. (∀. #1 → #0):
|
|
|
|
|
|
|
|
∀α,β,γ. β→γ
|
|
|
|
|
|
|
|
∀. (∀. #0 → #1) → ∀. #0 → #1 → #0:
|
|
|
|
|
|
|
|
∀α. (∀δ. δ→α) → ∀γ. γ → α → γ
|
|
|
|
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(* Imagine being a coq standard library author *)
|
|
|
|
|
|
|
|
Definition merge {A B C: Type} (f: A → B → C):
|
|
|
|
|
|
|
|
option A → option B → option C
|
|
|
|
|
|
|
|
:= fun oa ob => match oa, ob with
|
|
|
|
|
|
|
|
| Some a, Some b => Some (f a b)
|
|
|
|
|
|
|
|
| _, _ => None
|
|
|
|
|
|
|
|
end.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Definition gmap_inc_insert (m: gmap string nat) (key: string): gmap string nat :=
|
|
|
|
|
|
|
|
<[ key := 0 ]> (Nat.succ <$> m).
|
|
|
|
|
|
|
|
|
|
|
|
Fixpoint debruijn (m: gmap string nat) (A: ptype) : option type :=
|
|
|
|
Fixpoint debruijn (m: gmap string nat) (A: ptype) : option type :=
|
|
|
|
None (* FIXME *).
|
|
|
|
match A with
|
|
|
|
|
|
|
|
| PTVar ty_name => TVar <$> (m !! ty_name)
|
|
|
|
|
|
|
|
| PInt => Some Int
|
|
|
|
|
|
|
|
| PBool => Some Bool
|
|
|
|
|
|
|
|
| PTForall ty_name body => TForall <$> (debruijn (gmap_inc_insert m ty_name) body)
|
|
|
|
|
|
|
|
| PTExists ty_name body => TExists <$> (debruijn (gmap_inc_insert m ty_name) body)
|
|
|
|
|
|
|
|
| PFun lhs rhs =>
|
|
|
|
|
|
|
|
merge Fun (debruijn m lhs) (debruijn m rhs)
|
|
|
|
|
|
|
|
end.
|
|
|
|
|
|
|
|
|
|
|
|
(* Example *)
|
|
|
|
(* Example *)
|
|
|
|
Goal debruijn ∅ (∀: "x", ∀: "y", "x" → "y")%pty = Some (∀: ∀: #1 → #0)%ty.
|
|
|
|
Goal debruijn ∅ (∀: "x", ∀: "y", "x" → "y")%pty = Some (∀: ∀: #1 → #0)%ty.
|
|
|
|
Proof.
|
|
|
|
Proof.
|
|
|
|
(* Should be solved by reflexivity. *)
|
|
|
|
reflexivity.
|
|
|
|
(* TODO: exercise *)
|
|
|
|
Qed.
|
|
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "y")%pty = Some (∀: #0 → ∀: #0)%ty.
|
|
|
|
Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "y")%pty = Some (∀: #0 → ∀: #0)%ty.
|
|
|
|
Proof.
|
|
|
|
Proof.
|
|
|
|
(* Should be solved by reflexivity. *)
|
|
|
|
reflexivity.
|
|
|
|
(* TODO: exercise *)
|
|
|
|
Qed.
|
|
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "x")%pty = Some (∀: #0 → ∀: #1)%ty.
|
|
|
|
Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "x")%pty = Some (∀: #0 → ∀: #1)%ty.
|
|
|
|
Proof.
|
|
|
|
Proof.
|
|
|
|
(* Should be solved by reflexivity. *)
|
|
|
|
reflexivity.
|
|
|
|
(* TODO: exercise *)
|
|
|
|
Qed.
|
|
|
|
Admitted.
|
|
|
|
|
|
|
|
|
|
|
|
Theorem debruijn_inv_multiple: ∃ (T1 T2: ptype), T1 ≠ T2 ∧ debruijn ∅ T1 = debruijn ∅ T2.
|
|
|
|
|
|
|
|
Proof.
|
|
|
|
|
|
|
|
exists (∀: "x", "x")%pty.
|
|
|
|
|
|
|
|
exists (∀: "y", "y")%pty.
|
|
|
|
|
|
|
|
split.
|
|
|
|
|
|
|
|
discriminate.
|
|
|
|
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
|
|
|
|
The issue with our naive implementation of ⤉σ is that any non-primitive type can cause unwanted behavior if that type refers to something from the higher context:
|
|
|
|
|
|
|
|
∀. (∀.∀. #0 → #1)<∀.#0→#1> => ∀. (∀. (∀.#0→#1) → #1) and not what we expect, ie ∀. (∀. (∀.#0→#2) → #1)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In the lecture, we also saw `A[id] = (∀. #0 -> #1)[id] = ∀. (#0 -> #1)[⤉id] = ∀. (#0 -> (id(0))) = ∀. #0 -> #0`
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
To fix this, we would have to carefully tweak each value in our substitution map to increment all the free type variables
|
|
|
|
|
|
|
|
*)
|
|
|
|