(*---- Prelude -------------------------------------------------------------*) [SET=Type] [TYPE=Type]; $[Target : {A|Type}A->Type] $[on : {A|Type}{a:A}Target a]; Label (!Target!) Target; Label (!Target on!) on; (*---- JM Equality ---------------------------------------------------------*) $[op== : {A,B|Type}A->B->Prop // JMr]; Configure Infix == right 2; $[JMr : {A|Type}{x:A}x == x]; $[JM_elim : {A|Type}{a:A}{P:{b:A}(a == b)->Type}(P a (JMr a))-> {b:A}{q:a == b}{tg:Target q}P b q]; [[A:Type][a,b:A][P:{b:A}(a == b)->Type][p:P a (JMr a)][tg:Target (JMr a)] JM_elim a P p a (JMr a) tg ==> p ]; Label (!JM!) op==; Label (!JM refl!) JMr; Label (!JM elim!) JM_elim; Goal JM_J : {A|Type}{a,b|A}{q:a == b}{tg:Target q} {Phi:A->Type}{phi:Phi a}Phi b; Elim (!JM elim!) q; intros; Immed; Save; Label (!JM J!) JM_J; Goal JM_Jsym : {A|Type}{b,a|A}{q:b == a}{tg:Target q} {Phi:A->Type}{phi:Phi a}Phi b; Elim (!JM elim!) q; intros; Immed; Save; Label (!JM Jsym!) JM_Jsym; Goal JM_K : {A|Type}{a|A}{q:a == a}{tg:Target q} {Phi:(a == a)->Type}{phi:Phi (JMr a)}Phi q; Elim (!JM elim!) q; intros; Immed; Save; Label (!JM K!) JM_K; (*---- Nat, Fin, Vectors ---------------------------------------------------*) Inductive [Nat : Type] Constructors [n0 : Nat] [nS : {n:Nat}Nat]; Inductive [Fin : Nat -> Type] Constructors [f0 : {n:Nat}Fin (nS n)] [fS : {n|Nat}{i:Fin n}Fin (nS n)]; [op&v [A:Type][n:Nat] = (Fin n) -> A : Type ]; Configure Infix &v left 4; [vHd [A|Type][n|Nat][xs:A &v (nS n)] = xs (f0 n) : A ]; [vTl [A|Type][n|Nat][xs:A &v (nS n)] = [i:Fin n]xs (fS i) : A &v n ]; $[vNil : {A:Type}A &v n0]; $[vCons : {A|Type}{n|Nat}{x:A}{xs:A &v n}(A &v (nS n))]; [[A|Type][n|Nat][x:A][xs:A &v n][i:Fin n] vCons x xs f0 ==> x || vCons x xs (fS i) ==> xs i ]; [op&c [A|Type][a:A][n:Nat] = [i:Fin n]a : A &v n ]; Configure Infix &c left 5; [op&a [A,B|Type][n|Nat][fs:(A -> B) &v n][xs:A &v n] = [i:Fin n]fs i (xs i) : B &v n ]; Configure Infix &a left 4; (*---- Kind, Var -----------------------------------------------------------*) Inductive [Kind : Type] Constructors [STAR : Kind] [op>> : {S,T:Kind}Kind]; Configure Infix >> right 3; [Sig = Kind]; Inductive [Var : Sig -> Kind -> Type] Constructors [v0 : {K:Kind}{S:Sig}Var (K >> S) K] [vS : {J,K|Kind}{S|Sig}{v:Var S K}Var (J >> S) K]; (*---- Ty ------------------------------------------------------------------*) [Del,Lam ? Sig]; Inductive [Ty : Kind -> Type] Constructors [D : {K|Kind}{v:Var Del K}Ty K] [V : {K|Kind}{v:Var Lam K}Ty K] [op/ : {J,K|Kind}{F:Ty (J >> K)}{X:Ty J}Ty K] [Zero,One : Ty STAR] [op+,op* : {S,T:Ty STAR}Ty STAR]; Configure Infix + right 4; Configure Infix * right 5; Configure Infix / left 6; Discharge Lam; [TY = Ty STAR]; (*---- Args, Subst ---------------------------------------------------------*) [Args [K:Kind] = {J|Kind}(Var K J) -> TY J : Type ]; [aHd [J,K|Kind][Xs:Args (J >> K)] = Xs v0 : TY J ]; [aTl [J,K|Kind][Xs:Args (J >> K)] = [L|Kind][v:Var K L]Xs (vS v) : Args K ]; $[aNil : Args STAR]; $[aCons : {J,K|Kind}{X:TY J}{Xs:Args K}Args (J >> K)]; [[J,K,L|Kind][X:TY J][Xs:Args K][v:Var K L] aCons X Xs v0 ==> X || aCons X Xs (vS v) ==> Xs v ]; $[op@a : {K|Kind}{X:TY K}{Ys:Args K}TY STAR]; Configure Infix @a left 6; [[J,K|Kind][X:TY STAR][Ys0:Args STAR][F:TY (J >> K)][YsS:Args (J >> K)] op@a|STAR X Ys0 ==> X || op@a|(J >> K) F YsS ==> F / aHd YsS @a aTl YsS ]; $[op<< : {L,K|Kind}(Ty L K) -> (Args L) -> TY K]; Configure Infix << left 1; [[J,K,L|Kind][v:Var L K][d:Var Del K][Ys:Args L] [F:Ty L (J >> K)][X:Ty L J] [S,T:Ty L STAR] V v << Ys ==> Ys v || D L d << Ys ==> D STAR d || F / X << Ys ==> (F << Ys) / (X << Ys) || Zero L << Ys ==> Zero STAR || One L << Ys ==> One STAR || S + T << Ys ==> (S << Ys) + (T << Ys) || S * T << Ys ==> (S << Ys) * (T << Ys) ]; (*---- Env, Data -----------------------------------------------------------*) [Env = {K|Kind}(Var Del K) -> (Ty K STAR)]; [del ? Env]; Inductive [Data : {T:TY STAR}Type] Constructors [con : {K|Kind}{Xs|Args K}{d:Var Del K} {t:Data (del d << Xs)}Data (D STAR d @a Xs)] [inl : {S,T|TY STAR}{s:Data S}Data (S + T)] [inr : {S,T|TY STAR}{t:Data T}Data (S + T)] [void : Data One] [pair : {S,T|TY STAR}{s:Data S}{t:Data T}Data (S * T)]; (*---- UFold, UFolds -------------------------------------------------------*) [n|Nat] [Phi : (TY STAR &v (nS n)) -> Type]; $[UFolds : {K|Kind}(Args K &v nS n)->Type // del Phi]; [UFold [K|Kind][Xs:TY K &v nS n] = {Yss|Args K &v nS n}[Yss'=[i:Fin (nS n)][J|Kind][v:Var K J]Yss i v] (UFolds Yss') -> (Data (vHd Xs @a vHd Yss')) -> Phi ((op@a|K) &c nS n &a Xs &a Yss') : Type ]; [[J,K|Kind][Yss0:Args STAR &v nS n][Yss1:Args (J >> K) &v nS n] UFolds|STAR Yss0 ==> Prop || UFolds|(J >> K) Yss1 ==> (UFold|J ((aHd|J|K) &c nS n &a Yss1)) # (UFolds|K ((aTl|J|K) &c nS n &a Yss1)) ]; [Tr [n|Nat][K|Kind][Xss:Args K &v n] = [J|Kind][v:Var K J][i:Fin n]Xss i v : {J|Kind}(Var K J) -> (TY J &v n) ]; $[UFproj : {K,J|Kind}{Yss|Args K &v nS n} {fs:UFolds Yss}{v:Var K J} UFold (Tr Yss v)]; [[J,K,L|Kind][Yss|Args (K >> L) &v nS n][fs:UFolds Yss] [v:Var L J] UFproj fs v0 ==> fs.1 || UFproj fs (vS v) ==> UFproj (fs.2) v ]; (*---- ufold ---------------------------------------------------------------*) [doCon : {K|Kind}{d:Var Del K}{Wss|Args K &v nS n} (Phi (op<< (del d) &c nS n &a Wss)) -> Phi (op@a (D STAR d) &c nS n &a Wss)]; [doInl : {Ss,Ts|TY STAR &v nS n} (Phi Ss) -> Phi ((op+|STAR) &c nS n &a Ss &a Ts)]; [doInr : {Ss,Ts|TY STAR &v nS n} (Phi Ts) -> Phi ((op+|STAR) &c nS n &a Ss &a Ts)]; [doVoid : Phi (One STAR &c nS n)]; [doPair : {Ss,Ts|TY STAR &v nS n} (Phi Ss) -> (Phi Ts) -> Phi ((op*|STAR) &c nS n &a Ss &a Ts)]; $[ufoldBody : {L|Kind}{Wss|Args L &v nS n}{wfs:UFolds Wss} {K|Kind}{X:Ty L K} UFold (op<< X &c nS n &a Wss) // doCon doInl doInr doVoid doPair]; (* ufoldBody : {L|Kind}{Wss|Args L &v nS n}{wfs:UFolds Wss} {K|Kind}{X:Ty L K} {Yss|Args K &v nS n}[Yss'=[i:Fin (nS n)][J|Kind][v:Var K J]Yss i v] {yfs:UFolds Yss'} (Data ((X << vHd Wss) @a vHd Yss')) -> Phi ((op@a|K &c nS n) &a (op<< X &c nS n &a Wss) &a Yss') *) [[J,K,L|Kind][Wss|Args L &v nS n][wfs:UFolds Wss] [Yss|Args K &v nS n] [yfs:[Yss'=[i:Fin (nS n)][J|Kind][v:Var K J]Yss i v]UFolds Yss'] [v:Var L K] [tV:[Yss'=[i:Fin (nS n)][J|Kind][v:Var K J]Yss i v] Data (vHd Wss v @a vHd Yss')] [F:Ty L (J >> K)][X:Ty L J] [tA:[Yss'=[i:Fin (nS n)][J|Kind][v:Var K J]Yss i v] Data ((F << vHd Wss) / (X << vHd Wss) @a vHd Yss')] [d:Var Del K] [tD:[Yss'=[i:Fin (nS n)][J|Kind][v:Var K J]Yss i v] Data (del d << vHd Yss')] [S,T:Ty L STAR] [tS:Data (S << vHd Wss)] [tT:Data (T << vHd Wss)] [Ys0|Args STAR &v nS n] [fs0:[Ys0'=[i:Fin (nS n)][J|Kind][v:Var STAR J]Ys0 i v]UFolds Ys0'] ufoldBody wfs (V v) yfs tV ==> UFproj wfs v yfs tV || ufoldBody wfs (F / X) yfs tA ==> [Yss'=[i:Fin (nS n)][J|Kind][v:Var K J]Yss i v] ufoldBody wfs F|([i:Fin (nS n)]aCons (X << Wss i) (Yss' i)) (ufoldBody wfs X,yfs) tA || ufoldBody wfs (D L d) yfs (con d tD) ==> doCon d (ufoldBody yfs (del d)|(aNil &c nS n) ({P:Prop}P->P) tD) || ufoldBody wfs (S + T) fs0 (inl tS) ==> doInl|?|(op<< T &c ? &a Wss) (ufoldBody wfs S fs0 tS) || ufoldBody wfs (S + T) fs0 (inr tT) ==> doInr|(op<< S &c ? &a Wss) (ufoldBody wfs T fs0 tT) || ufoldBody wfs (One L) fs0 void ==> doVoid || ufoldBody wfs (S * T) fs0 (pair tS tT) ==> doPair (ufoldBody wfs S fs0 tS) (ufoldBody wfs T fs0 tT) ]; $[idLemma : {K|Kind}{X:TY K}(X << aNil) == X]; [[J,K|Kind][d:Var Del K] [F:TY (J >> K)][X:TY J][S,T:TY STAR] idLemma (D STAR d) ==> JMr (D STAR d) || idLemma (F / X) ==> JM_J ? (on (idLemma F)) ([F':TY (J >> K)]((F << aNil) / (X << aNil)) == F' / X) (JM_J ? (on (idLemma X)) ([X':TY J]((F << aNil) / (X << aNil)) == (F << aNil) / X') JMr) || idLemma (Zero STAR) ==> JMr (Zero STAR) || idLemma (One STAR) ==> JMr (One STAR) || idLemma (S + T) ==> JM_J ? (on (idLemma S)) ([S':TY STAR]((S << aNil) + (T << aNil)) == S' + T) (JM_J ? (on (idLemma T)) ([T':TY STAR]((S << aNil) + (T << aNil)) == (S << aNil) + T') JMr) || idLemma (S * T) ==> JM_J ? (on (idLemma S)) ([S':TY STAR]((S << aNil) * (T << aNil)) == S' * T) (JM_J ? (on (idLemma T)) ([T':TY STAR]((S << aNil) * (T << aNil)) == (S << aNil) * T') JMr) ]; [ufold [K|Kind][X:TY K] = JM_J ? (on (idLemma X)) ([X:TY K]UFold (X &c nS n)) (ufoldBody|STAR|(aNil &c nS n) ({P:Prop}P->P) X) ]; (*---- Fold, fold ----------------------------------------------------------*) $[Fold : {K|Kind}{X:TY K &v nS n}Type // del Phi]; [[Ts : TY STAR &v nS n] [J,K|Kind][Fs : TY (J >> K) &v nS n] Fold|STAR Ts ==> (Data (vHd Ts)) -> Phi ([i:Fin (nS n)]Ts i) || Fold|(J >> K) Fs ==> {Xs|TY J &v nS n} (Fold ([i:Fin (nS n)]Xs i)) -> Fold ((op/|STAR|J|K) &c nS n &a Fs &a Xs) ]; $[curry : {K|Kind}{Xs|TY K &v nS n}(UFold Xs)->Fold Xs]; $[uncurry : {K|Kind}{Xs|TY K &v nS n}(Fold Xs)->UFold Xs]; [[J,K|Kind] [Ts|TY STAR &v nS n][uTs:UFold Ts] [Fs|TY (J >> K) &v nS n][uFs:UFold Fs] curry|STAR uTs ==> uTs|(aNil &c nS n) ({P:Prop}P->P) || curry|(J >> K) uFs ==> [Xs|TY J &v nS n][fXs:Fold ([i:Fin (nS n)]Xs i)] curry|K|((op/|STAR|J|K &c nS n) &a Fs &a Xs) ([Yss|Args K &v nS n] [usYss:UFolds ([i:Fin (nS n)][J|Kind][v:Var K J]Yss i v)] uFs|([i:Fin (nS n)]aCons (Xs i) (Yss i)) (uncurry fXs,usYss)) ]; [[J,K|Kind] [Ts|TY STAR &v nS n][fTs:Fold Ts][Ys0:Args STAR &v nS n][usYs0:UFolds Ys0] [Fs|TY (J >> K) &v nS n][fFs:Fold Fs] [Yss:Args (J >> K) &v nS n][usYss:UFolds Yss] uncurry|STAR fTs|Ys0 usYs0 ==> fTs || uncurry|(J >> K) fFs usYss ==> uncurry|K (fFs|([i:Fin (nS n)]Yss i (v0 J K)) (curry usYss.1)) |([i:Fin (nS n)]aTl (Yss i)) usYss.2 ]; [fold [K|Kind][X:TY K] = curry (ufold X) : Fold (X &c nS n) ]; Discharge n; (*---- Some generic operations ---------------------------------------------*) [Bool = One STAR + One STAR : TY STAR]; [True = inl|?|One void : Data Bool]; [False = inr|One void : Data Bool]; [PhiEq [Ts : TY STAR &v nS n0] = (Data (vHd Ts)) -> Data Bool : Type ]; $[conEq : {K|Kind}{d:Var Del K}{Wss|Args K &v nS n0} (PhiEq ((op<< (del d) &c nS n0) &a Wss))-> PhiEq ((op@a (D STAR d) &c nS n0) &a Wss)]; [[K|Kind][d:Var Del K][Wss|Args K &v nS n0] [phi:PhiEq ((op<< (del d) &c nS n0) &a Wss)] [t:Data (del d << vHd Wss)] conEq d phi (con d t) ==> phi t ]; $[inlEq : {Ss,Ts|TY STAR &v nS n0}(PhiEq Ss)-> PhiEq ((op+|STAR &c nS n0) &a Ss &a Ts)]; [[Ss,Ts|TY STAR &v nS n0][phi:PhiEq Ss][s:Data (vHd Ss)][t:Data (vHd Ts)] inlEq|Ss|Ts phi (inl s) ==> phi s || inlEq|Ss|Ts phi (inr t) ==> False ]; $[inrEq : {Ss,Ts|TY STAR &v nS n0}(PhiEq Ts)-> PhiEq ((op+|STAR &c nS n0) &a Ss &a Ts)]; [[Ss,Ts|TY STAR &v nS n0][phi:PhiEq Ts][s:Data (vHd Ss)][t:Data (vHd Ts)] inrEq|Ss|Ts phi (inl s) ==> False || inrEq|Ss|Ts phi (inr t) ==> phi t ]; [voidEq = [_:Data One]True : PhiEq (One STAR &c nS n0) ]; $[and : {p,q:Data Bool}Data Bool]; [[b:Data Bool] and (inl|?|One void) b ==> b || and (inr|One void) b ==> False ]; $[pairEq : {Ss,Ts|TY STAR &v nS n0}(PhiEq Ss)->(PhiEq Ts)-> PhiEq ((op*|STAR &c nS n0) &a Ss &a Ts)]; [[Ss,Ts|TY STAR &v nS n0][phis:PhiEq Ss][phit:PhiEq Ts] [s:Data (vHd Ss)][t:Data (vHd Ts)] pairEq|Ss|Ts phis phit (pair s t) ==> and (phis s) (phit t) ]; [eq = fold PhiEq conEq inlEq inrEq voidEq pairEq]; [PhiMap [Ts : TY STAR &v nS (nS n0)] = Data (vHd (vTl Ts)) : Type ]; [conMap [K|Kind][d:Var Del K][Wss|Args K &v nS (nS n0)] [t:Data (del d << (vHd (vTl Wss)))] = con d t : Data (D STAR d @a (vHd (vTl Wss))) ]; [inlMap [Ss,Ts|TY STAR &v nS (nS n0)] = inl|(vHd (vTl Ss))|(vHd (vTl Ts)) ]; [inrMap [Ss,Ts|TY STAR &v nS (nS n0)] = inr|(vHd (vTl Ss))|(vHd (vTl Ts)) ]; [pairMap [Ss,Ts|TY STAR &v nS (nS n0)] = pair|(vHd (vTl Ss))|(vHd (vTl Ts)) ]; [map = fold PhiMap conMap inlMap inrMap void pairMap]; Discharge Del; (*---- Examples ------------------------------------------------------------*) [myDel = STAR >> (* Nat *) (STAR >> STAR) >> (* List *) STAR]; [myNat [L:Sig] = D|myDel L v0 : Ty myDel L STAR]; [myList [L:Sig] = D|myDel L (vS v0) : Ty myDel L (STAR >> STAR)]; $[mydel : Env myDel]; [ || mydel v0 ==> One ? STAR + myNat STAR || mydel (vS v0) ==> (One myDel (STAR >> STAR) + V ? v0 * myList / V ? v0 : Ty myDel (STAR >> STAR) STAR) ]; Goal my0 : Data mydel myNat; Refine con v0; Refine aNil; Refine inl; Refine void; Save; Goal myS : (Data mydel myNat) -> Data mydel myNat; intros n; Refine con v0; Refine aNil; Refine inr; Refine n; Save; Goal myNil : {X|TY myDel STAR}Data mydel (myList / X); intros X; Refine con|?|?|?|(aCons X aNil) (vS v0); Refine inl; Refine void; Save; Goal myCons : {X|TY myDel STAR}{x:Data mydel X}{xs:Data mydel (myList / X)} Data mydel (myList / X); intros X x xs; Refine con|?|?|?|(aCons X aNil) (vS v0); Refine inr; Refine pair; Refine x; Refine xs; Save; [XXX = map mydel (myList STAR) |(vCons (myNat STAR) (vCons (myNat STAR) (vNil (Ty myDel STAR STAR)))) myS (myCons my0 (myCons (myS my0) (myNil|(myNat STAR)))) ]; [YYY = myCons (myS my0) (myCons (myS (myS my0)) myNil)]; [BBB = eq mydel (myList STAR)|(vCons (myNat STAR) (vNil (Ty myDel STAR STAR))) (eq mydel (myNat STAR)) XXX YYY]; (Normal BBB);