Posted on July 1, 2017 by Calvin Beck

Tags: coq, tactics, theorem proving, proofs

# Induction

## Introducing too much.

https://softwarefoundations.cis.upenn.edu/draft/lf-current/Tactics.html#lab139

By introducing a variable you are saying for a “particular” instance of that variable. Not for all such instances of the variable.

Thus, when introducing more than necessary prior to induction you may unintentionally weaken the induction hypothesis that you will get, making it impossible to prove your goal.

# Destruct

## Forgetting things

When you `destruct`

a compound expression you lose what the original equation was. For instance:

```
destruct (beq_nat 3 n).
```

will give you two subgoals. One where `(beq_nat 3 n)`

is replaced with `true`

, and one where it is replaced with `false`

.

Sometimes, however, you actually need the fact that ```
(beq_nat 3 n)
= true
```

in that branch of the proof, or that ```
(beq_nat 3 n) =
false
```

in the other branch of the proof. You can keep this information with:

```
destruct (beq_nat 3 n) eqn:Hbeq3.
```

Which will introduce in the context a hypothesis `Hbeq3`

which will be `beq_nat 3 n = true`

in the `true`

branch of the proof, and `beq_nat 3 n = false`

in the false branch.