6
$\begingroup$

I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate boilerplate code while having much fewer static guarantees and much harder interactive stepping. This looks to me like a clear code smell, but I always assumed that is inevitable evil.

I solved most of Software Foundations Volume 1 (and partially 2) and while doing it, I spent most of my time trying to understand how tactic language works, not actually grasping PL theory or formal verification overall. After that, I found out that the Agda "variant" of SF exists, and I do not have any such issues with it. Almost all proofs seem clear to me at first sight, at least once you understand Agda syntax and the math idea behind proof. PLFA case report claims that it was not clear that using language without tactics would not make things much longer, but in fact it worked very well. While PLFA is only covering part of SF, so far I do not see any reasons why the same reasoning would not work for the rest of SF.

I was looking and asking for examples of tactic usage in practice, where working without them would be painful, but did not find anything that would convince me. All examples I could understand seem to me either like tactic languages used as boilerplate generating (instead of design making proper proof reuse easy) or just using auto/ring/simp, which may work without any tactic language. I only understand PL theory and basic abstract algebra/topology well and also do not understand complex tactic code, which may be a reason I did not find suitable examples.

I know that SSReflect was used for proving multiple very complex results, but as far as I understand what is going on (not being able to get how this proof works in detail), it seems like the "reflect pattern" part of SSReflect is much more important for writing such kind of proofs, then is tactic language by itself.

So my current hypothesis is that any use of tactic language is possible to be refactored by using proof patterns/instrumentation which is possible (while not always actually implemented) in Agda-style language. By such I mean:

  1. Boolean reflection proof pattern
  2. Libraries designed for proper code reuse by means of class types/parameterized modules/polymorphism
  3. Interactive programming with case splitting and auto tooling (which is AFAIU is not SoA in Agda currently)
  4. Large-scale decision procedures, like ring/omega tactics and external ATP integrations

So to (dis-)proof this hypothesis, I am asking for specific, clear, and (hopefully) short examples of theorems/theories/libraries for which proofs are simple/clear/nice with tactic language, but they would not be without them (even by using tools I listed before instead).

I would stress, that while the question may have some flame potential, I think that my question is clear and examples I am looking for may be very useful for discussion of proof techniques. So even if you do not agree with me, the question is clear and useful, so please do not vote for closing.

Partially related question:

UPD:

I would like to reiterate, that I am asking for more specific examples not to confront anyone, and even not necessarily because I disagree. I just think that while general direction answers make sense as well, in such kinds of questions one must specify a specific task, a specific measure of "simple proof" and an overall goal, otherwise, the discussion is too vague and prone to "dynamic typing is bad" kind of holy war. Depending on proof/coding style and task people could evaluate measures of proof/code construction usability very differently.

$\endgroup$
4
  • 1
    $\begingroup$ Good question! Is there a typo in the title? It looks a bit confusing and ungrammatical as it is currently written. $\endgroup$
    – Trebor
    Nov 1, 2023 at 12:42
  • $\begingroup$ Thanks. Linted with Gramarly, there was a lot grammar errors, hopefully it is better now. $\endgroup$
    – uhbif19
    Nov 1, 2023 at 13:38
  • $\begingroup$ Todays youth, they say things like "AFAIU" and "SoA". $\endgroup$ Nov 1, 2023 at 17:29
  • 1
    $\begingroup$ A typo? "So do (dis-)proof this hypothesis" should be "So to (dis-)proof this hypothesis"? $\endgroup$ Nov 2, 2023 at 10:17

1 Answer 1

4
$\begingroup$

so far I do not see any reasons why the same reasoning would not work for the rest of SF

Wait for (or jump straight to) at least https://softwarefoundations.cis.upenn.edu/slf-current/Rules.html ;)

3. Interactive programming with case splitting and auto tooling

For one, I don't see why auto is not a tactic, or why it is an "acceptable tactic" in contrast to the rest. For sure I don't want auto in the core of my proof assistant! :D

Second, we're talking about proof readability and understandability. Long ladders of trivial case splits and straightforward proofs via substitution of the right equals for equals, or even induction are not very readable for me at all. To me, it's much more understandable when you swipe boring proofs under the rug of tactics and only keep the high-level structure of the argument before my eyes.

4. Large-scale decision procedures, like ring/omega tactics and external ATP integrations

I don't see the difference between "decision procedures" and "tactics"...

Moreover, we don't trust external tools, so we have to convert these external proofs from ATPs into our internal proofs for the proof assistant to double-check. And before that, we need to convert our goal and theorems from the internal format to the format of an external ATP. So we're taking the goal and theorems, processing them somehow, and spitting out a proof term. Congratulations, you've invented tactics! :D

$\endgroup$
14
  • $\begingroup$ > ... at least softwarefoundations.cis.upenn.edu/slf-current/Rules.html Could you please elaborate, on what you mean? You say that embedded non-classical logics, like separation logic, are hard to reason about in Agda? Could you give some specific reasons you have in mind? $\endgroup$
    – uhbif19
    Nov 3, 2023 at 9:16
  • $\begingroup$ I see them less acceptable because: 1. I am against "tactic languages", which are a strange kind of automation combination language, not any automation by itself. Decision procedures are self-contained, you just discharge them, and then you think the proof is only technical. 2. Auto as instrumentation gives you the resulting proof, which may be more direct to read (as a text, without interactive stepping). 3. Also, if tactic combination is really that essential, you I believe you could encode both normal forms and tactics inside language (HDec monad is an example). $\endgroup$
    – uhbif19
    Nov 3, 2023 at 9:21
  • $\begingroup$ > Long ladders of trivial case splits and Could you point me to any specific proof example, that you believe cannot be refactored in some well-readable form? $\endgroup$
    – uhbif19
    Nov 3, 2023 at 9:23
  • 1
    $\begingroup$ @uhbif19 please take a look at doi.org/10.1007/978-3-030-51054-1_10 $\endgroup$ Nov 3, 2023 at 16:08
  • 1
    $\begingroup$ OK, if you think you can rewrite any proof in Agda simpler and more concise, here's one for you to play with: softwarefoundations.cis.upenn.edu/slf-current/… :) $\endgroup$ Nov 3, 2023 at 16:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.