User talk:Jcreed

From The Twelf Project
Jump to: navigation, search

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

Tom7's Twelf Mystery Du Jour

This is the thing that curiously didn't work:

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 _ _).

Modal encoding

% sorts
sort : type. %name sort S.
src : sort. % term from source language
rs : sort. % resource
fm : sort. % frame
wd : sort. % kripke modal world
sx : sort. % sequent


% terms
tm : sort -> type. %name tm X.
z : tm src.
s : tm src -> tm src.
/ : tm wd -> tm fm -> tm sx. %infix right 19 /.
* : tm wd -> tm wd -> tm wd. %infix right 21 *.
↝ : tm wd -> tm fm -> tm fm. %infix right 20 ↝.

% props
spos : type. %name spos P.
sneg : type. %name sneg N.

tpos : type. %name tpos TP.
tneg : type. %name tneg TN.

-o : spos -> sneg -> sneg.  %infix right 10 -o.
⊗ : spos -> spos -> spos.  %infix right 11 ⊗.
&  : sneg -> sneg -> sneg.  %infix right 11 &.
↑ : spos -> sneg.
◇ : spos -> sneg.
↓ : sneg -> spos.
□ : sneg -> spos.
atm+ : tm src -> spos.
atm- : tm src -> sneg.

⇒ : tpos -> tneg -> tneg.  %infix right 10 ⇒.
∧ : tpos -> tpos -> tpos.  %infix right 11 ∧.
∨ : tneg -> tneg -> tneg.  %infix right 10 ∨.
⇑ : tpos -> tneg.
∃ : (tm S -> tpos) -> tpos.
∀ : (tm S -> tneg) -> tneg.
⇓ : tneg -> tpos.
≤ : tm S -> tm S -> tpos. %infix right 8 ≤.
• : tm sx -> tneg.

%abbrev $ = [x] [y] • (x / y).
%infix right 19 $.

xlpn : spos -> (tm wd -> tneg) -> tneg -> type.
xlnn : sneg -> (tm fm -> tneg) -> tneg -> type.

xlpn/⊗ : xlpn (P1 ⊗ P2) K Z1
          <- ({a1} xlpn P2 ([a2] K (a1 * a2)) (Z2 a1))
          <- xlpn P1 ([a1] Z2 a1) Z1.

xlnn/-o : xlnn (P -o N) K Z1
          <- ({a} xlnn N ([f] K (a ↝ f)) (Z2 a))
          <- xlpn P ([a] Z2 a) Z1.

xlnn/↑ : xlnn (↑ P) K (∀ [f] ⇓ (Z f) ⇒ K f)
          <- {f} xlpn P ([a] a $ f) (Z f).

xlpn/↓ : xlpn (↓ N) K (∀ [a] ⇓ (Z a) ⇒ K a)
          <- {a} xlnn N ([f] a $ f) (Z a).

xlpp : spos -> tm wd -> tpos -> type.
xlnp : sneg -> tm fm -> tpos -> type.

xlpp/⊗ : xlpp (P1 ⊗ P2) A (∃ [a1] Z1 a1 ∧ ∃ [a2] Z2 a2 ∧ (a1 * a2 ≤ A))
          <- ({a1} xlpp P1 a1 (Z1 a1))
          <- ({a2} xlpp P2 a2 (Z1 a2)).

xlnp/-o : xlnp (P -o N) F (∃ [a] Z1 a ∧ ∃ [f] Z2 f ∧ (a ↝ f ≤ F))
          <- ({a} xlpp P a (Z1 a))
          <- ({f} xlnp N f (Z2 f)).

xlpn/↓ : xlpp (↓ N) A (⇓ (∀ [f] (Z f) ⇒ A $ f))
          <- {f} xlnp N f (Z f).

xlpn/↑ : xlnp (↑ P) F (⇓ (∀ [a] (Z a) ⇒ a $ F))
          <- {a} xlpp P a (Z a).

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

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)