The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

I guess this is a know behaviour (and somewhat expected…), but will the
following kind of behaviour be fixed in coming versions.

(This is some kind of exploit on eta expansion)

=============================================================
Require Import Utf8.
Record Spec (A : Type) (P : A → Prop) : Type := Sp
  { element : A
  ; specification : P element
  }.

Notation "{ x 'st' P }" := (Spec _ (λ x, P)).

Inductive pos : nat → Prop := Pos : ∀ n, pos (S n).

Definition x : Spec nat pos := Sp nat pos (S O) (Pos O).
Definition y : {x st pos x} := {|specification:=Pos O|}.

Goal x = y.
split.
Qed.

Goal ∀ l, x = l → y = l.
intros.
unfold x in H.
unfold y.
(*rewrite H.*)
simpl in *.
(*rewrite H.*)
compute in *.
(*rewrite H.*)
==============================================================
I think there lacks some tactics on eta expansion.

Of course I can prove this goal using the change tactic, but I know no
otherway than change to expand/contract eta.

I know it has nothing to do with that, but will 'native' proof
irrelevance be built on a future Coq version (or more precisely will
that be planned), like it has been done for eta (I mean automatically
unify elements of same Prop without inspecting them)?

Or do some people work in theory where proof-irrelevance contradicts
the other lemmas.