4 ms·

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 bac

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 8y ago
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.
- uryga 8y ago
  > the underlying type theory is intuitive isn't that "intuitionistic"?
  - gnulinux 8y ago
    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 8y ago
      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 :) )
- tomsmeding 8y ago
  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.

gnulinux 8y ago

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.

uryga 8y ago
> the underlying type theory is intuitive isn't that "intuitionistic"?
- gnulinux 8y ago
  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 8y ago
    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 :) )
tomsmeding 8y ago
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.