of (abs R) (arrow T U) :- pi x\ (of x T => of (R x) U). of (app M N) T :- of M (arrow U T), of N U. eval (abs R) (abs R). eval (app M N) V :- eval M (abs R), eval (R N) V. step (app (abs R) M) (R M). step (app M N) (app M' N) :- step M M'. nstep A A. nstep A C :- step A B, nstep B C.
Click on a command or tactic to see a detailed view of its use.
%% Lambda calculus and various results on typing and evaluation %% %% Even though we use higher-order abstract syntax here, we do not need %% to define a meta-level context predicate because all contexts are %% empty in the inductions. %% %% Determinancy %% Theorem eval_det : forall E V1 V2, {eval E V1} -> {eval E V2} -> V1 = V2. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. search. case H2. apply IH to H3 H5. apply IH to H4 H6. search. Theorem step_det : forall E1 E2 E3, {step E1 E2} -> {step E1 E3} -> E2 = E3. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. search. case H3. case H2. case H3. apply IH to H3 H4. search. Theorem nstep_det : forall E R1 R2, {nstep E (abs R1)} -> {nstep E (abs R2)} -> R1 = R2. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. search. case H3. case H2. case H3. apply step_det to H3 H5. apply IH to H4 H6. search. %% %% Equivalence of semantics %% Theorem nstep_lemma : forall M N R V, {nstep M (abs R)} -> {nstep (R N) V} -> {nstep (app M N) V}. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply IH to H4 H2. search. Theorem eval_nstep : forall E V, {eval E V} -> {nstep E V}. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply IH to H2. apply IH to H3. apply nstep_lemma to H4 H5. search. Theorem step_eval_lemma : forall A B C, {step A B} -> {eval B C} -> {eval A C}. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. case H2. apply IH to H3 H4. search. Theorem nstep_eval : forall E R, {nstep E (abs R)} -> {eval E (abs R)}. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply IH to H3. apply step_eval_lemma to H2 H4. search. %% %% Subject reduction %% Theorem sr_eval : forall E V T, {eval E V} -> {of E T} -> {of V T}. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. case H2. apply IH to H3 H5. case H7. inst H8 with n1 = N. cut H9 with H6. apply IH to H4 H10. search. Theorem sr_step : forall E1 E2 T, {step E1 E2} -> {of E1 T} -> {of E2 T}. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H3. inst H5 with n1 = M. cut H6 with H4. search. case H2. apply IH to H3 H4. search. Theorem sr_nstep : forall E1 E2 T, {nstep E1 E2} -> {of E1 T} -> {of E2 T}. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply sr_step to H3 H2. apply IH to H4 H5. search. %% %% Misc %% % A cut property for typing judgments Theorem type_subst : forall L E E' T T', nabla x, {L, of x T' |- of (E x) T} -> {L |- of E' T'} -> {L |- of (E E') T}. [Show Proof][Hide Proof] intros. inst H1 with n1 = E'. cut H3 with H2. search. % Self application cannot be simply-typed Theorem of_self_app_absurd : forall T, {of (abs (x\ app x x)) T} -> false. [Show Proof][Hide Proof] intros. case H1. case H2. case H3. case H4. case H4. case H5. case H3. case H6. case H7. case H6. % The term (lambda x . x x) (lambda x . x x) does not evaluate to a value Theorem no_eval : forall V, {eval (app (abs x\ app x x) (abs x\ app x x)) V} -> false. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. apply IH to H3. % We can also define divergence coinductivly to prove that % (lambda x . x x) (lambda x . x x) diverges CoDefine diverge (app M N) := diverge M. CoDefine diverge (app M N) := exists R, {eval M (abs R)} /\ diverge (R N). Theorem omega_diverge : diverge (app (abs x\ app x x) (abs x\ app x x)). [Show Proof][Hide Proof] coinduction. search. % More generally we can prove that evaluation and divergence are % mutually exclusive Theorem eval_diverge_absurd : forall M V, {eval M V} -> diverge M -> false. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. apply IH to H3 H5. apply eval_det to H3 H5. apply IH to H4 H6.