The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

Hello list,

A development I have been working on using Coq 8.3 beta0-1 [1] contains
some pieces of Coq code that are accepted by Coq 8.3 beta0-1, but trigger
a universe inconsistency in current Coq trunk (2010-08-10).

Should I consider these as bugs in my code and find workarounds, or is
it possible that this is faulty behaviour introduced in Coq trunk?

Attached is an isolated example, but I also have some others that are
not as easily extracted consisely.

I have not pinpointed this down to a specific SVN revision, but could
if appreciated (the change was before 2010-05-10 I think).

thanks,
Martijn

[1] http://coq.inria.fr/coq-83-beta-version
Require Import Equality.


Set Implicit Arguments.


Inductive Fin : nat -> Type :=
  | First : forall n, Fin (S n)
  | Next  : forall n, Fin n -> Fin (S n).

Lemma Fin_0_inv (A : Type) : Fin 0 -> A.
inversion 1.
Qed.


Definition vector (A : Type) (n : nat) := Fin n -> A.


Definition vcast (A : Type) n (v : vector A n) m (H : n = m) : vector A m :=
  match H in (_ = m) return vector A m with
  | refl_equal => v
  end.

(** Introduce a [vcast] in a binary predicate on [A].

   This lemma introduces a universe inconsistency in Coq trunk 2010-08-10
   but not in Coq 8.3 beta0-1.

   In Coq 8.2pl1 the [dependent destruction] tactic fails. *)
Lemma vcast_intro :
  forall (A : Type) R n m (v1 v2 : vector A m) (H1 H2 : m = n) i,
    (forall i, R (v1 i) (v2 i)) ->
    R (vcast v1 H1 i) (vcast v2 H2 i).
Proof.
intros A R n m v1 v2 H1 H2 i H.
dependent destruction H1.
(** Still consistent universe... *)
dependent destruction H2.
(** Universe inconsistency *)
apply H.
Qed.