sig fcurry. %%% fcurry.sig
kind tm, ty type.
type arr ty -> ty -> ty.
type all (ty -> ty) -> ty.
type app tm -> tm -> tm.
type abs (tm -> tm) -> tm.
type ins ty -> ty -> o.
type ins* ty -> ty -> o.
type of tm -> ty -> o.
type step tm -> tm -> o.
type steps tm -> tm -> o.
module fcurry. %%% fcurry.mod
of (app M N) T :- of M (arr U T), of N U.
of (abs R) (arr T U) :- pi x\ (of x T => of (R x) U).
of N (all T) :- pi a\ of N (T a).
of N (T U) :- of N (all T).
ins (all T) (T U).
ins* T T.
ins* T S :- ins T U, ins* U S.
step (app M N) (app M' N) :- step M M'.
step (app M N) (app M N') :- step N N'.
step (abs R) (abs R') :- pi x\ step (R x) (R' x).
step (app (abs R) N) (R N).
steps M M.
steps M N :- step M M', steps M' N.
Click on a command or tactic to see a detailed view of its use.
%% %% Contributed by Ahn Ki YungSpecification "fcurry". Close ty, tm. Theorem member_prune : forall L E, nabla (x : tm), member (E x) L -> exists F, E = x\ F. % Q.E.D. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Define ctx : olist -> prop by ctx nil ; nabla x, ctx (of x T :: L) := ctx L. Define name : tm -> prop by nabla x, name x. Theorem of_name : forall L E, ctx L -> member E L -> exists X T, E = of X T /\ name X. % Proof: induction on 1. intros. case H1. case H2. case H2. search. apply member_prune to H4. apply IH to H3 H4. search.% Q.E.D. Theorem ctx_uniq : forall L E T1 T2, ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2.% Proof: induction on 1. intros. case H1. case H2. case H2. case H3. search. apply member_prune to H5. case H3. apply member_prune to H5. apply IH to H4 H5 H6. search.% Q.E.D. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Theorem abs_ins_arr : forall L R N U T S, ctx L -> {L |- of (abs R) S} -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}.% Proof: induction on 2. intros. case H2. % Subgoal 1 case H3. inst H5 with n1 = N. cut H6 with H4. search. % 1.1 case H6. apply of_name to _ H9. case H8. % 1.2 apply of_name to _ H7. case H6. % 1.3 % Subgoal 2 case H3. case H6. % 2.1 inst H5 with n1 = U2. apply IH to _ H8 H7 H4. search. % 2.1.1 apply of_name to _ H9. case H8. % 2.1.2 apply of_name to _ H7. case H6. % 2.2 % Subgoal 3 assert {L |- ins* (all T1) (arr U T)}. apply IH to _ H5 H6 H4. search. % Subgoal 4 apply of_name to _ H6. case H5. case H7.% Q.E.D. Theorem abs_arr : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}.% Proof: induction on 2. intros. case H2. % Subgoal 1 inst H4 with n1 = N. cut H5 with H3. search. % Subgoal 2 (abs_ins*_arr lemma used) case H4. % Subgoal 2.1 assert {L |- ins* (all (z1\arr (T2 z1) (T3 z1))) (arr (T2 U1) (T3 U1))}. apply abs_ins_arr to _ H5 H6 H3. search. % Subgoal 2.2 assert {L |- ins* (all (z1\z1)) (arr U T)}. apply abs_ins_arr to _ H5 H6 H3. search. % Subgoal 3 apply of_name to _ H5. case H6. case H4.% Q.E.D. Theorem step_preserves_of : forall L M N T, ctx L -> {L |- of M T} -> {step M N} -> {L |- of N T}.% Proof: induction on 2. intros. case H2. case H3. % Subgoal 1 apply IH to _ H4 H6. search. % 1.1 apply IH to _ H5 H6. search. % 1.2 apply abs_arr to _ H4 H5. search. % 1.3 (abs_arr lemma used) % Subgoal 2 case H3. apply IH to _ H4 H5. search. % Subgoal 3 apply IH to _ H4 H3. search. % Subgoal 4 apply IH to _ H4 H3. search. % Subgoal 5 apply of_name to _ H5. case H4. case H3. case H6. case H6. case H6. case H6.% Q.E.D.