Coq be an actual proof assist tool

Using Coq
1

I am forced to use Coq as its in my master’s degree. I don’t like it at all I thinks too rigid and its not assisting in proof its actually make them harder.

It might be a bit unfaire since I am a c purist that dislike fonctional programming and math in general but there is an issue wih coq.
Here are some suggestions:
-Add proof suggestions build into the language. It can be really hard to prove something getting a tip from something that can see paterns in proof would be great.
-Less rigidity. Sometimes proofs just won’t work because coq doesn’t like how you wrote them.

2

Add proof suggestions build into the language. It can be really hard to prove something getting a tip from something that can see paterns in proof would be great.

There are many tools to do proofs automatically, theory-specific solvers like lia, proof search tactics like auto, general purposed solvers, AI based solutions like Coq-copilot etc…
Yet, proving stuffs ain’t easy: Maths and formalized math / CS are both research fields and at every step many formalization choices are possible which influences how proof must be done. Further, as of yet, some basic design choices still don’t have a clear solution. So there can hardly be a universal and perfect solution. I guess some suggestions could be possible for very simple proofs but it is unclear to me how far such suggestions could go. For instance, tools like ChatGPT can generate proofs that look right, because well code generation, but are deeply logically wrong, even for basic stuffs.

This being said, if your teachers haven’t introduced any of them, then learning how to do rigorous proof on your own is most likely one of the objective of your course. Maybe, they will also be introduced later ?

-Less rigidity. Sometimes proofs just won’t work because coq doesn’t like how you wrote them.

Coq is very different from a language like C. They are not meant for the same purpose, and can’t do the same thing. Typically, you can’t use C to very maths the way Coq does. To actually be able to do that statically and to be safe, Coq needs to have a strict typing system to ensure that what you write actually corresponds to math, and that it makes sense. It is actually the whole point, you don’t need to compile and execute code like in C to find errors. Errors can be detected statically, and you can work interactively. So yes, you won’t have much as freedom as in C, but it is for a good reason.

Consequently, if a proof doesn’t work, it is most likely means your proof is false. It is much more likely that what you are trying to do does not corresponds to what you think and else fails, than that Coq has an error, though as for any softwares those can happen. If you have a particular MWE and an improvement suggestions, you can share it.

3

Learning Coq is challenging. It is still primarily a tool for research. It has many quirks, it should be easier to use and the documentation still needs considerable improvement. It has gotten better over time and I expect it will continue to do so. Keep in mind it is free software developed by volunteers.

Add proof suggestions build into the language. It can be really hard to prove something getting a tip from something that can see paterns in proof would be great.

I hope you understand that there’s no practical algorithm that can prove (or give useful hints for) every true theorem. Some theorems are very hard. That said, it should be possible to give useful hints in many cases, but so far no one has done the work to make that happen.

The Search command can help you find useful theorems (if you’re not already using it).

Sometimes proofs just won’t work because coq doesn’t like how you wrote them.

If you give concrete examples then we may be able to help you with specific points.

4

If writing or generating proofs is hard then the focus should be made on effective search for solutions among proved theorems.
And now there is not a bone in the truck.

sherlocoq didn’t get gathered enough interest and is not running now.

Even built-in search capabilities in Coq among loaded definitions (no tricky indexing is assumed) is very limited.
E.g.

  Theorem t1 : forall (a :: nat) (l : list nat), a :: l = [a] ++ l. Admitted.
  Theorem t2 : forall (a :: nat) (l : list nat), [a] ++ l = a :: l. Admitted.
  Search (_ :: _ = _ ++ _).

Search with the pattern above misses theorem t2 nonetheless it is symmetrical to t1.

Function search by a type signature cannot neglect order of arguments:

  Fixpoint f1 (l : list nat) (n : nat) : option nat.
  Fixpoint f2 (n : nat)  (l : list nat) : option nat.
  Search (list _ -> nat -> option _).

So f2 falls out from results.