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.
%% Correctness for LLambda subst predicate Define ctx nil nil. Define ctx (term X :: L1) (copy X X :: L2) := ctx L1 L2. Theorem ctx_lemma : forall L1 L2 T, ctx L1 L2 -> member (term T) L1 -> member (copy T T) L2. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. Theorem copy_id : forall L1 L2 T, ctx L1 L2 -> {L1 |- term T} -> {L2 |- copy T T}. [Show Proof][Hide Proof] induction on 2. intros. case H2. apply ctx_lemma to H1 H3. search. apply IH to H1 H3. apply IH to H1 H4. search. apply IH to _ H3. search. Define ctx2 nil. Define ctx2 (copy X X :: L) := ctx2 L. Theorem ctx2_eq : forall L T S, ctx2 L -> member (copy T S) L -> T = S. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. Theorem copy_eq : forall L T S, ctx2 L -> {L |- copy T S} -> T = S. [Show Proof][Hide Proof] induction on 2. intros. case H2. apply ctx2_eq to H1 H3. search. apply IH to H1 H3. apply IH to H1 H4. search. apply IH to _ H3. search. Theorem subst : forall R T S, {term T} -> {subst R T S} -> R T = S. [Show Proof][Hide Proof] intros. case H2. apply copy_id to _ H1. inst H3 with n1 = T. cut H5 with H4. apply copy_eq to _ H6. search.