4 ms·

Untangling Mechanized Proofs

55 points by matt_d 6y ago

a-bedford 6y ago
That is pretty cool! I have also tried to address this problem in the past, but by adding annotations to the proofs (https://github.com/andrew-bedford/coqatoo https://github.com/andrew-bedford/coqatoo). It was only a proof-of-concept though.
- cpitclaudel 6y ago
  Oh, this is great. Sorry I missed that in my related work section :/
johnbender 6y ago
The thing I love most about mechanized proofs is that my questions about the reasoning always have tangible answers, even if the answer is “we axiomatized this thing”. The availability of the intermediate proof state as a part of the published object makes those answers that much easier to find. This is a really great project!
jacobmischka 6y ago
This is one area where Isabelle/Isar surpasses Coq in my experience, the proofs are simpler to follow because they somewhat mimic written English, and try to emulate flows of states as the author of this article mentions. Isabelle's older apply-script syntax suffers from the same problem as Coq, but Isar seems to solve this problem more cleanly than this addon does for Coq, as it's built into the Isabelle ecosystem directly. Edit: However, this is a neat augmentation to Coq that seems helpful. I commend the author, it looks well done.
- zozbot234 6y ago
  Older versions of Coq used to include an Isar-like feature known as C-zar, or the "Mathematical Proof Language". It was quite intuitive to use, perhaps even moreso than Isar. Unfortunately it was also quite buggy and unmaintained, so it got removed in later releases. Within current versions of Coq, I think the "structuring" operators in Ssreflect could perhaps be used to replicate that proof format, but some extensions are needed. The basic operation "have ... by ..." is pretty much there, but an Isar-like proof language includes more than that.
  - cpitclaudel 6y ago
    That's a great point! I actually discuss Czar in the paper, as part of my discussion of structured proofs: Calculational, structured, and declarative proofs The tactic-based proof style pioneered by LCF [LCF+Gordon1979] is sometimes called *imperative* or *procedural*, in contrast to the *declarative* style introduced by Mizar [Mizar+Trybulec1985] and later implemented in proof assistants like HOL88 [MizarHol+Harrison1996], Isabelle/Isar [Isar+Wenzel1999], TLA+ [TwentyFirstCenturyProof+Lamport2012], HOL Light [MizarLight+Wiedijk2001]_ and even in program verifiers like Dafny [Dafny+Leino2014]. Declarative proofs tend to more closely mirror pen-and-paper proofs, and are generally more readable in isolation than plain imperative proof scripts. They derive from *structured calculational* proofs [ShapeOfArguments+VanGasteren1990, PredicateCalculus+Dijkstra1990, StructuredCalc+Back1997, StructuredHOL+Grundy1997], in which calculations (sequences of propositions chained by logical connectors, each annotated with a succinct justification of the corresponding step, as in `A = { because X } B ⇒ { because Y } C`) are structured through logical cuts and typographical means such as indentation and explicit nesting marks. A declarative proof language was added to Coq in version 8.1 [Czar+Corbineau2008]_(2006), but it saw only limited use and was removed in version 8.7 (2017). Coq 8.4 instead introduced structure to imperative proof scripts using bullets and braces, giving scripts most of the *structured* part of *structured calculational* proofs. While it is possible to emulate the *calculational* part in imperative proofs using tactics to re-state the current goal and hypotheses after each step in a chain of rewrites, this “checked comments” style is not particularly common in Coq (rich tooling existed in Isabelle to support this style of proofs before the introduction of Isar and the switch to declarative style [ProofPresentationIsabelle+Simons1997]). Alectryon's automatic annotations, combined with careful structuring of proof scripts and judicious use of logical cuts (`assert … by …` or SSReflect's `have`), offer the readability benefits of declarative proofs without the burden of adding output annotations.
carapace 6y ago
I find this very hopeful, as I feel that presentation should be a first-class consideration for these sorts of tools. Math is something that happens in the human mind. It doesn't matter if the machine is uncovering the secrets of the Universe if no one can ever appreciate them, eh? I was explaining this to my sister this afternoon and to make the point I picked up a sliderule and slid the slipstick back and forth while pointedly not looking at the thing and asked her, "Am I doing math right now?" - - - - I'm trying to put together a simple, easy (relatively) to understand "stack" for this, starting with the theorem provers of Jens Otten: http://jens-otten.de/provers.html http://jens-otten.de/provers.html (See also "How to Build an Automated Theorem Prover" http://www.jens-otten.de/tutorial_tableaux19/ http://www.jens-otten.de/tutorial_tableaux19/ ) Prolog is a very simple language, the theorem provers are only a dozen lines of code or so, and the sequent calculus prover at least generates proofs that I personally find easy to follow. It doesn't go very far yet, but it's a start. Any information on formal methods and automated theorem proving would be much appreciated. (along the lines of: Concrete Semantics https://news.ycombinator.com/item?id=22074483 https://news.ycombinator.com/item?id=22074483 Metamath Zero, a bootstrapping theorem prover https://news.ycombinator.com/item?id=21358674 https://news.ycombinator.com/item?id=21358674 The Future of Mathematics? [video] https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721 "Building the Mathematical Library of the Future" https://news.ycombinator.com/item?id=25060613 https://news.ycombinator.com/item?id=25060613
- cma 6y ago
  > It doesn't matter if the machine is uncovering the secrets of the Universe if no one can ever appreciate them, eh? It's possible with access to something that almost serves as an oracle like this, we can use it prove deeper things that we do understand, with only the details of this one portion left un-understood. You could just assume a proposition is true or false, and do the same by working with the assumption, but that can quickly combinatorically explode with multiple propositions.
  - carapace 6y ago
    Yes, but you still have a regress: you have to have good reason to trust the oracle. (E.g. Yin-Yang – A tool for stress-testing SMT solvers https://news.ycombinator.com/item?id=25123138 https://news.ycombinator.com/item?id=25123138 They found a bunch of bugs in Z3 and CVC4!)

55 points by matt_d 6y ago

That is pretty cool! I have also tried to address this problem in the past, but by adding annotations to the proofs (https://github.com/andrew-bedford/coqatoo https://github.com/andrew-bedford/coqatoo). It was only a proof-of-concept though.

cpitclaudel 6y ago
Oh, this is great. Sorry I missed that in my related work section :/

johnbender 6y ago

The thing I love most about mechanized proofs is that my questions about the reasoning always have tangible answers, even if the answer is “we axiomatized this thing”. The availability of the intermediate proof state as a part of the published object makes those answers that much easier to find. This is a really great project!

jacobmischka 6y ago

This is one area where Isabelle/Isar surpasses Coq in my experience, the proofs are simpler to follow because they somewhat mimic written English, and try to emulate flows of states as the author of this article mentions. Isabelle's older apply-script syntax suffers from the same problem as Coq, but Isar seems to solve this problem more cleanly than this addon does for Coq, as it's built into the Isabelle ecosystem directly. Edit: However, this is a neat augmentation to Coq that seems helpful. I commend the author, it looks well done.

zozbot234 6y ago
Older versions of Coq used to include an Isar-like feature known as C-zar, or the "Mathematical Proof Language". It was quite intuitive to use, perhaps even moreso than Isar. Unfortunately it was also quite buggy and unmaintained, so it got removed in later releases. Within current versions of Coq, I think the "structuring" operators in Ssreflect could perhaps be used to replicate that proof format, but some extensions are needed. The basic operation "have ... by ..." is pretty much there, but an Isar-like proof language includes more than that.
- cpitclaudel 6y ago
  That's a great point! I actually discuss Czar in the paper, as part of my discussion of structured proofs: Calculational, structured, and declarative proofs The tactic-based proof style pioneered by LCF [LCF+Gordon1979] is sometimes called *imperative* or *procedural*, in contrast to the *declarative* style introduced by Mizar [Mizar+Trybulec1985] and later implemented in proof assistants like HOL88 [MizarHol+Harrison1996], Isabelle/Isar [Isar+Wenzel1999], TLA+ [TwentyFirstCenturyProof+Lamport2012], HOL Light [MizarLight+Wiedijk2001]_ and even in program verifiers like Dafny [Dafny+Leino2014]. Declarative proofs tend to more closely mirror pen-and-paper proofs, and are generally more readable in isolation than plain imperative proof scripts. They derive from *structured calculational* proofs [ShapeOfArguments+VanGasteren1990, PredicateCalculus+Dijkstra1990, StructuredCalc+Back1997, StructuredHOL+Grundy1997], in which calculations (sequences of propositions chained by logical connectors, each annotated with a succinct justification of the corresponding step, as in `A = { because X } B ⇒ { because Y } C`) are structured through logical cuts and typographical means such as indentation and explicit nesting marks. A declarative proof language was added to Coq in version 8.1 [Czar+Corbineau2008]_(2006), but it saw only limited use and was removed in version 8.7 (2017). Coq 8.4 instead introduced structure to imperative proof scripts using bullets and braces, giving scripts most of the *structured* part of *structured calculational* proofs. While it is possible to emulate the *calculational* part in imperative proofs using tactics to re-state the current goal and hypotheses after each step in a chain of rewrites, this “checked comments” style is not particularly common in Coq (rich tooling existed in Isabelle to support this style of proofs before the introduction of Isar and the switch to declarative style [ProofPresentationIsabelle+Simons1997]). Alectryon's automatic annotations, combined with careful structuring of proof scripts and judicious use of logical cuts (`assert … by …` or SSReflect's `have`), offer the readability benefits of declarative proofs without the burden of adding output annotations.

carapace 6y ago

I find this very hopeful, as I feel that presentation should be a first-class consideration for these sorts of tools. Math is something that happens in the human mind. It doesn't matter if the machine is uncovering the secrets of the Universe if no one can ever appreciate them, eh? I was explaining this to my sister this afternoon and to make the point I picked up a sliderule and slid the slipstick back and forth while pointedly not looking at the thing and asked her, "Am I doing math right now?" - - - - I'm trying to put together a simple, easy (relatively) to understand "stack" for this, starting with the theorem provers of Jens Otten: http://jens-otten.de/provers.html http://jens-otten.de/provers.html (See also "How to Build an Automated Theorem Prover" http://www.jens-otten.de/tutorial_tableaux19/ http://www.jens-otten.de/tutorial_tableaux19/ ) Prolog is a very simple language, the theorem provers are only a dozen lines of code or so, and the sequent calculus prover at least generates proofs that I personally find easy to follow. It doesn't go very far yet, but it's a start. Any information on formal methods and automated theorem proving would be much appreciated. (along the lines of: Concrete Semantics https://news.ycombinator.com/item?id=22074483 https://news.ycombinator.com/item?id=22074483 Metamath Zero, a bootstrapping theorem prover https://news.ycombinator.com/item?id=21358674 https://news.ycombinator.com/item?id=21358674 The Future of Mathematics? [video] https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721 "Building the Mathematical Library of the Future" https://news.ycombinator.com/item?id=25060613 https://news.ycombinator.com/item?id=25060613

cma 6y ago
> It doesn't matter if the machine is uncovering the secrets of the Universe if no one can ever appreciate them, eh? It's possible with access to something that almost serves as an oracle like this, we can use it prove deeper things that we do understand, with only the details of this one portion left un-understood. You could just assume a proposition is true or false, and do the same by working with the assumption, but that can quickly combinatorically explode with multiple propositions.
- carapace 6y ago
  Yes, but you still have a regress: you have to have good reason to trust the oracle. (E.g. Yin-Yang – A tool for stress-testing SMT solvers https://news.ycombinator.com/item?id=25123138 https://news.ycombinator.com/item?id=25123138 They found a bunch of bugs in Z3 and CVC4!)