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

eta-expanded projections applied to arguments should be the same as non-eta-expanded projections (polyproj) #83

Closed JasonGross closed 10 years ago

JasonGross commented 10 years ago

This might subsume #79.

Set Primitive Projections.
Set Implicit Arguments.
Set Universe Polymorphism.

Record category :=
  { ob : Type }.

Goal forall C, ob C -> ob C.
intros.
generalize dependent (@ob C). 
(* 1 subgoals, subgoal 1 (ID 6)

  C : category
  X : ob C
  ============================
   Type -> ob C
(dependent evars:) *)

Undo.
generalize dependent (ob C).
(* 1 subgoals, subgoal 1 (ID 7)

  C : category
  ============================
   forall T : Type, T -> T
(dependent evars:) *)
JasonGross commented 10 years ago

Unlike #79, this is not fixed in trunk-polyproj.

mattam82 commented 10 years ago

That's a problem of matching semantics again, generalize is doing syntactic matching. Feel free to open a but report on the bugzilla.