[gnulinux]

Not pretending to be an expert but I did a lot of proofs in Agda (a related subject was my bachelor's thesis). In what way do you find tactics useful? I personally find Coq having bunch of mini-languages inside, one being a tactic language confusing. I think it's a non-optimal (though viable) solution to the problem. I think, as always, lisp gets it right. Computing is all about abstractions and sometimes even abstractions that can talk between each other and the best way to approach this problem is homoiconicity. I think agda gets it right, if you write macros helping you solve the problem at hand you can write very elegant and readable proofs. I understand that tactics are very popular in proof automation community and I'm very likely very wrong. But this is just a reflection of my experience. I'm currently writing my own dependently typed PL and am debating merits of tactics. So far I can't find a reason to add them provided you give enough lispness to your language.

[fmap]

Tactics are very useful when developing proofs rather than dependently typed programs (unless you are using very precise types, as is common in e.g. the Coq program package).

The point is that in a proof you are usually not interested in the precise shape or computation behavior of the underlying proof term and this allows you to use far more aggressive automation than what you are doing with a typical macro. Likewise, you don't really want to see the proof term in the first place. Think about how long chains of equational reasoning are encoded in type theory - this is just noise that detracts from writing your proofs.

As for homoiconicity, I think this is orthogonal to a tactic language. Both lean's tactics and template Coq allow you to reify the syntax of the type theory in order to write automation tactics, but this is separate from the proof search aspects of tactics.

[tomsmeding]

My experience with this kind of stuff: done some Coq by myself and some HOL in class.

Generally, the distinguishing feature of tactics is that they provide backward reasoning, instead of forward reasoning, what a verification engine would be written around. Mind that I haven't worked with any proof system yet besides Coq and HOL, so my opinion might be far out, but I think backward reasoning is a very nice way to construct proofs, especially in the context of a proof assistant.

Aren't things like algorithms for simple automated proving more easily embedded in a tactic language than in a forward reasoning language? When reasoning backward, one naturally reduces the statement to prove to simpler and simpler statements, and at some point they become simple enough to be handled by some automatic prover. (auto/omega/... in Coq, PROVE_TAC/COOPER_TAC in HOL) When reasoning forward, I don't see how one would go about using automated provers like that, but it's likely I'm missing some idea here.

> I'm currently writing my own dependently typed PL

Awesome! I'm all for writing interesting new languages and implementations, especially in this area. Once you've got something to show, be sure to post here on HN, since people might enjoy looking around. :) (If it doesn't get lost in the swarm of submissions...)

[gnulinux]

I think forward reasoning works only because the underlying type theory is intuitive. When I approach proofs in agda, I simply approach it the same way I write haskell code. "You have bunch of cosets and you wanna go to group." You have objects (proofs) around and you want to construct an instance of a type (theorem) so you start with functions (lemmas) that give objects of desired types. Again, I'm not very familiar with Coq (only agda) but I suppose by backwards reasoning you mean the last unconstructed type in your proof is the type with highest level of abstraction. On the other hand, in agda it's the first one because either you already know a function (lemma) returning this type and need to construct it's arguments (assumptions) or you can use an anonymous function (implication introduction).

This is a totally random and not a well-thought-out statement but to me it seems like the difference between agda and Coq seems like the difference between purely functional and imperative programming.

[tomsmeding]

I think I just need to try out something like Agda before I make any more claims :) Does Agda have something that can automatically prove small formulas in e.g. pure predicate logic?

Backwards reasoning works something like this: to prove 'forall n: P n', it is sufficient to prove 'P 0' and 'P n => P (succ n)', so if you have 'forall n: P n' as your so-called proof goal, you can use the induction tactic to transform that into two goals: 'P 0' and 'P n => P (succ n)'. You then have to separately prove both goals. The tactic system then basically build the actual proof by putting everything on a stack and applying in reverse: once you've proved both goals, it knows it can apply the forward-reasoning induction proof function to construct a proof of the original statements from the two proofs you gave.

> the difference between agda and Coq seems like the difference between purely functional and imperative programming.

Bold, bold :) I'll have to try Agda before I can comment on that. Coq proofs do seem a bit inperative, so there's that.

[TezlaOil]

> The tactic system then basically build the actual proof by putting everything on a stack and applying in reverse: once you've proved both goals, it knows it can apply the forward-reasoning induction proof function to construct a proof of the original statements from the two proofs you gave.

In Agda, you would type something like `nat-ind ?x ?y` into a hole of type (forall m -> P m). Then ?x becomes a hole of type (P zero) and ?y becomes a hole of type (forall n -> P n -> P (suc n)), and you can fill these holes with proofs at your own leisure. It does not feel all that different from using `induction m` in Coq. In Agda, you'd normally implement your "reflective tactics" as functions, or you'd write macros if you really need them (e.g. for ring solvers), but there is no separate tactic language and proofs are never tactic scripts.

[uryga]

> the underlying type theory is intuitive

isn't that "intuitionistic"?

[gnulinux]

No I meant intuitive like easy to understand for humans. (It is also intuitionistic but that's a technical fact shared by both Coq and Agda (though not HOL)). The reason I said that is because thinking in terms of types is very straightforward for people. "Give me a View and Serializer so I can give you JSON" "Why is my code not working? Oh because you can't always find the head of a list, I need to give you NonEmpty List T". Similarly, proving something is a group is like trying to go Group somehow from the objects around.

[uryga]

ah, my bad, i see how that makes more sense. FWIW i agree – often, mentally converting a theorem to a type and thinking about the problem in that framework makes things easier for me to grasp. (also explains why we "apply" theorems/lemmas :) )