search

HoTT / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
http://coq.inria.fr/
GNU Lesser General Public License v2.1
27 stars 5 forks source link

[abstract] duplicates fresh lemmas in universe polymorphic mode (polyproj) #111

Open JasonGross opened 10 years ago

JasonGross commented 10 years ago 
Set Universe Polymorphism.
Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x.
Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope.

Axioms A B : Type.
Axiom P : A = B.
Definition foo : (A = B) * (A = B).
split; abstract (rewrite <- P; reflexivity).
(* Error: internal_paths_rew already exists. *)
Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)

This is the universe polymorphism version of #110. Might also be related to #108.

JasonGross commented 10 years ago

Here's a slightly simpler example:

Set Universe Polymorphism.
Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x.
Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope.

Axioms A B : Type.
Axiom P : A = B.
Definition foo : A = B.
abstract (rewrite <- P; reflexivity).
(* Error: internal_paths_rew already exists. *)
Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)