The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

2012/4/13 AUGER Cédric 
<sedrikov AT gmail.com>:
> Le Thu, 12 Apr 2012 16:38:25 +0200,
> Jonas Oberhauser 
>Â <s9joober AT googlemail.com>
>  a écrit :
>
>> 2012/4/12 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).
>>
>> I know. That's exactly the problem. Is there any reason for that?
>>
>
> Yes: a rewritten subterm is not a subterm anymore.
> And inversion does rewritings.

I asked my question in an unclear way, let me rephrase:

"Is there any reason why inversion does rewritings?"


>> >> 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
>
> -- so do not apply inversion in then subterm

What do you mean by that?

>> > if possible, do your recursion first and only then do you rewritings
>>
>> I'd really love to do that - but I can't! Because inversion already
>> /does/ the rewriting, without my consent!
>
> So do not use it for fixpoint.
> I can provide you an example of how to do that if you give me a minimal
> self contained file in which your problem occur.

I'll try to come up with a small example.

>> What I'd expect inversion to do is destruct the argument and infer
>> some rules like equalities and impossibilities etc, but what I don't
>> expect it to - what it does, however - is to also rewrite in the
>> subterms and in the goal.
>
> inversion is a badly coded tactic (it is already known in the
> community), for instance it produces ugly terms with equalities
> everywhere, even when that wouldn't be needed. Do "Print <your_term>."
> on a proved term using induction, and you will understand what I mean.

With a term using inversion you mean.
Someone should go and write a good alternative.

> For simple, people use tactics to build proofs, not terms; and when you
> build proofs, you hardly ever use "fix", as "induction" is better to
> use. People writing terms do not use tactics, and so do not use
> "inversion".
>
> So you mainly have to choose between [fix/match with] and
> [induction/inversion]. Mixing the two styles is considered bad taste.

I see. The problem with induction are dependent types, eg. I want
ind : forall a b, P a b -> ...
and not
ind : P a0 b0 -> ...
(where I recurse over the proof of P a b).

As fo mixing terms and tactics, I'm not willing to do the inversion
process by hand (which would give me the situation I expected).
(With by hand, I mean writing the match term).

Have a nice day, Jonas