The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

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

  I guess you want to define the map2 function on vectors. You start
with an induction on the length on the vectors, i.e. you start
building the program

  Fixpoint Vbinary [n:nat] : (vector n)->(vector n)->(vector n) :=
  <[n](vector n)->(vector n)->(vector n)>Cases n of
  |  O    => [v1,v2]Vnil
  | (S n) => [v1,v2]?
  end.

  but your vectors v1 and v2 are not destructed (i.e. no Cases on
them), only the length is. Then the role of the two calls to Inversion
is to destruct each of them (and eliminating the impossible cases),
i.e. you're building the program

  Fixpoint Vbinary [n:nat] : (vector n)->(vector n)->(vector n) :=
  <[n](vector n)->(vector n)->(vector n)>Cases n of
  |  O    => [v1,v2]Vnil
  | (S n) => [v1,v2]
    Cases v1 of
    | Vnil => (* impossible by typing *) (False_rec ...)
    | (VCons a v3) =>
      Cases v2 of
      | Vnil => (* impossible by typing *) (False_rec ...)
      | (VCons a0 v5) => ?
      end
    end
  end

  But maybe you'd expect rather a program working directly by
induction on the vectors (not on the length).

  Then do

Intros n v1 v2; NewInduction v1;
  [Exact Vnil 
  |Inversion_clear v2; Rename H into v2; Exact (Vcons (g a a0) n (IHv1 v2))]

and you'll (morally) get the program

  Fixpoint Vbinary [n:nat][v1:(vector n)] : (vector n)->(vector n) :=
  <[n,v](vector n)->(vector n)>Cases n of
  |  Vnil        => [v2]Vnil
  | (VCons a v1) => [v2]
       Cases v2 of
       |  Vnil => (* impossible by typing *) (False_rec ...)
       | (VCons a0 v2) => (Vcons (g a a0) n (Vbinary v2))
       end
  end

  Hope it helps.

  Hugo Herbelin