[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.