Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Inversion, Induction & Fix Guard

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Inversion, Induction & Fix Guard


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page