Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question about decidability of relations and proof irrelevance

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about decidability of relations and proof irrelevance


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: AUGER Cédric <sedrikov AT gmail.com>
  • Cc: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>, coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Question about decidability of relations and proof irrelevance
  • Date: Sun, 7 Apr 2013 11:51:38 -0400

Thanks, all!

-Jason


On Sun, Apr 7, 2013 at 10:52 AM, AUGER Cédric <sedrikov AT gmail.com> wrote:
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.




Archive powered by MHonArc 2.6.18.

Top of Page