The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Tue, 6 Dec 2011 23:30:38 +0900,
Gyesik Lee 
<leegys AT gmail.com>
 a écrit :

> I don't try to answer your question, but want to ask back why Coq
> should choose your simplified version of induction.
> I am saying without having done any deep consideration, but probably
> there are cases where the simplified version is not comfortable to be
> used. The question is now about the mechanism of producing induction
> principles.
> 
> Gyesik

I think you are wrong on that point, Lee;

==============================================================
Parameter X : Type.
Parameter r : X -> X -> Prop.

Inductive star (x:X): X -> Prop :=
| starR : star x x
| starT x' y : r x x' -> star x' y -> star x y.

Definition star_ind' y (P:X->Prop) HR RT x HS
:= star_ind (fun x z => y = z -> P x)
            (fun x H => match H in _=y0 return P y0 with
                        eq_refl => HR end)
            (fun x x' z H K L Heq =>
                 match Heq in _=y0 return star _ y0 -> _ with
                 eq_refl => RT x x' H end K (L Heq))
            x y HS (eq_refl y).

Definition star_ind'' (P : X -> X -> Prop) HR HT x y HS :=
 star_ind' y (fun t => P t y) (HR y) (fun x x' => HT x x' y) x HS.

Goal forall P HR HT x y HS, star_ind'' P HR HT x y HS = star_ind P HR
HT x y HS. intros.
 unfold star_ind'', star_ind'.
 revert x y HS.
 fix IH 3.
 intros x y [].
  clear IH.
  split.
 intros x' y0 r0 s.
 assert (K := IH _ _ s); clear IH.
 Guarded.
 simpl.
 rewrite K; clear.
 split.
Qed.
=======================================================

This show that defining star_ind'' from star_ind' is a lot easier
than defining star_ind' from star_ind.

That means that in any place you should want to use star_ind, then
using star_ind' will be really easy; but the reciproque doesn't hold,
as you will probably need some rewritings (since you need to keep that
the 'y' in the subterm is equal to the 'y' in the term).
=======================================================

Now, for the reason why to have this generation, I would say that:

* the current generation is what the user expects, not some
  obscure trick understanding what should be a parameter and
  what shouldn't be
* the generation is very easy, for instance, for star_ind:
Eval compute in star_ind.
     = fun (P : X -> X -> Prop) (f : forall x : X, P x x)
         (f0 : forall x x' y : X, r x x' -> star x' y -> P x' y -> P x
y) => fix F (x x0 : X) (s : star x x0) {struct s} : P x x0 :=
         match s in (star _ x1) return (P x x1) with
         | starR => f x
         | starT x' y r s0 => f0 x x' y r s0 (F x' y s0)
         end
     : forall P : X -> X -> Prop,
       (forall x : X, P x x) ->
       (forall x x' y : X, r x x' -> star x' y -> P x' y -> P x y) ->
       forall x x0 : X, star x x0 -> P x x0

  whereas the generation of star_ind' would give what I defined earlier
  (so it would rely on star_ind, or be probably even uglier!)
  Of course, coq could generate "star_ind" and "star_ind_smart",
  but that would make even more generated functions, and for example
  when I extract program, I really dislike these automatically generated
  functions in the code (I do not say we should remove them; because
  they can be used in extracted terms).
* changing that now may break some proofs (think of retrocompatibility),
  so that should mean introducing a new tactic (smart_induction)
* I think it is the responsability of the programmer to understand what
  he does and think how to define its inductive constructions.
* There are a lot of really more interessant features to develop
  than this one which in fact does not come often; and as I
  previously said is easily solved by thinking what should be
  a parameter and what can't be a parameter, then write the inductive
  with the arguments in the right order (and if you want, define a
  Notation to have it in the order you want and not the order Coq
  wants).

Of course, if you have ideas how to adress these points, you can tell
us to include your feature!