What `dependent induction` tactic does in Coq and how to use it

Question

Can you please provide me with high-level explanation on which usecases dependent induction / dependent destruct tactics have, and how they work (I would be grateful for explanation high-level enough for a beginner to understand).

Everything I found on it so far is extremely overcomplicated.

Answer 1

Well, we know inductive data types are often indexed by indices, a basic example that you may have seen is the vector that is indexed by a Type and its size.

Given an example of a vector t A (S n), since we know that the vector has a size higher than 0, we know there is a value of type A in this vector. It would be simply written as :

Theorem not_empty : forall A n, t A (S n) -> A.

but if you tried to prove this using the usual destruct/induction, you end up with two cases:

Theorem not_empty : forall A n, t A (S n) -> A.
intros.
destruct X.
- admit. (*here is our impossible clause*)
- exact h.
Admitted.

Even though we know the vector has a size equal/higher than one, Coq still gives you a goal that is related when the vector is null. We can abuse from remembering indices and we can catch these cases by hand.

Theorem not_empty2 : forall A n, t A (S n) -> A.
intros.
remember (S n).
destruct X.
- inversion Heqn0.
- exact h.
Defined.

That is good but would be cooler if there is a tactic that already does it for you and eliminates the impossible clauses?

Theorem not_empty3 : forall A n, t A (S n) -> A.
intros.
dependent induction X.
exact h.
Defined.