Quelle bug_7015.v Sprache: Coq

Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Set Printing Universes.

Module Simple.

  (* in the real world foo@{i} might be [@paths@{i} nat] I guess *)
  Inductive foo : nat -> Type :=.

  (* on [refl (fun x => f x)] this computes to [refl f] *)
  Definition eta_out {A B} (f g : forall x : A, B x) (e : (fun x => f x) = (fun x => g x)) : f = g.
  Proof.
    change (f = g) in e. destruct e;reflexivity.
  Defined.

  Section univs.
    Universes i j.
    Constraint i < j. (* fail instead of forcing equality *)

    Definition one : (fun n => foo@{i} n) = fun n => foo@{j} n := eq_refl.

    Definition two : foo@{i} = foo@{j} := eta_out _ _ one.

    Definition two' : foo@{i} = foo@{j} := Eval compute in two.

    Definition three := @eq_refl (foo@{i} = foo@{j}) two.
    Definition four := Eval compute in three.

    Definition five : foo@{i} = foo@{j} := eq_refl.
  End univs.

  (* inference tries and succeeds with syntactic equality which doesn't eta expand *)
  Fail Definition infer@{i j k|i < k, j < k, k < eq.u0}
    : foo@{i} = foo@{j} :> (nat -> Type@{k})
    := eq_refl.

End Simple.

Module WithRed.
  (** this test needs to reduce the parameter's type to work *)

  Inductive foo@{i j} (b:bool) (x:if b return Type@{j} then Type@{i} else nat) : Type@{i} := .

  (* on [refl (fun x => f x)] this computes to [refl f] *)
  Definition eta_out {A B} (f g : forall x : A, B x) (e : (fun x => f x) = (fun x => g x)) : f = g.
  Proof.
    change (f = g) in e. destruct e;reflexivity.
  Defined.

  Section univs.
    Universes i j k.
    Constraint i < j. (* fail instead of forcing equality *)

    Definition one : (fun n => foo@{i k} false n) = fun n => foo@{j k} false n := eq_refl.

    Definition two : foo@{i k} false = foo@{j k} false := eta_out _ _ one.

    Definition two' : foo@{i k} false = foo@{j k} false := Eval compute in two.

    (* Failure of SR doesn't just mean that the type changes, sometimes
     we lose being well-typed entirely. *)
    Definition three := @eq_refl (foo@{i k} false = foo@{j k} false) two.
    Definition four := Eval compute in three.

    Definition five : foo@{i k} false = foo@{j k} false := eq_refl.
  End univs.

  (* inference tries and succeeds with syntactic equality which doesn't eta expand *)
  Fail Definition infer@{i j k|i < k, j < k, k < eq.u0}
    : foo@{i k} false = foo@{j k} false :> (nat -> Type@{k})
    := eq_refl.

End WithRed.

quality99%

¤ Dauer der Verarbeitung: 0.4 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.