coqcoq-tacticinduction

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


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.


Solution

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