coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonas Oberhauser <s9joober AT googlemail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Inversion, Induction & Fix Guard
- Date: Thu, 12 Apr 2012 01:44:30 +0200
After doing inversion instead of destruction in a fixpoint, I don't
get the correct terms as assumptions. 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.
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
- [Coq-Club] Inversion, Induction & Fix Guard, Jonas Oberhauser
- Re: [Coq-Club] Inversion, Induction & Fix Guard,
AUGER Cédric
- Message not available
- Message not available
- Re: [Coq-Club] Inversion, Induction & Fix Guard, Jonas Oberhauser
- Message not available
- Message not available
- Re: [Coq-Club] Inversion, Induction & Fix Guard,
AUGER Cédric
Archive powered by MhonArc 2.6.16.