Abella logo (small)

cascade.thm

%% Arbitrary cascading substitutions on untyped lambda terms %% %% Nabla in the head of the definition of subst allows us to actively %% manipulate the context of a term in order to make an arbitrary %% number of substitutions for the nominal constants in the term. %% Here we prove that this form of substitution acts compositionally. Kind tm type. Type app tm -> tm -> tm. Type abs (tm -> tm) -> tm. Type pair tm -> tm -> o. Define subst : olist -> tm -> tm -> prop by subst nil T T ; nabla x, subst (pair x K :: L) (T x) S := subst L (T K) S. Theorem subst_app : forall L T R S, subst L (app T R) S -> exists U V, S = app U V /\ subst L T U /\ subst L R V. induction on 1. intros. case H1. search. apply IH to H2. search. Theorem subst_abs : forall L T R, subst L (abs T) R -> exists S, R = abs S /\ nabla z, subst L (T z) (S z). induction on 1. intros. case H1. search. apply IH to H2. search.