The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

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.

-- 
Robin