[POPLmark] Poplmark Digest, Vol 10, Issue 5

Daniel C. Wang danwang at CS.Princeton.EDU
Thu Jun 1 21:44:32 EDT 2006


Ahh, you've read between the lines.... correctly. :)

1. There isn't a nice "nat" library I could just include.
2.

height_of_subst : ({x : tm} {dx : height x (s z)} height (E1 x) N1)
		   -> height E2 N2
		   -> height (E1 E2) NSubst
		   -> sum N1 N2 N12
		   -> lt NSubst N12
		   -> type.
%mode height_of_subst +X1 +X2 -X3 -X4 -X5.

is the Twelfized version of my challenge problem. It takes me a while to convince my self that's 
really the theorem I had in my head before I twelfized it.

Anyway, I want to thank everyone for putting in the effort to code this up. 
I think all the examples are really great at showing off the "basics" of each system. i.e.
reasoning about naturals, lambda terms, and basic induction on a relation. 

As I'm too old fashioned to know how to use a Wiki properly. I'd appreciate it if someone could put 
up links to all the solutions on the Wiki.


Dan Licata wrote:
> {stuff deleted}
> Daniel, you mentioned in a previous e-mail that there is a system in
> which you found this task "tedious".  Since you haven't made this
> complaint about the Coq/Isabelle/HOL solutions, I wonder if Twelf is the
> system you had in mind.  If so, I'm curious as to why.
>
> -Dan
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>   



More information about the Poplmark mailing list