[POPLmark] Submission

[jevgenijs@dva.lv]

Here attached submission for PoplMark challenges 1A, 2A 
with explicit (directly computable) evaluation relation 
and progress operator, so providing basis also for challenge 3
(without records).
Coq solution with de Bruijn nameless representation is based on 
previous submission of Jerome Vouillon with numerous simplifications.
The role of natural numbers clarified by providing interface 
(see module type T_Nat in sub_def.v) of all their properties used 
outside implementation module (no induction principles, additional 
recursion operators and even no order relation required).
This could help with modifications and translations to others representations.
Among most interesting findings there could be mentioned the usage of 
functions t_semi_P, t_semi_S and their properties t_semi_S_P, t_semi_S_2,
which allows removing case analysis on order relation for natural numbers.
Also some parts of paper proofs were simplified. 
For example lemmas on inversions of typing rules 
(T_Abs_inversion and T_Tabs_inversion) allows avoiding rather 
complicated reasoning for lemmas A.12, A.13, 
where existence of some types should be established by induction. 
All additional inductive definitions used in Jerome Vouillon's 
solution were removed, by introducing explicit operators. 
This results in somehow more lengthy proofs, but to my mind justified, 
since any inductive definitions with their properties are just extra 
assumptions (proven metatheoreticaly to be consistent).
It could became especially important for abstract solutions 
(which I am planning to work on), 
where we are explicitly indicate all required assumptions and 
any extra assumptions are diminishing quality of such solutions.
Evaluation relation (red) and reduction step (progr) are 
defined explicitly as Coq fixpoint operators, 
so basically providing solution for challenge 3 (without records).
One can easily extract them as Ocaml/Haskell programs or use 
'eval compute in' statement directly within Coq environment.
For the latest case slight modification of development required, 
since Coq canonic natural numbers are hidden within module M_T_Nat 
(see sub_def.v).
One can change opaque definition 'Module M_T_Nat:T_Nat' 
to transparent 'Module M_T_Nat<:T_Nat', 
but some proofs will also require changes since Coq will do more
automatic reductions for transparent definitions.
 
There could be also added verification of entered terms and verification 
programs extracted, similar to development of Bruno Barras for 
Calculus of Construction (see http://pauillac.inria.fr/~barras).  
Same development could be used as example of technique to translate 
name-carrying terms and to define their alpha-equivalence.  

In case there will be time (also need and response), 
I am planning to do something also with name-caring syntax, 
at least to show its correspondence with de Bruijn syntax and to provide 
explicit operators for alpha-equivalence 
(especially waiting for more details of Urban's and Tasson's approach 
(http://www.mathematik.uni-muenchen.de/~urban/nominal), possible will try to 
implement it with Coq).
Any cooperation is desirable; there is lot to do, but not having sufficient 
time.For immediate contribution one can try to improve implementation of module
M_T_Nat by exposing all used properties of natural numbers,
removing usage of omega and reducing compilation time 
(which now is too high, probably tactics used are proving same things many 
times). Suggestion for future work or comments are welcome.
Also, if there are some possibilities to host separate web site devoted 
to Coq solutions, I will be glad to contribute by either maintaining it or 
just by providing information.

Best Regards.
Jevgenijs Sallinens 
(PhD in mathematics, currently programmer) 
           



-------------------------------------------------
This mail sent through IMP: http://webmail.dva.lv/
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: compile.txt
Url: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050825/09db451c/compile-0001.txt
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: tactics.v
Url: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050825/09db451c/tactics-0001.ksh
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: sub_defs.v
Url: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050825/09db451c/sub_defs-0001.ksh
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: sub.v
Url: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050825/09db451c/sub-0001.ksh
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: typ_defs.v
Url: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050825/09db451c/typ_defs-0001.ksh
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: typ.v
Url: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050825/09db451c/typ-0001.ksh
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: red_defs.v
Url: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050825/09db451c/red_defs-0001.ksh
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: red.v
Url: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050825/09db451c/red-0001.ksh