• Coq Overview
• Isabelle Overview
• Editors and Environments
• Readability of Proofs
• Automation and Tools
  • Term simplification
  • Manual search for relevant lemmas
  • Automagically find proofs
  • More

• internals
  • calculus of inductive constructions (TODO..)
  • focus on backward reasoning
• pro
  • proof structure is solid
  • more explicit handling of subgoals (less confusing)
  • more supported IDEs
• contra
  • weaker automation tools
  • quickly becomes tedious when large formulas need to be reformed
  • primarily designed for constructive proofs, needs to be extended to include some widely accepted standards
    • excluded middle: $A ∨ ¬A = True$
    • proof by contradiction
  • theory files (.v) need to be compiled to import them
    • recompile necessary after Coq version update

• internals
  • the minimalist kernel supports only natural deduction (see also talk:isa_intro)
    • small means less room for errors in specification and implementation
    • natural deduction axioms are the "assembly" of Isabelle
      • strategies/tactics submit calls to modify kernel state
  • focus on forward-reasoning using Isabelle/Isar
• pro
  • strong automation, powerful tools
    • more compact proof scripts
    • simple goals are simple to prove
    • sledgehammer
  • comparatively simple to use
• contra
  • confusing goal structure and application rules
  • automation sometimes leads to large leaps in reasoning, missing details
    • proofs are harder to follow
  • lack of good inspection tools (view step-by-step results from automatic solver)
  • lack of unified search/print tools
  • lack of concise documentation
    • everything in paper structure
    • searching terms in isar-ref.pdf is tedious and sometimes inconclusive as examples are rare and in most cases very abstract

The language of Coq with the solvers of Isabelle would be an ideal combination.

Both proof assistants include IDEs in their default distributions (CoqIde and Isabelle/jEdit), however, those are not the most modern or streamlined. The benefit of a pre-configured IDE is that it just works™ and does not have to be fiddled around with to get it to work properly.

Coq provides a web interface (jsCoq) and the VSCode plugin (VSCoq) works fairly well (comparable with the functionality of CoqIde, but with all the added benefits of VSCode).

TODO test jsCoq with a bigger example

TODO emacs & proof general?

TODO overlap with simplification => merge?

TODO Isabelle/auto2, as referenced in this answer

Isabelle provides the Isabelle/Isar language extension (the recommended way to write proofs [citation needed]), which enables proofs that state intermediate results instead of just tactics for the proof assistant.

A proof translator to natural language (English and French) contributed by Yann Coscoy could be used to write in a readable manner the proof terms that had been constructed by the tactics. This was an important advantage against competitor proof systems that did not construct explicit proofs, since it allowed auditing of the formal certifications.

TODO find the proof translator

for improved readability of .v files one might use a tool like Coqatoo

TODO get coqatoo to work (i have not managed to get it to generate output so far)

TODO overlap with readability => merge?

Isabelle provides a host of tactics like simp and auto to automatically apply fitting lemmas and perform rewrites. Coq provides similarly named tactics simpl and auto (as well variations of both), which are however not as powerful as their Isabelle counterparts and are only able to solve trivial problems.

