pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
frap/LambdaCalculusAndTypeSoundness_template.v
Adam Chlipala bcbb2181be LambdaCalculusAndTypeSoundness_template update
2021-03-27 19:15:05 -04:00

526 lines
13 KiB
Coq
Raw Blame History

(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
* Chapter 11: Lambda Calculus and Simple Type Soundness
* Author: Adam Chlipala
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
Require Import Frap.
(* The last few chapters have focused on small programming languages that are
* representative of the essence of the imperative languages. We now turn to
* lambda-calculus, the usual representative of functional languages. *)
Module Ulc.
Inductive exp : Set :=
| Var (x : var)
| Abs (x : var) (body : exp)
| App (e1 e2 : exp).
Fixpoint subst (rep : exp) (x : var) (e : exp) : exp :=
match e with
| Var y => if y ==v x then rep else Var y
| Abs y e1 => Abs y (if y ==v x then e1 else subst rep x e1)
| App e1 e2 => App (subst rep x e1) (subst rep x e2)
end.
(** * Big-step semantics *)
Inductive eval : exp -> exp -> Prop :=
| BigAbs : forall x e,
eval (Abs x e) (Abs x e)
| BigApp : forall e1 x e1' e2 v2 v,
eval e1 (Abs x e1')
-> eval e2 v2
-> eval (subst v2 x e1') v
-> eval (App e1 e2) v.
Inductive value : exp -> Prop :=
| Value : forall x e, value (Abs x e).
Local Hint Constructors eval value : core.
Theorem value_eval : forall v,
value v
-> eval v v.
Proof.
invert 1; eauto.
Qed.
Local Hint Resolve value_eval : core.
Theorem eval_value : forall e v,
eval e v
-> value v.
Proof.
induct 1; eauto.
Qed.
Local Hint Resolve eval_value : core.
(* Some notations, to let us write more normal-looking lambda terms *)
Coercion Var : var >-> exp.
Notation "\ x , e" := (Abs x e) (at level 50).
Infix "@" := App (at level 49, left associativity).
(* Believe it or not, this is a Turing-complete language! Here's an example
* nonterminating program. *)
Example omega := (\"x", "x" @ "x") @ (\"x", "x" @ "x").
(** * Church Numerals, everyone's favorite example of lambda terms in
* action *)
(* Here are two curious definitions. *)
Definition zero := \"f", \"x", "x".
Definition plus1 := \"n", \"f", \"x", "f" @ ("n" @ "f" @ "x").
(* We can build up any natural number [n] as [plus1^n @ zero]. Let's prove
* that, in fact, these definitions constitute a workable embedding of the
* natural numbers in lambda-calculus. *)
(* A term [plus^n @ zero] evaluates to something very close to what this
* function returns. *)
Fixpoint canonical' (n : nat) : exp :=
match n with
| O => "x"
| S n' => "f" @ ((\"f", \"x", canonical' n') @ "f" @ "x")
end.
(* This missing piece is this wrapper. *)
Definition canonical n := \"f", \"x", canonical' n.
(* Let's formalize our definition of what it means to represent a number. *)
Definition represents (e : exp) (n : nat) :=
eval e (canonical n).
(* Zero passes the test. *)
Theorem zero_ok : represents zero 0.
Proof.
unfold zero, represents, canonical.
simplify.
econstructor.
Qed.
(* So does our successor operation. *)
Theorem plus1_ok : forall e n, represents e n
-> represents (plus1 @ e) (S n).
Proof.
unfold plus1, represents, canonical; simplify.
econstructor.
econstructor.
eassumption.
simplify.
econstructor.
Qed.
(* What's basically going on here? The representation of number [n] is [N]
* such that, for any function [f]:
* N(f) = f^n
* That is, we represent a number as its repeated-composition operator.
* So, given a number, we can use it to repeat any operation. In particular,
* to implement addition, we can just repeat [plus1]! *)
Definition add := \"n", \"m", "n" @ plus1 @ "m".
(* Our addition works properly on this test case. *)
Example add_1_2 : exists v,
eval (add @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v
/\ eval (plus1 @ (plus1 @ (plus1 @ zero))) v.
Proof.
eexists; propositional.
repeat (econstructor; simplify).
repeat econstructor.
Qed.
(* By the way: since [canonical'] doesn't mention variable "m", substituting
* for "m" has no effect. This fact will come in handy shortly. *)
Lemma subst_m_canonical' : forall m n,
subst m "m" (canonical' n) = canonical' n.
Proof.
induct n; simplify; equality.
Qed.
(* This inductive proof is the workhorse for the next result, so let's skip
* ahead there. *)
Lemma add_ok' : forall m n,
eval
(subst (\ "f", (\ "x", canonical' m)) "x"
(subst (\ "n", (\ "f", (\ "x", "f" @ (("n" @ "f") @ "x")))) "f"
(canonical' n))) (canonical (n + m)).
Proof.
induct n; simplify.
econstructor.
econstructor.
econstructor.
econstructor.
econstructor.
econstructor.
econstructor.
simplify.
econstructor.
econstructor.
simplify.
eassumption.
simplify.
econstructor.
Qed.
(* [add] properly encodes the usual addition. *)
Theorem add_ok : forall n ne m me,
represents ne n
-> represents me m
-> represents (add @ ne @ me) (n + m).
Proof.
unfold represents; simplify.
econstructor.
econstructor.
econstructor.
eassumption.
simplify.
econstructor.
eassumption.
simplify.
econstructor.
econstructor.
econstructor.
econstructor.
simplify.
econstructor.
econstructor.
rewrite subst_m_canonical'.
apply add_ok'.
Qed.
(* Let's repeat the same exercise for multiplication. *)
Definition mult := \"n", \"m", "n" @ (add @ "m") @ zero.
Example mult_1_2 : exists v,
eval (mult @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v
/\ eval (plus1 @ (plus1 @ zero)) v.
Proof.
eexists; propositional.
repeat (econstructor; simplify).
repeat econstructor.
Qed.
Lemma mult_ok' : forall m n,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
((\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ (("n" @ "f") @ "x"))))) @ "m")
"f" (canonical' n))) (canonical (n * m)).
Proof.
induct n; simplify.
econstructor.
econstructor.
econstructor.
econstructor.
econstructor.
econstructor.
econstructor.
simplify.
econstructor.
econstructor.
simplify.
eassumption.
simplify.
econstructor.
econstructor.
econstructor.
econstructor.
simplify.
econstructor.
econstructor.
rewrite subst_m_canonical'.
apply add_ok'. (* Note the recursive appeal to correctness of [add]. *)
Qed.
Theorem mult_ok : forall n ne m me,
represents ne n
-> represents me m
-> represents (mult @ ne @ me) (n * m).
Proof.
unfold represents; simplify.
econstructor.
econstructor.
econstructor.
eassumption.
simplify.
econstructor.
eassumption.
simplify.
econstructor.
econstructor.
econstructor.
econstructor.
econstructor.
econstructor.
simplify.
econstructor.
simplify.
econstructor.
econstructor.
simplify.
rewrite subst_m_canonical'.
apply mult_ok'.
Qed.
(** * Small-step semantics *)
Inductive step : exp -> exp -> Prop :=
| ContextBeta : forall x e v,
value v
-> step (App (Abs x e) v) (subst v x e)
(* However, we also need bureaucractic rules for pushing evaluation inside
* applications. *)
| App1 : forall e1 e1' e2,
step e1 e1'
-> step (App e1 e2) (App e1' e2)
| App2 : forall v e2 e2',
value v
-> step e2 e2'
-> step (App v e2) (App v e2').
Local Hint Constructors step : core.
(* Here we now go through a proof of equivalence between big- and small-step
* semantics, though we won't spend any further commentary on it. *)
Lemma step_eval' : forall e1 e2,
step e1 e2
-> forall v, eval e2 v
-> eval e1 v.
Proof.
induct 1; simplify; eauto.
invert H0.
econstructor.
apply IHstep.
eassumption.
eassumption.
assumption.
invert H1.
econstructor.
eassumption.
apply IHstep.
eassumption.
assumption.
Qed.
Local Hint Resolve step_eval' : core.
Theorem step_eval : forall e v,
step^* e v
-> value v
-> eval e v.
Proof.
induct 1; eauto.
Qed.
Local Hint Resolve eval_value : core.
Theorem step_app1 : forall e1 e1' e2,
step^* e1 e1'
-> step^* (App e1 e2) (App e1' e2).
Proof.
induct 1; eauto.
Qed.
Theorem step_app2 : forall e2 e2' v,
value v
-> step^* e2 e2'
-> step^* (App v e2) (App v e2').
Proof.
induct 2; eauto.
Qed.
Theorem eval_step : forall e v,
eval e v
-> step^* e v.
Proof.
induct 1; eauto.
eapply trc_trans.
apply step_app1.
eassumption.
eapply trc_trans.
eapply step_app2.
constructor.
eassumption.
econstructor.
constructor.
eauto.
assumption.
Qed.
End Ulc.
Module Stlc.
Inductive exp : Set :=
| Var (x : var)
| Const (n : nat)
| Plus (e1 e2 : exp)
| Abs (x : var) (e1 : exp)
| App (e1 e2 : exp).
Inductive value : exp -> Prop :=
| VConst : forall n, value (Const n)
| VAbs : forall x e1, value (Abs x e1).
Fixpoint subst (e1 : exp) (x : string) (e2 : exp) : exp :=
match e2 with
| Var y => if y ==v x then e1 else Var y
| Const n => Const n
| Plus e2' e2'' => Plus (subst e1 x e2') (subst e1 x e2'')
| Abs y e2' => Abs y (if y ==v x then e2' else subst e1 x e2')
| App e2' e2'' => App (subst e1 x e2') (subst e1 x e2'')
end.
Inductive step : exp -> exp -> Prop :=
| Beta : forall x e v,
value v
-> step (App (Abs x e) v) (subst v x e)
| Add : forall n1 n2,
step (Plus (Const n1) (Const n2)) (Const (n1 + n2))
| App1 : forall e1 e1' e2,
step e1 e1'
-> step (App e1 e2) (App e1' e2)
| App2 : forall v e2 e2',
value v
-> step e2 e2'
-> step (App v e2) (App v e2')
| Plus1 : forall e1 e1' e2,
step e1 e1'
-> step (Plus e1 e2) (Plus e1' e2)
| Plus2 : forall v e2 e2',
value v
-> step e2 e2'
-> step (Plus v e2) (Plus v e2').
Definition trsys_of (e : exp) := {|
Initial := {e};
Step := step
|}.
Inductive type :=
| Nat (* Numbers *)
| Fun (dom ran : type) (* Functions *).
Inductive hasty : fmap var type -> exp -> type -> Prop :=
| HtVar : forall G x t,
G $? x = Some t
-> hasty G (Var x) t
| HtConst : forall G n,
hasty G (Const n) Nat
| HtPlus : forall G e1 e2,
hasty G e1 Nat
-> hasty G e2 Nat
-> hasty G (Plus e1 e2) Nat
| HtAbs : forall G x e1 t1 t2,
hasty (G $+ (x, t1)) e1 t2
-> hasty G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2,
hasty G e1 (Fun t1 t2)
-> hasty G e2 t1
-> hasty G (App e1 e2) t2.
Local Hint Constructors value step hasty : core.
(* Some notation to make it more pleasant to write programs *)
Infix "-->" := Fun (at level 60, right associativity).
Coercion Const : nat >-> exp.
Infix "^+^" := Plus (at level 50).
Coercion Var : var >-> exp.
Notation "\ x , e" := (Abs x e) (at level 51).
Infix "@" := App (at level 49, left associativity).
(* Some examples of typed programs *)
Example one_plus_one : hasty $0 (1 ^+^ 1) Nat.
Proof.
repeat (econstructor; simplify).
Qed.
Example add : hasty $0 (\"n", \"m", "n" ^+^ "m") (Nat --> Nat --> Nat).
Proof.
repeat (econstructor; simplify).
Qed.
Example eleven : hasty $0 ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) Nat.
Proof.
repeat (econstructor; simplify).
Qed.
Example seven_the_long_way : hasty $0 ((\"x", "x") @ (\"x", "x") @ 7) Nat.
Proof.
repeat (econstructor; simplify).
Qed.
(** * Let's prove type soundness. *)
Definition unstuck e := value e
\/ (exists e' : exp, step e e').
Lemma progress : forall e t,
hasty $0 e t
-> value e
\/ (exists e' : exp, step e e').
Proof.
Admitted.
(* Replacing a typing context with an equal one has no effect (useful to guide
* proof search as a hint). *)
Lemma hasty_change : forall G e t,
hasty G e t
-> forall G', G' = G
-> hasty G' e t.
Proof.
Admitted.
Local Hint Resolve hasty_change : core.
Lemma preservation : forall e1 e2,
step e1 e2
-> forall t, hasty $0 e1 t
-> hasty $0 e2 t.
Proof.
Admitted.
Theorem safety : forall e t, hasty $0 e t
-> invariantFor (trsys_of e) unstuck.
Proof.
simplify.
(* Step 1: strengthen the invariant. In particular, the typing relation is
* exactly the right stronger invariant! Our progress theorem proves the
* required invariant inclusion. *)
apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t).
(* Step 2: apply invariant induction, whose induction step turns out to match
* our preservation theorem exactly! *)
apply invariant_induction; simplify.
equality.
eapply preservation.
eassumption.
assumption.
simplify.
eapply progress.
eassumption.
Qed.
End Stlc.
Reference in a new issue View git blame Copy permalink