Quelle bug_6661.v Sprache: Coq

(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter" "-w" "-notation-overridden,-deprecated-option") -*- *)
(*
    The Coq Proof Assistant, version 8.7.1 (January 2018)
    compiled on Jan 21 2018 15:02:24 with OCaml 4.06.0
    from commit 391bb5e196901a3a9426295125b8d1c700ab6992
*)

Require Export Corelib.Init.Notations.
Require Export Corelib.Init.Ltac.
Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..)
  (at level 200, x binder, y binder, right associativity) : type_scope.
Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
  (at level 200, x binder, y binder, right associativity).
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Reserved Notation "p @ q" (at level 60, right associativity).
Reserved Notation "! p " (at level 50).

Monomorphic Universe uu.
Monomorphic Universe uu0.
Monomorphic Universe uu1.
Constraint uu0 < uu1.

Global Set Universe Polymorphism.
Global Set Polymorphic Inductive Cumulativity.
Global Unset Universe Minimization ToSet.

Notation UU  := Type (only parsing).
Notation UU0 := Type@{uu0} (only parsing).

Global Set Printing Universes.

Inductive unit : UU0 := tt : unit.

Inductive paths@{i} {A:Type@{i}} (a:A) : A -> Type@{i} := idpath : paths a a.
#[export] Hint Resolve idpath : core .
Notation "a = b" := (paths a b) (at level 70, no associativity) : type_scope.

Set Primitive Projections.
Set Nonrecursive Elimination Schemes.

Record total2@{i} { T: Type@{i} } ( P: T -> Type@{i} ) : Type@{i}
  := tpair { pr1 : T; pr2 : P pr1 }.

Arguments tpair {_} _ _ _.
Arguments pr1 {_ _} _.
Arguments pr2 {_ _} _.

Notation "'∑' x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..))
  (at level 200, x binder, y binder, right associativity) : type_scope.

Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X.
  induction xy as [x y].
  exact x.
Defined.

Definition idfun (T : UU) := λ t:T, t.

Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c.
Proof.
  intros. induction e1. exact e2.
Defined.

#[export] Hint Resolve @pathscomp0 : pathshints.

Notation "p @ q" := (pathscomp0 p q).

Definition pathsinv0 {X : UU} {a b : X} (e : a = b) : b = a.
Proof.
  intros. induction e. exact (idpath _).
Defined.

Notation "! p " := (pathsinv0 p).

Definition maponpaths {T1 T2 : UU} (f : T1 -> T2) {t1 t2 : T1}
           (e: t1 = t2) : f t1 = f t2.
Proof.
  intros. induction e. exact (idpath _).
Defined.

Definition map_on_two_paths {X Y Z : UU} (f : X -> Y -> Z) {x x' y y'} (ex : x = x') (ey: y = y') :
  f x y = f x' y'.
Proof.
  intros. induction ex. induction ey. exact (idpath _).
Defined.

Definition maponpathscomp0 {X Y : UU} {x1 x2 x3 : X}
           (f : X -> Y) (e1 : x1 = x2) (e2 : x2 = x3) :
  maponpaths f (e1 @ e2) = maponpaths f e1 @ maponpaths f e2.
Proof.
  intros. induction e1. induction e2. exact (idpath _).
Defined.

Definition maponpathsinv0 {X Y : UU} (f : X -> Y)
           {x1 x2 : X} (e : x1 = x2) : maponpaths f (! e) = ! (maponpaths f e).
Proof.
  intros. induction e. exact (idpath _).
Defined.

