The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Sat, Nov 29, 2008 at 02:36:05PM +0000, Robin Green wrote:
> On Sat, 29 Nov 2008 14:03:06 +0000
> Thorsten Altenkirch 
> <txa AT Cs.Nott.AC.UK>
>  wrote:
> 
> > > I suspect I need K (or I am just too stupid). Can anybody conform  
> > > either? I.e. can I prove this using Coq.Logic.Eqdep or without?
> > 
> > I am just too stupid. But so is Coq. I just need to use dependent  
> > inversion.
> > 
> > Actually I realized that I can prove it with the standard eliminator  
> > for equality:
> > 
> > eq_elim : forall (A:Set)(x:A)(P:forall y:A, (x=y)->Set)
> >                              (m:P x (refl_equal x))
> >                              (y:A)(p:x=y),P y p.
> > 
> > This is not automatically derived by Coq (why not?) but it can be  
> > proven using dependent inversion.
> 
> Doesn't the generated proof rely on K or an equivalent, though?
> 
> On that note, I think the coq documentation should be updated to warn
> when using certain tactics can introduce axioms.


Concerning the dependent version of the elimination principle for eq
(or more generally for inductive types in Prop), it's true that Coq
doesn't provide it by default. Probably because it has been considered
that the non-dependent version is enough for most usages and quite
simplier. But you can nonetheless obtain the full version
automatically:

Scheme eq_elim := Induction for eq Sort Type.

Check eq_elim.
eq_elim
     : forall (A : Type) (x : A) (P : forall a : A, x = a -> Type),
       P x (refl_equal x) -> forall (y : A) (e : x = y), P y e

Reciprocally, the "Scheme ... := Minimality for ..." command allows
one to obtain the non-dependent version of the elimination principle.
This might be interesting when Coq has decided that the full version
is best (that is, for inductive types in Set or Type).

On the topic of axioms, a "Print eq_elim" after the above command
shows clearly that no axiom is used in the proof. This can also be
confirmed by the new command "Print Assumption eq_elim" whose aim is
to recursively retreive the axiom(s) a particular object is using.
Concerning standard tactics, apart obviously from "admit", I can see
none that might introduce axioms. And anyway, in case of doubt, 
you can do a "Print Assumption" of your lemma. 

Best regards, 

Pierre Letouzey