Proof automation

Harpoon provides rudimentary automation for basic tasks during proofs. Each automation type can be controlled via the toggle-automation tactic.

Automations run at the moment that a new subgoal is created.

Actions performed by automatic tactics can be undone.

auto-intros

This automation introduces assumptions into the context whenever the subgoal has a function type.

auto-solve-trivial

This automation solves subgoals in which the context contains an assumption whose type is convertible with goal type.

It will never solve the last remaining subgoal in a theorem, as this makes certain theorems impossible to prove using Harpoon. For example, this is essential for implementing a function such as double : [|- nat] -> [|- nat]: auto-intros will bring x : [|- nat] into the context and auto-solve-trivial would immediately finish the theorem before the user ever sees a subgoal prompt.