Why fail apply?
Signature File
sig lc. kind tm,ty type. type c tm. type app tm -> tm -> tm. type abs (tm -> tm) -> tm. type top ty. type arrow ty -> ty -> ty. type ty ty -> o. type of tm -> ty -> o. type step tm -> tm -> o.
Module File
module lc. ty top. ty (arrow A B) :- ty A,ty B. of (app M N) B :- of M (arrow A B), of N A. of (abs R) (arrow A B) :- ty A,pi x\ (of x A => of (R x) B). of c A :- ty A. step (app M N) (app M' N ) :- step M M'. step (app M N) (app M N') :- step M N'. step (app (abs R) M) (R M). step (abs R) (abs R') :- pi x\ step (R x) (R' x).
I want to prove next Theorem
Welcome to Abella 1.3.4 Abella < Specification "lc". Reading specification lc Abella < Close tm,ty. Abella < Define sn : tm -> prop by sn M := forall N,{step M N} -> sn N. Abella < Theorem lamSN : forall F T,sn (F T) -> sn (abs F). ============================ forall F T, sn (F T) -> sn (abs F) lamSN < induction on 1. IH : forall F T, sn (F T) * -> sn (abs F) ============================ forall F T, sn (F T) @ -> sn (abs F) lamSN < intros. Variables: F, T IH : forall F T, sn (F T) * -> sn (abs F) H1 : sn (F T) @ ============================ sn (abs F) lamSN < case H1. Variables: F, T IH : forall F T, sn (F T) * -> sn (abs F) H2 : forall N, {step (F T) N} -> sn N * ============================ sn (abs F) lamSN < unfold. Variables: F, T IH : forall F T, sn (F T) * -> sn (abs F) H2 : forall N, {step (F T) N} -> sn N * ============================ forall N, {step (abs F) N} -> sn N lamSN < intros. Variables: F, T, N IH : forall F T, sn (F T) * -> sn (abs F) H2 : forall N, {step (F T) N} -> sn N * H3 : {step (abs F) N} ============================ sn N lamSN < case H3. Variables: F, T, N, R' IH : forall F T, sn (F T) * -> sn (abs F) H2 : forall N, {step (F T) N} -> sn N * H4 : {step (F n1) (R' n1)} ============================ sn (abs R') lamSN < inst H4 with n1 = T. Variables: F, T, N, R' IH : forall F T, sn (F T) * -> sn (abs F) H2 : forall N, {step (F T) N} -> sn N * H4 : {step (F n1) (R' n1)} H5 : {step (F T) (R' T)} ============================ sn (abs R') lamSN < apply H2 to H5. Variables: F, T, N, R' IH : forall F T, sn (F T) * -> sn (abs F) H2 : forall N, {step (F T) N} -> sn N * H4 : {step (F n1) (R' n1)} H5 : {step (F T) (R' T)} H6 : sn (R' T) * ============================ sn (abs R') lamSN < apply IH to H6. Error: Unify.UnifyError(0) %% Why?? Variables: F, T, N, R' IH : forall F T, sn (F T) * -> sn (abs F) H2 : forall N, {step (F T) N} -> sn N * H4 : {step (F n1) (R' n1)} H5 : {step (F T) (R' T)} H6 : sn (R' T) * ============================ sn (abs R')