User talk:Drl

From The Twelf Project

Jump to: navigation, search

Hello! I actually like the monospaced presentation better:

\texttt{even}(N) \over \texttt{even}(s \, (s \, N))

You've got admin rights, btw. — Rob (and his talk) 16:02, 23 October 2006 (EDT)


Contents

[edit] Sidebar

You might be interested in editing the sidebar. — Rob (and his talk) 16:51, 23 October 2006 (EDT)

[edit] Oh yeah

You did write one of those papers-about-twelf things, now didn't you? :-) — Rob (and his talk) 21:50, 20 March 2007 (EDT)

[edit] Aite

I'm showering, driving to school, and emailing! — Rob (and his talk) 09:18, 21 March 2007 (EDT)

[edit] Some small feature requests (didn't want to lose track of these completely)

  •  %reduces under a binder (comes up, e.g. in strengthening). When you know (forall x. A x < B), you could at least conclude A < B when x doesn't occur, which as I recall is enough for this example.
  • new emacs mode with karl's macros
  • for world violations, move some of the info that gets printed on higher chatter to the default, so it's easier to debug

[edit] Example (which Adam did much better slower than me)

tp : type.
unit : tp.
arrow : tp -> tp -> tp.

exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

of : exp -> tp -> type.
of/app : of (app E1 E2) T
        <- of E1 (arrow T2 T)
        <- of E2 T2.
of/lam : of (lam E) (arrow T2 T)
       <- {x : exp} of x T2 -> of (E x) T.

false : type.

%block ofb : some {T : tp} block {x : exp} {dx : of x T}.

id : tp -> tp -> type.
refl : id T T.

lemma : ({x} {dx : of x T} of x T')
      -> ({x} of x T -> of x (arrow T' T0)) 
      -> false
      -> type.
%mode lemma +X1 +X2 -X3.

%worlds (ofb) (lemma _ _ _).
%total {} (lemma _ _ _).

thm : of (lam [x] (app x x)) T -> false -> type.
%mode thm +X1 -X2.

- : thm (of/lam [x] [dx] (of/app (D x dx) (D' x dx))) XXX
  <- lemma D D' XXX. 

%worlds (ofb) (thm X Y).
%total {} (thm X Y).

[edit] Any var, not just the last one

tp : type.                                                                                                                                                                        ar : tp -> tp -> tp. %infix right 10 ar.                                                                                                                                          
b : tp.                                                                                                                                                                           
                                                                                                                                                                                  
exp : type.                                                                                                                                                                       
app : exp -> exp -> exp.                                                
lam : (exp -> exp) -> exp.                                                                                                                                                        
                                                                                                                                                                                  
of : exp -> tp -> type.                                                                                                                                                           
of_app : of E1 (T1 ar T2) -> of E2 T1 -> of (app E1 E2) T2.                                                                                                                       
of_lam : ({x}of x T1 -> of (E x) T2) -> of (lam E) (T1 ar T2).                                                                                                                    
                                                                                                                                                                                  
%block ofblock : some {T:tp} block {x:exp}{u: of x T}.                                                                                                                            
%worlds (ofblock) (of _ _).                                                                                                                                                       
                                                                                                                                                                                  
false : type.                                                                                                                                                                     
                                                                                                                                                                                  
isvar : exp -> type.                                                                                                                                                              
                                                                                                                                                                                  
                                                                                                                                                                                  
                                                                                                                                                                                  
%block varBlock : some {T:tp} block {x:exp}{u: of x T}{v:isvar x}.                                                                                                                
                                                                                                                                                                                  
contra : isvar X -> of X T1 -> of X (T1 ar T2) -> false -> type.                                                                                                                  
%mode contra +V +D1 +D2 -E.                                                                                                                                                       
%worlds (varBlock) (contra _ _ _ _).                                                                                                                                              
%total {E1 D1 D2} (contra E1 D1 D2 _).                                                                                                                                            
                                                                                                                                                                                  
boo : isvar X -> of (app X X) T -> false -> type.                                                                                                                                 
%mode boo +X +D -E.                                                                                                                                                               
boo_lam : boo X (of_app D1 D2) B                                                                                                                                                  
           <- contra X D2 D1 B.                                                                                                                                                                                                                                                                                                                                   
                                                                                                                                                                                  
%worlds (varBlock) (boo _ _ _).                                                                                                                                                   
%total {} (boo _ _ _).

[edit] Delphin Version by Adam

sig <tp : type> %name A t

   <ar : tp -> tp -> tp> %infix right 10                                                                                                                                         
    ;                                                                                                                                                                    
                                                                                                                                                                                 

sig <exp : type>

   <app : exp -> exp -> exp>                                                                                                                                                     
   <lam : (exp -> exp) -> exp>;                                                                                                                                                  
                                                                                                                                                                                 

sig <of : exp -> tp -> type>

   <of_app : of E1 (T1 ar T2) -> of E2 T1 -> of (app E1 E2) T2>                                                                                                                  
   <of_lam : ({x}of x T1 -> of (E x) T2) -> of (lam E) (T1 ar T2)>;                                                                                                              
                                                                                                                                                                                 

sig <false : type>;

sig <eq : tp -> tp -> type> -> of X (T1 ar T2) -> false -> type.

   <eqid : eq T1 T1>;                                                                                                                                                            
                                                                                                                                                                                 

params = <exp>, <of (E#) T>;


type contextProp = <x:exp#> -> <(of x T1)> -> <(of x T2)> -> <eq T1 T2>;


fun contraEq : <eq (T1 ar T2) T1> -> <false> = fn .;

fun impossible1 : contextProp -> <of (lam [x] app x x) T> -> <false>

  = fn C <of_lam ([x][d] of_app (D1 x d) (D2 x d))> =>                                                                                                                           
          (case {<x>}{<d:of x T1>} contraEq ((C with <x> <d> <d> => <eqid>) <x> <D1 x d> <D2 x d>)                                                                               
            of {<x>}{<d>}<bot> => <bot>);                                                                                                                                        
                                                                                           d                                                                                     
                                                                                                                                                                                 

fun impossibleGeneral : contextProp -> <x:exp#> -> <of (app x x) T> -> <false>

  = fn C <x> <of_app D1 D2> => contraEq (C <x> <D1> <D2>); 

</code>

Personal tools