type top. type (arrow A B) :- type A, type B. value (abs A R). of (app M N) B :- of M (arrow A B), of N A. of (abs A R) (arrow A B) :- type A, pi x\ (of x A => of (R x) B). % We add [type A] in order to reflect typing during reasoning. % Without this we would have to worry about judgments like % of (abs bad (x\ x)) (arrow bad bad) % which doesn't make sense since bad isn't a valid type. step (app M N) (app M' N) :- step M M'. step (app M N) (app M N') :- value M, step N N'. step (app (abs A R) M) (R M) :- value M. steps M M. steps M N :- step M P, steps P N.
Click on a command or tactic to see a detailed view of its use.
%% Tait's logical relations argument for weak normalization of STLC %% %% This is based on the presentation in Types and Programming %% Languages by Pierce. %% Conventions: %% Types: A, B, C %% Terms: M, N, P, R %% Values (Terms): V %% Contexts: L Define halts M := exists V, {steps M V} /\ {value V}. %% Reduce is the logical relation used to prove normalization. %% %% This definition uses itself recursively in a negative context (the %% left side of an implication). In order to guarantee consistency of %% the system we must ensure this definition is stratified. Note the %% second argument to reduce is strictly smaller in the (negative) %% recursive occurrence, thus the definition is indeed stratified. Define reduce M top := {of M top} /\ halts M. Define reduce M (arrow A B) := {of M (arrow A B)} /\ halts M /\ (forall N, reduce N A -> reduce (app M N) B). Theorem reduce_halts : forall A M, reduce M A -> halts M. [Show Proof][Hide Proof] intros. case H1. search. search. Theorem reduce_of : forall A M, reduce M A -> {of M A}. [Show Proof][Hide Proof] intros. case H1. search. search. %% Properties of evaluation Theorem absurd_step_value : forall V M, {step V M} -> {value V} -> false. [Show Proof][Hide Proof] intros. case H2. case H1. Theorem step_det : forall M N P, {step M N} -> {step M P} -> N = P. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. apply IH to H3 H4. search. apply absurd_step_value to H3 H4. case H3. case H2. apply absurd_step_value to H5 H3. apply IH to H4 H6. search. apply absurd_step_value to H4 H5. case H2. case H4. apply absurd_step_value to H5 H3. search. Theorem step_follows_steps : forall M N V, {step M N} -> {steps M V} -> {value V} -> {steps N V}. [Show Proof][Hide Proof] intros. case H2. apply absurd_step_value to H1 H3. apply step_det to H1 H4. search. % steps is defined by left recursion on step, so this lemma tells us % that it acts right recursively as well Theorem steps_right : forall M N R, {steps M N} -> {step N R} -> {steps M R}. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply IH to H4 H2. search. Theorem steps_app_value : forall M N R, {value M} -> {steps N R} -> {steps (app M N) (app M R)}. [Show Proof][Hide Proof] induction on 2. intros. case H2. search. apply IH to H1 H4. search. Theorem halt_step_forward : forall M N, halts M -> {step M N} -> halts N. [Show Proof][Hide Proof] intros. case H1. apply step_follows_steps to H2 H3 H4. search. Theorem halt_step_backward : forall M N, halts N -> {step M N} -> halts M. [Show Proof][Hide Proof] intros. case H1. search. Theorem of_step_forward : forall M N A, {of M A} -> {step M N} -> {of N A}. [Show Proof][Hide Proof] induction on 2. intros. case H2. case H1. apply IH to H4 H3. search. case H1. apply IH to H6 H4. search. case H1. case H4. inst H7 with n1 = M1. cut H8 with H5. search. Theorem reduce_step_forward : forall M N A, reduce M A -> {step M N} -> reduce N A. [Show Proof][Hide Proof] induction on 1. intros. case H1. apply of_step_forward to H3 H2. apply halt_step_forward to H4 H2. search. unfold. apply of_step_forward to H3 H2. search. apply halt_step_forward to H4 H2. search. intros. apply H5 to H6. apply IH to H7 _. search. Theorem reduce_steps_forward : forall M N A, reduce M A -> {steps M N} -> reduce N A. [Show Proof][Hide Proof] induction on 2. intros. case H2. search. apply reduce_step_forward to H1 H3. apply IH to H5 H4. search. Theorem reduce_step_backward : forall M N A, reduce N A -> {step M N} -> {of M A} -> reduce M A. [Show Proof][Hide Proof] induction on 1. intros. case H1. apply halt_step_backward to H5 H2. search. unfold. search. apply halt_step_backward to H5 H2. search. intros. apply H6 to H7. apply reduce_of to H7. apply IH to H8 _ _. search. Theorem reduce_steps_backward : forall M N A, reduce N A -> {steps M N} -> {of M A} -> reduce M A. [Show Proof][Hide Proof] induction on 2. intros. case H2. search. apply of_step_forward to H3 H4. apply IH to H1 H5 H6. apply reduce_step_backward to H7 H4 H3. search. %% Properties about nominal constants, e.g. where they can and cannot occur. %% Also properties about the contexts of judgments. % of_ctx defines the context of "of M A" judgments. The judgment {type A} % ensures that all types in the context are well-formed, e.g. they do % not contain nominal constants. Define of_ctx nil. Define nabla x, of_ctx (of x A :: L) := {type A} /\ of_ctx L. % A term is closed if it can be typed in the empty context Define closed M := exists A, {of M A}. Define nabla x, fresh x M. Theorem member_fresh : forall X L E, member E L -> fresh X L -> fresh X E. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. search. assert fresh X L1. case H2. search. apply IH to H3 H4. search. % Types do not contain nominal constants, thus any dependencies on % nominal constants can be pruned Theorem prune_type : forall A, nabla x, {type (A x)} -> exists B, A = (x\ B). [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply IH to H2. apply IH to H3. search. Theorem absurd_member_type_of_ctx : forall L A, member (type A) L -> of_ctx L -> false. [Show Proof][Hide Proof] induction on 2. intros. case H2. case H1. case H1. apply IH to H5 H4. Theorem type_ignores_of_ctx : forall L A, of_ctx L -> {L |- type A} -> {type A}. [Show Proof][Hide Proof] induction on 2. intros. case H2. apply absurd_member_type_of_ctx to H3 H1. search. apply IH to H1 H3. apply IH to H1 H4. search. % A term cannot contain a nominal variable which does not appear in % its typing context L. Theorem prune_of : forall L R A, nabla x, of_ctx L -> {L |- of (R x) (A x)} -> exists M, R = (x\ M). [Show Proof][Hide Proof] induction on 2. intros. case H2. apply member_fresh to H3 _. case H4. search. apply IH to H1 H3. apply IH to H1 H4. search. apply type_ignores_of_ctx to H1 H3. apply prune_type to H5. apply IH to _ H4. search. % Closed terms cannot contain any nominal constants Theorem prune_closed : forall R, nabla x, closed (R x) -> exists M, R = (x\ M). [Show Proof][Hide Proof] intros. case H1. apply prune_of to _ H2. search. Theorem reduce_closed : forall M A, reduce M A -> closed M. [Show Proof][Hide Proof] intros. apply reduce_of to H1. search. Theorem prune_reduce : forall R A, nabla x, reduce (R x) A -> exists M, R = (x\ M). [Show Proof][Hide Proof] intros. apply reduce_closed to H1. apply prune_closed to H2. search. Theorem of_ctx_type : forall L M A, of_ctx L -> member (of M A) L -> {type A}. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. search. apply IH to H4 H5. search. Theorem of_type : forall L M A, of_ctx L -> {L |- of M A} -> {type A}. [Show Proof][Hide Proof] induction on 2. intros. case H2. apply of_ctx_type to H1 H3. search. apply IH to H1 H3. case H5. search. apply type_ignores_of_ctx to H1 H3. apply IH to _ H4. search. %% Now we need to state the generalize theorem. This will require reasoning %% about all possible closed instantiations of an open term. % Suppose that {L |- of M A} is true. Then M is an open term with nominal % constants that are listed in L. The judgment "subst L M N" holds for all % instantiations N of the nominal constants in M with values that satisfy % the reduce relation for their respective types. The key to defining this % judgment is the use of nabla in the head of a definition which extracts % a nominal constant from L and M. The definition of subst then substitutes % for this nominal constant and continues processing the list L. Define subst nil M M. Define nabla x, subst (of x A :: L) (R x) M := exists V, reduce V A /\ {value V} /\ subst L (R V) M. % Subst on a closed term has no effect Theorem closed_subst : forall L M N, closed M -> subst L M N -> M = N. [Show Proof][Hide Proof] induction on 2. intros. case H2. search. apply prune_closed to H1. apply IH to H1 H5. search. Theorem subst_var : forall L M N A, of_ctx L -> member (of M A) L -> subst L M N -> reduce N A. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. case H3. apply reduce_closed to H6. apply closed_subst to H9 H8. search. case H3. apply member_fresh to H6 _. case H10. apply IH to H5 H6 H9. search. Theorem subst_app : forall L M N R, of_ctx L -> subst L (app M N) R -> exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. search. case H2. apply IH to H4 H7. search. % This theorem has a {type A} hypothesis to ensure that no nominal variables % can appear in A and thus substitutions do not affect A Theorem subst_abs : forall L M R A, of_ctx L -> subst L (abs A M) R -> {type A} -> exists MR, R = abs A MR /\ (forall V, reduce V A -> {value V} -> nabla x, subst (of x A :: L) (M x) (MR V)). [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. exists M. split. search. intros. search. case H2. apply prune_type to H3. apply IH to H5 H8 H3. exists MR. split. search. intros. apply prune_reduce to H10. apply H9 to H10 H11. case H12. search. Theorem subst_preserves_type : forall L M N A, of_ctx L -> subst L M N -> {L |- of M A} -> {of N A}. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. search. case H2. apply reduce_of to H6. inst H3 with n1 = V. cut H10 with H9. apply of_type to _ H3. apply prune_type to H12. apply IH to H5 H8 H11. search. Theorem weak_norm_ext : forall L M R A, of_ctx L -> {L |- of M A} -> subst L M R -> reduce R A. [Show Proof][Hide Proof] induction on 2. intros. case H2 (keep). apply subst_var to H1 H4 H3. search. apply subst_app to H1 H3. apply IH to H1 H4 H6. apply IH to H1 H5 H7. case H8. apply H12 to H9. search. apply type_ignores_of_ctx to H1 H4. apply subst_abs to H1 H3 H6. apply subst_preserves_type to H1 H3 H2. unfold. search. search. intros. % The rest is one single case apply reduce_halts to H9. case H10. apply reduce_steps_forward to H9 H11. apply H7 to H13 H12. apply IH to _ H5 H14. apply steps_app_value to _ H11 with M = abs A1 MR. apply steps_right to H16 _ with R = MR V. apply reduce_of to H9. apply reduce_steps_backward to H15 H17 _. search. Theorem weak_norm : forall M A, {of M A} -> halts M. [Show Proof][Hide Proof] intros. apply weak_norm_ext to _ H1 _. apply reduce_halts to H2. search.