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