The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 07 Apr 2013 16:34:19 +0200,
Robbert Krebbers 
<mailinglists AT robbertkrebbers.nl>
 a écrit :

> On 04/07/2013 03:12 PM, AUGER Cédric wrote:
> >> Require Import Eqdep Eqdep_dec Omega Utf8.
> >>
> >> Lemma nat_le_pi: ∀ (x y : nat) (p q : x<  y), p = q.
> >> Proof.
> >>     assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
> >>       y = y' → eq_dep nat (le x) y p y' q) as aux.
> >>     { fix 3. intros x ? [|y p] ? [|y' q].
> >>       * easy.
> >>       * clear nat_le_pi. omega.
> >>       * clear nat_le_pi. omega.
> >>       * injection 1. intros Hy. now case (nat_le_pi x y p y' q
> >> Hy). } intros x y p q. now apply (eq_dep_eq_dec eq_nat_dec), aux.
> >> Qed.
> >
> > That is cheating, you are using an axiom ^^
> 
> Not according to Coq: [Print Assumptions nat_le_pi.] gives:
> 
> Warning: query commands should not be inserted in scripts
> Closed under the global context

Mea culpa, I just printed

Print eq_rect_eq__eq_dep_eq.

which returned:

eq_rect_eq__eq_dep_eq = 
λ (U : Type) (eq_rect_eq : Eq_rect_eq U)
(P : U → Type) (p : U) (x y : P p)
(H : eq_dep U P p x p y),
eq_rect_eq__eq_dep1_eq U eq_rect_eq P p x y
  (eq_dep_dep1 U P p p x y H)
     : ∀ U : Type, Eq_rect_eq U → Eq_dep_eq U

then I wanted to explore eq_rect_eq which uses an axiom.

What I didn't see is that the occuring "eq_rect_eq" is here a bounded
variable and not some definition of the library.