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.

actions capabilities.

Current limitations:

• no paramater variables
• no substitution variables
• no case splits (>1 case produced)
• no pair type
• no splitting on contexts

auto-invert-solve

This automation attempts to solve the subgoal if no variable splitting (other than inversions) is required to solve the goal. It performs 2 iterations of depth-first proof-search, once on the computation level, and once again on the LF level. Use auto-invert-solve INT to specify the maximum depth you want your search tree to reach. Depth is incremented when we attempt to solve a subgoal.

For example, if we want to solve Ev [|- S (S (S (S z)))] this would require a depth bound of at least 2::

inductive Ev : [⊢ nat] → ctype =
| ZEv : Ev [⊢ z]
| SEv : Ev [⊢ N] → Ev [⊢ S (S N)]

depth = 0
solve for Ev [|- S (S (S (S z)))] -> focus on SEv --->

depth = 1
solve for Ev [|- S (S z)] -> focus on SEv --->

depth = 2
solve for Ev [|- z] -> focus on zEv

Note: If a goal has more than one subgoal, depth only increments by 1.

For example, if we want to solve ``Less_Than [|- S z] [|- S (S (S z))]`` this
would require depth bound of 3:

inductive Less_Than : [⊢ nat] → [⊢ nat] → ctype =
| ZLT : Less_Than [⊢ z] [⊢ S N]
| LT : Less_Than [⊢ N] [⊢ M] → Less_Than [⊢ S N] [⊢ S M]
| Trans_LT : Less_Than [⊢ N] [⊢ M]
               → Less_Than [⊢ M] [⊢ K] → Less_Than [⊢ N] [⊢ K]

depth = 0
solve for Less_Than [|- S z] [|- S (S (S z))] -> focus on Trans_LT --->

   depth = 1
   solve for Less_Than [|- M] [|- S (S (S z))] -> focus on LT --->

      depth = 2
      solve for Less_Than [|- M'] [|- S (S z)] -> focus on LT --->

         depth = 3
         solve for Less_Than [|- M''] [|- S z] -> focus on ZLT

   ---> found LT LT ZLT : Less_Than [|- S (S z)] [|- S (S (S z))]

   depth = 1
   solve for Less_Than [|- S z] [|- S (S z)] -> focus on LT --->

      depth = 2
      solve for Less_Than [|- z] [|- S z] -> focus on ZLT

   ---> found LT ZLT : Less_Than [|- S z] [|- S (S z)]

-> found Trans_LT (LT ZLT) (LT LT ZLT) : Less_Than [|- S z] [|- S (S (S z))]

inductive-auto-solve

This automation will perform a case split on the user-specified variable then call auto-invert-solve on each sub case. Use inductive-auto-solve INT to specify the maximum depth you want your search tree to reach. Depth is incremented as above.