User talk:Jcreed

From The Twelf Project

hi — Rob (and his talk) 00:43, 7 October 2006 (EDT)

[edit] Tom7's Twelf Mystery Du Jour

This is the thing that curiously didn't work:

ERROR: option 'name' deprecated or invalid

o : type.
k : o.

pred : o -> type.
pred2 : (o -> o) -> type.


pred2/ : {A:o -> o} pred2 A -> pred (A k).

lemma : pred k -> type.
%mode lemma +T.

- : lemma (pred2/ _ _).


%worlds () (lemma _).
%total D (lemma D).

This is the thing that finally worked:

bool : type.

o : type.
k : o.
l : o.
eq : o -> o -> type.
refl : eq X X.

pred : o -> type.
pred2 : (o -> o) -> type.

pred/k : bool -> pred k.
pred/l : pred l.
pred2/ : {A:o -> o} pred2 A -> pred (A k).

lemma : {A} pred A -> eq A k -> bool -> type.
%mode lemma +A +T +E -B.

 - : lemma _ (pred2/ _ _) _ true.

- : lemma k (pred/k B) EQ B.

%block bb : block {b : bool} {x:o}.
%worlds (bb) (lemma _ _ _ _).
%total D (lemma _ D _ _).

[edit] Looking at the equality proof

A simple test of looking at the equality proof and seeing that in each case it is refl:

look-at-eq : {A : o -> o} eq (A k) k -> type.
%mode look-at-eq +A +D.

- : look-at-eq ([x] x) refl.
- : look-at-eq ([x] k) refl.

%worlds () (look-at-eq _ _).
%total {} (look-at-eq _ _).

Does this show that you can do any decomposition you'd want to do? Drl 18 October 2007

[edit] A Copy Function

o : type.
eq : o -> o -> type.
refl : eq X X.
k : o.
l : o.

ho : (o -> o) -> type.

%block b : some {A : o -> o} block {x : ho A}.

src : o -> type.
dst : o -> type.

src/base : src X.
src/ho : ho A -> src (A k).

dst/base : dst k.
dst/ho : ho A -> dst k.

lemma :  src A -> eq A k -> dst k -> type.
- : lemma src/base EQ dst/base.
- : lemma (src/ho HO) EQ (dst/ho HO).

%mode lemma +S +E -D.
%worlds (b) (lemma _ _ _).
%total D (lemma D _ _ ).

copy :  src k -> dst k -> type.
- : copy A B <- lemma A refl B.

%mode copy +S -D.
%worlds (b) (copy _ _).
%total D (copy D _).

Jcreed 15:15, 18 October 2007 (EDT)