The Coq mailing list

[Daniel Wyckoff <dwyckoff76 AT hotmail.com>]

I stand by the first e-mail.  I couldn't refine it.  No hurry, and sorry for the last two irrelevant e-mails.
-Daniel

---

From: dwyckoff76 AT hotmail.com
To: coq-club AT inria.fr
Date: Wed, 5 Aug 2015 00:17:18 +0000
Subject: RE: [Coq-Club] Universe inconsistency message after two unrelated proof scripts.

In my haste, I just realized that my conditions in [uniont_eq_iff] are kind of redundant, so I think I can eliminate my need for [inj_pair2], but
I guess I was in a hurry because of the unrelatedness of the two.

I'm pretty sure that'll fix it,
but any comments are still welcome.

-Daniel

---

From: dwyckoff76 AT hotmail.com
To: coq-club AT inria.fr
Date: Tue, 4 Aug 2015 23:41:47 +0000
Subject: [Coq-Club] Universe inconsistency message after two unrelated proof scripts.

(*
Dear Coq-Club,

In my ongoing Boolean algebras development at
http://cvs.savannah.gnu.org/viewvc/bool2/?root=bool2
I came to the point where I needed to define the union
of a directed family of algebras (not necessarily subalgebras),
and had to do define a non-necessarily-disjoint union for 
types ([uniont] below).
Anyway, the below code yields a universe inconsistency
when compiled on Coq 8.4pl6.  But if I comment out
[uniont_eq_iff], then it works fine.  But [uniont_eq_iff] compiles
fine also.  It's just the combination of
[uniont_eq_iff] and the unrelated [includedt_transfer] 
that causes 
the universe consistency. I don't know if it's as a result
of some metatheory related to my use of [inj_pair2] or a bug.
I guess I'm confused because I never thought that one completed
proof script can affect another unrelated completed proof script.

Thanks so much,
-Daniel Wyckoff
*)

Require Import Basics.
Require Import ProofIrrelevance.

Definition transfer {T U:Type} (pf:T=U) (x:T) : U.
revert x. rewrite pf. intro u. refine u.
Defined.

Inductive uniont (T U:Type) : Type :=
  uniont_intro : forall V:Type,
                   V = T \/ V = U ->
                   forall x:V, uniont T U.


Lemma uniont_eq_iff : 
  forall {T U:Type} (x y:uniont T U),
    let (V, _, x') := x in
    let (W, _, y') := y in 
    x = y <->
    ((V = W /\
     existT id _ x' = existT id _ y')
    \/ 
    (exists (pfv:V = T) (pfw:W = T),
       transfer pfv x' = transfer pfw y') 
    \/
    (exists (pfv:V = U) (pfw:W = U),
       transfer pfv x' = transfer pfw y')).
intros T U x y.
destruct x as [V h1 x'].  destruct y as [W h2 y'].
split.
intro h3.
destruct h1 as [h1l | h1r]. subst.
injection h3 as h4. intro h5. left; auto.
subst.
injection h3 as h4. intro h5. left; auto.
intro h3.
destruct h3 as [h4 | h5].
destruct h4 as [h4l h4r].
subst.
assert (h5:h1 = h2). apply proof_irrelevance.
subst.
apply inj_pair2 in h4r. subst.
reflexivity.
destruct h5 as [h5 | h6].
destruct h5 as [h5 h6]. destruct h6 as [h6 h7]. subst.
unfold transfer in h7. unfold eq_rect_r in h7. simpl in h7.
subst.
assert (h3:h1 = h2). apply proof_irrelevance. subst.
reflexivity.
destruct h6 as [h6 h7]. destruct h7 as [h7 h8]. subst.
unfold transfer in h8. unfold eq_rect_r in h8. simpl in h8.
subst.
assert (h3:h1 = h2). apply proof_irrelevance. subst.
reflexivity.
Qed.

Definition includedt (T U:Type) : Prop :=
  uniont T U = U.


Definition includedt_transfer {T U:Type} (pf:includedt T U) (x:T) :=
  (transfer pf (uniont_intro T U T (or_introl (T=U) (eq_refl T)) x)).