sig subst. kind tm type. type app tm -> tm -> tm. type abs (tm -> tm) -> tm. type term tm -> o. type copy tm -> tm -> o. type subst (tm -> tm) -> tm -> tm -> o.
module subst. term (app M N) :- term M, term N. term (abs R) :- pi x\ term x => term (R x). copy (app N M) (app P Q) :- copy N P, copy M Q. copy (abs R) (abs S) :- pi x\ copy x x => copy (R x) (S x). subst R T S :- pi x\ copy x T => copy (R x) S.
Click on a command or tactic to see a detailed view of its use.
Specification "subst". Define ctx : olist -> olist -> prop by ctx nil nil ; ctx (term X :: L) (copy X X :: K) := ctx L K. Theorem ctx_member1 : forall L K E, ctx L K -> member E L -> exists T, E = term T /\ member (copy T T) K. Theorem ctx_member2 : forall L K E, ctx L K -> member E K -> exists T, E = copy T T. Theorem copy_id : forall L K T, ctx L K -> {L |- term T} -> {K |- copy T T}.induction on 2. intros. case H2. apply IH to H1 H3. apply IH to H1 H4. search. apply IH to _ H3. search. apply ctx_member1 to H1 H4. case H3. search.Theorem copy_eq : forall L K T S, ctx L K -> {K |- copy T S} -> T = S.induction on 2. intros. case H2. apply IH to H1 H3. apply IH to H1 H4. search. apply IH to _ H3. search. apply ctx_member2 to H1 H4. case H3. search.Theorem subst : forall R T S, {term T} -> {subst R T S} -> R T = S.