Interactive Proving with Harpoon

Harpoon is an interactive prover for Beluga. Users of Harpoon develop proofs in a REPL using a small set of built-in tactics. These correspond to the main proof strategies one uses in developing metatheory proofs, e.g. inversion or appeal to a lemma or induction hypothesis.

• Prover Structure
  • Session
  • Subgoal
• Proof automation
  • auto-intros
  • auto-solve-trivial
  • auto-invert-solve
  • inductive-auto-solve
• Interactive Command Reference
  • Administrative tactics
  • Proof tactics
  • auto-invert-solve
  • inductive-auto-solve
• Undo
  • Limitations