The Coq mailing list

["J. Zhang" <j.l.zhang AT durham.ac.uk>]

Dear Coq people,

 

Can I get the more detailed explaination of inversion tactic in Coq. For example, from the this below definition on Vector, when we define Vbinary function, why do we need to do inversion twice. And for each inversion operation, what is consequence of it. I feel confused to understand.

 

Hope to get advice.

 

Inductive vector: nat -> Set :=
        | Vnil : (vector O)
        | Vcons : (a:A) (n:nat) (vector n) -> (vector (S n)).

 

Lemma Vbinary : (n:nat)(vector n)->(vector n)->(vector n).
Proof.
        Induction n; Intros.
        Exact Vnil.
        Inversion H0; Inversion H1.
        Exact (Vcons (g a a0) n0 (H H3 H5)).
Defined.

Regards

 

Jack