For arithmetic terms, the Coq tactics ring_simplify (simplify using the properties of a (semi-)ring: associativity, commutativity for addition, distributivity) and ring (similar, tries to solve the current goal), as well as their field counterparts, can be used, but lack extensibility and integration with more powerful tactics compared to Isabelle. Note that over the naturals and integers, division has to be handled manually, as field is not applicable and ring is not capable of processing division. (see the Coq documentation on ring and field). A more powerful option is lia (linear integer arithmetic), a part of the micromega solver package that is to replace the older strategies omega and romega (see GitHub issues #7872 and #7878).

The process of applying automatic solvers is by default not very transparent and can quickly become a guessing game of which tactic will work with which arguments, which in turn leads to a lack of understanding of what is going on behind the scenes. Isabelle has a higher risk of becoming like this, as the automation tools are more powerful. Both proof assistants have solutions for this issue: in Isabelle, one can enable tracing with using [[simp_trace_new mode=full]]; in Coq, tactics can be prepended by info_ (like info_auto) and the command Show Proof. can be used inside proofs to show the associated proof program.

Proving anything more than bare basics requires lemmas or proofs too large to be comprehensible. Finding lemmas that can assist in finding the proof for a posed theorem can be tedious, though. For this task, the Coq command Search and its Isabelle counterpart find_theorems can be used. Both allow using wildcards and searching for patterns in theorems.

Note that this function is not smart in the sense of being able to compensate for typos and incompleteness, and even slight mistakes can lead to wrong results or none at all.

(Isabelle) See tutorial.pdf section 3.1.11 for more filters.

Theorems whose names are known can be printed out using the commands thm <name> and Print <name>. in Isabelle and Coq, respectively.

The source file in which a specific theorem or similar is defined can be found in Isabelle/jEdit by control-clicking (Ctrl+LeftMouseButton) on the name of the entity. No similar functionality exists in Coq [citation needed], the source file can instead be found by following the package import path (obtained from Locate <name>.) starting from <Coq>/lib/coq/theories/ for the Coq root package, where <Coq> is the Coq installation directory.

Example: Nat.add_0_l states $0+n=n$. Note that there are multiple versions of add_0_l for different domains; Nat.add_0_l is stated over the naturals. Locate Nat.add_0_l. yields Constant Coq.Arith.PeanoNat.Nat.add_0_l. The path to the source file is therefore <Coq>/lib/coq/theories/Arith/PeanoNat.v.

sledgehammer is the most powerful of Isabelle's automation tools, querying several automatic solvers in parallel and reporting if one or more found a correct proof. Some of the solvers automatically find relevant lemmas, which simplifies the process immensely. Sledgehammer is not a tactic, but a tool that searches for relevant tactics and lemmas for a problem, and (if successful) outputs a sequence of steps (normal Isabelle tactics) that solve the current goal.

This can be utilized to avoid large amounts of work finding proofs for simple lemmas, but at the same time contributes to the readability problem, as often the generated proofs contain (or are) obscure one-liners that do not make sense at first glance.

The option to generate Isar proofs has been included, but this does not solve the problem of readability, as these proofs again often contain obscure parts [citation needed].

Sledgehammer is however not a complete substitute for someone who knows what they are doing and will often fail when confronted with seemingly simple problems.

This however can quickly change when the right approach is chosen.

The Coq project CoqHammer aims to provide a tool with similar capabilities, and is included in the Coq distribution (closed issue, charter). Similar to sledgehammer, it is designed to collect relevant facts, feed them to external ATPs and use their results to suggest proofs.

The hammer works best when the goal and the needed lemmas are "close to" first-order logic, as some more sophisticated features of the Coq logic are not translated adequately. In particular, when dependent types are heavily used in a development then the effectiveness of the hammer tool is limited.

from Czajka, Kaliszyk. Hammer for Coq: Automation for Dependent Type Theory (2018)

The Coq project Tactician applies machine learning to suggest applicable proof tactics based on patterns learned from previous proofs.

How good is Tactician?
todo

From the overview on coq-tactician.github.io

See also:

• SMTCoq (seems not to do relevance filtering)
• Discussion on proof hammers on lean zulip archive
• What proof assistant has the best proof search? on Reddit r/dependent_types
• What does it mean that Isabelle has better automation than Coq? on Coq Discourse forum

Another very useful gadget built into Isabelle is Quickcheck (quickcheck), which automatically checks posed theorems for counterexamples. This prevents unnecessary effort put into trying to prove theorems with minor formulation errors. A restricted version (Auto Quickcheck) that only finds trivial counterexamples is executed automatically when a theorem is posed:

TODO find out in which way auto quickcheck is restricted. possible: number of variables to instantiate