Definition constr1 {X : UU} (P : X -> UU) {x x' : X} (e : x = x') :
  ∑ (f : P x -> P x'),
  ∑ (ee : ∏ p : P x, tpair _ x p = tpair _ x' (f p)),
  ∏ (pp : P x), maponpaths pr1 (ee pp) = e.
Proof.
  intros. induction e.
  split with (idfun (P x)).
  split with (λ p, idpath _).
  unfold maponpaths. simpl.
  intro. exact (idpath _).
Defined.

Definition transportf@{i} {X : Type@{i}} (P : X -> Type@{i}) {x x' : X}
           (e : x = x') : P x -> P x' := pr1 (constr1 P e).

Lemma two_arg_paths_f@{i} {A : Type@{i}} {B : A -> Type@{i}} {C:Type@{i}} {f : ∏ a, B a -> C} {a1 b1 a2 b2}
      (p : a1 = a2) (q : transportf B p b1 = b2) : f a1 b1 = f a2 b2.
Proof.
  intros. induction p. induction q. exact (idpath _).
Defined.

Definition iscontr@{i} (T:Type@{i}) : Type@{i} := ∑ cntr:T, ∏ t:T, t=cntr.

Lemma proofirrelevancecontr {X : UU} (is : iscontr X) (x x' : X) : x = x'.
Proof.
  intros.
  induction is as [y fe].
  exact (fe x @ !(fe x')).
Defined.

Definition hfiber@{i} {X Y : Type@{i}} (f : X -> Y) (y : Y) : Type@{i} := total2 (λ x, f x = y).

Definition hfiberpair {X Y : UU} (f : X -> Y) {y : Y}
           (x : X) (e : f x = y) : hfiber f y :=
  tpair _ x e.

Definition coconustot (T : UU) (t : T) := ∑ t' : T, t' = t.

Definition coconustotpair (T : UU) {t t' : T} (e: t' = t) : coconustot T t
  := tpair _ t' e.

Lemma connectedcoconustot {T : UU} {t : T} (c1 c2 : coconustot T t) : c1 = c2.
Proof.
  intros.
  induction c1 as [x0 x].
  induction x.
  induction c2 as [x1 y].
  induction y.
  exact (idpath _).
Defined.

Definition isweq@{i} {X Y : Type@{i}} (f : X -> Y) : Type@{i} :=
  ∏ y : Y, iscontr (hfiber f y).

Lemma isProofIrrelevantUnit : ∏ x x' : unit, x = x'.
Proof.
  intros. induction x. induction x'. exact (idpath _).
Defined.

Lemma unitl0 : tt = tt -> coconustot _ tt.
Proof.
  intros e. exact (coconustotpair unit e).
Defined.

Lemma unitl1: coconustot _ tt -> tt = tt.
Proof.
  intro cp. induction cp as [x t]. induction x. exact t.
Defined.

Lemma unitl2: ∏ e : tt = tt, unitl1 (unitl0 e) = e.
Proof.
  intros. unfold unitl0. simpl. exact (idpath _).
Defined.

Lemma unitl3: ∏ e : tt = tt, e = idpath tt.
Proof.
  intros.

  assert (e0 : unitl0 (idpath tt) = unitl0 e).
  { simple refine (connectedcoconustot _ _). }

  set (e1 := maponpaths unitl1 e0).

  exact (! (unitl2 e) @ (! e1) @ (unitl2 (idpath _))).
Defined.

Theorem iscontrpathsinunit (x x' : unit) : iscontr (x = x').
Proof.
  intros.
  split with (isProofIrrelevantUnit x x').
  intros e'.
  induction x.
  induction x'.
  simpl.
  apply unitl3.
Qed.

Lemma ifcontrthenunitl0 (e1 e2 : tt = tt) : e1 = e2.
Proof.
  intros.
  simple refine (proofirrelevancecontr _ _ _).
  exact (iscontrpathsinunit tt tt).
Qed.

Section isweqcontrtounit.

  Universe i.

  (* To see the bug, run it both with and without this constraint: *)

  (* Constraint uu0 < i. *)

  (* Without this constraint, we get i = uu0 in the next definition *)
  Lemma isweqcontrtounit@{} {T : Type@{i}} (is : iscontr@{i} T) : isweq@{i} (λ _:T, tt).
  Proof.
    intros. intro y. induction y.
    induction is as [c h].
    split with (hfiberpair@{i i i} _ c (idpath tt)).
    intros ha.
    induction ha as [x e].
    simple refine (two_arg_paths_f (h x) _).
    simple refine (ifcontrthenunitl0 _ _).
  Defined.

  (*
     Explanation of the bug:

     With the constraint uu0 < i above we get:

            |= uu0 <= bug.3
               uu0 <= i
               uu1 <= i
               i <= bug.3

     from this print statement: *)

         Print isweqcontrtounit.

  (*

     Without the constraint uu0 < i above we get:

            |= i <= bug.3
               uu0 = i

     Since uu0 = i is not inferred when we impose the constraint uu0 < i,
     it is invalid to infer it when we don't.

   *)

  Context (X : Type@{uu1}).

  Check (@isweqcontrtounit X). (* detect a universe inconsistency *)

End isweqcontrtounit.

quality99%

¤ Dauer der Verarbeitung: 0.8 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.