Application of automatic induction principle versus induction tactic

Using Coq
1

Hi there,

Consider a binary relation over a type and its reflexive transitive closure:

Definition Rel (A:Type) := A -> A -> Prop.

Inductive refltrans {A:Type} (R: Rel A) : Rel A :=
| refl: forall a, (refltrans R) a a
| rtrans: forall a b c, R a b -> refltrans R b c -> refltrans R a c.

The corresponding induction principle is given as follows:

forall (A : Type) (R : Rel A) (P : A -> A -> Prop),
       (forall a : A, P a a) ->
       (forall a b c : A, R a b -> refltrans R b c -> P b c -> P a c) -> forall y y0 : A, refltrans R y y0 -> P y y0

I want to prove a theorem whose environment at some point (after unfolding some definitions and generalizing some variables) seems to match the goal of the induction principle above:

  A : Type
  R : Rel A
  HZ_prop : exists f : A -> A, forall a b : A, R a b -> refltrans R b (f a) /\ refltrans R (f a) (f b)
  ============================
  forall a b : A, refltrans R a b -> forall c : A, refltrans R a c -> exists d : A, refltrans R b d /\ refltrans R c d

At this point I wanted to “apply refltrans_ind” because I was expecting P to match with “forall c : A, refltrans R a c -> exists d : A, refltrans R b d /\ refltrans R c d” but I get an error:

Error:
In environment
A : Type
R : Rel A
HZ_prop : exists f : A -> A, forall a b : A, R a b -> refltrans R b (f a) /\ refltrans R (f a) (f b)
Unable to unify "forall a : ?M160, ?M162 a a" with "A".

I managed to prove this theorem using the induction tactic directly, but I wanted to understand better the relation between the induction tactic and the use of the induction principle automatic generated by Coq for inductive definitions in more elaborated examples as the one above.

Any help is very much appreciated.

Regards,
Flávio.

1 Like
2

This is fine. Unfortunately, you are expecting a bit too much from the unification algorithm used by apply. It usually has a hard time find the correct form of P. So, you have to help Coq a bit by constraining the problem some more. Here are two examples:

  1. apply (refltrans_ind A R (fun a b => forall c : A, _ -> exists d : A, _)).
  2. refine (refltrans_ind _ _ _ _ _).
3

Thank you very much Guillaume!