Can I achieve some specific project with Coq?

Using Coq
1

Hi, I am a ~50 years old teacher in Computer Science; I have encountered references to Coq for many years without taking the time to investigate more about it yet. I am much into functional programming and curious about learning new languages/systems.

However I have a very specific project in mind and I would like if learning Coq for it would be the best choice.

I am expecting to teach some short initiation-level parts of lambda calculus in about one year, and I would like to use the months to come for writing tools I could use for illustrating various things in lambda calculus.

I am perfectly aware that very good interpreters exist, and I actually compiled some of them, but I enjoy programming and I would like to have my own project anyway.

Currently, I have two different ideas in mind:

  • writing my own interpreter (in some language I already know) which would exactly fit my requirements;
  • learning Coq and implementing my “examples” and “manipulations” with it.

My requirements are not big: encoding integers in the lambda calculus with several conventions, using the Y combinator, etc. One specific requirement would be to be able to use shortcuts when displaying expressions (“Since we agree to encode the integer 3 in such or such manner, we will display “3” from now on rather than the full lambda expression”, "From now on, I will write “I” rather than “\x.x”, etc.).

I know that Coq is a proof assistant, and I must admit that I am not much concerned (yet?) with the “proof” part; I am rather looking for a tool I could use in front of the student for illustrating basic manipulations. Thus maybe Coq is not the tool I need.

What I am expecting for answers to the current question would be something like:

  • really, while doing what you are looking for could (maybe, probably, surely) be achievable, you will not really focus on the most interesting aspects of Coq by using it that way; if you can do what you want by yourself in some other way, you should probably keep Coq for something else later;
  • well, main purpose of Coq is not really what you are asking, and some other tools could certainly be some better first choice, but since you said you like learning things, and since Coq can perfectly do it, it would be a great idea trying to do it with Coq!
  • doing what you want is very easy with Coq, you should really give it a try!

Thank you by advance,

best regards,

a.

1 Like
2

Not only what you want to do seems quite achievable using Coq (a lot of programming language researchers are, after all, formalizing extensions of lambda-calculus using Coq), but by choosing it, you can take advantage of the very powerful notation system that Coq provides (including the number notation system). See https://coq.inria.fr/refman/user-extensions/syntax-extensions.html and in particular https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#numbers-and-strings.

Others than me can probably elaborate on both tips for encoding lambda calculus in Coq and tips for using the notation system.

3

IMO this highly depends on how much evaluation you want to do. Because Coq functions must be total and terminating, it is not possible to define an interpreter for untyped lambda calculus inside Coq.
(something that does finite amounts of small steps would be fine though)

4

I understand about the terminating requirement. What I have currently in mind should be one step at a time however: I want to transform expressions in front of the students. In the other hand, I should be able to choose the evaluation strategy at each step.

5

i think on the contrary you would actually be using the proof mode quite from the beginning. Because once you will have define terms and the reduction relation you will want to show them in action. And using tactics on a goal is imho the best way. So you will probably not only do (simple) proofs like « t reduces to t’ with this strategy » but you will most likely define your own tactics.

Defining your own tool may be very enjoyable too. But writing you own notation system and proof mode is great piece of work.