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