The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 12 Apr 2012 01:44:30 +0200,
Jonas Oberhauser 
<s9joober AT googlemail.com>
 a écrit :

> After doing inversion instead of destruction in a fixpoint, I don't
> get the correct terms as assumptions.

fix is a very low level tactic.
NEVER USE IT unless you know very well coq mechanisms and are ready to
face the consequences (as you do here).

Induction is a far better tactic (although not very usefull with mutual
inductives).

Inversion is not "fix" compliant, since it fact it produces terms
which are not subterms of the main term).

> Instead, I get terms which have
> been rewritten by the rules inversion
> My code looks like this (I won't go into too much detail here):
> 
> 'fix ind 9. ...
> 
> inversion su.
>   .. (* solving the base cases... *)
>   ..
>   .. (* inductive case *)
>   apply (ind .. .. H4).
> 
> Guarded.'
> 
> Where H4 is one of the variables generated by inversion.
> This is what my assumptions are (as shown in CoqIde):
> 
> '...
> H4 : P a
> ...'
> 
> However, the Guarded command complains bitterly:
> 
> 'Recursive call to ind has principal argument equal to "H8" instead of
> one of the following variables: "H" "H0" "H1".'
> 
> While it says that the environment looks like this:
> 
> '...
> H1 : P a
> ...
> H3 : a = b
> ...
> H8 : P b
> 
> In that environment, I expect to be able to solve the goal with (ind
> ... H1), using eq_ind with H3.

Do not rewrite in subterms, as they won't be subterms anymore.

> However, H1 is hidden by the tactic. Is there a (non-cosmetical)
> reason for that?
> I have had this problem frequently in the past. This specific instance
> could be solved by a dependent induction, but it makes those proofs
> unnecessarily hard to come up with.
> 
> Kind regards, Jonas

So:
avoid inversion when you can easily avoid it
if you are to use it, do not rewrite in the structural argument of the
fixpoint
if possible, do your recursion first and only then do you rewritings

fix is very strict, if you touch your induction hypothesis, you break
the structural induction only regular conversion tactics are allowed
(simpl, red, cbv, compute, change…) rewrite is not a conversion tactic.
Furthermore, you need some extra vigilance, and often have to use
"Guarded" to check you didn't something wrong. It is not advised to use
it, unless you really know what you are doing.

Some advice when you use the fix tactic:
- immediately "destruct" your main argument.
- in each case, immediately do a
 "assert (Rec := fun x1..xn => <your fixpoint> x1..xn
                                 <your structural subterm>);
  clear <your fixpoint>. (*but not Rec !*)
  Guarded."
  x1..xn are terms you dont't yet know how to instantiate;
  only the call to the recursive argument is necessary to
  ensure the recursion, other parameters can be
  generalized at whish.
  Clearing the fixpoint ensure you won't use it inadvertatly
  (for example using the auto tactic).
- now you are safe!