The Coq mailing list

[Daniel Wyckoff <dwyckoff76 AT hotmail.com>]

(*
Dear Coq-Club,

To conclude, it works fine now that I refined the conditions.
I'm still not sure what caused that weird message, but
we're busy enough in these parlous times!  Don't sweat it.

-Daniel
*)

Require Import Basics.
Require Import ProofIrrelevance.
Require Import Setoid.

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').
intros T U x y.
destruct x as [V h1 x]. destruct y as [W h2 y].
split.
destruct h1 as [h1l | h1r]; destruct h2 as [h2l | h2r]; subst.
intro h1. injection h1 as h2.
split; auto.
intro h1.
injection h1 as h2. tauto.
intro h1. injection h1 as h2. tauto.
intro h1. injection h1 as h2. tauto.
destruct h1 as [h1l | h1r]; destruct h2 as [h2l | h2r]; subst.
intro h1. destruct h1 as [? h1]. f_equal. apply inj_pair2 in h1.
assumption.
intro h1. destruct h1 as [h1 h2]. subst.
apply inj_pair2 in h2.
subst.
assert (h2:@or_introl (U = U) (U = U) (@eq_refl Type U) =
           @or_intror (U = U) (U = U) (@eq_refl Type U)).
  apply proof_irrelevance.
rewrite h2 at 1.
reflexivity.
intro h1.
destruct h1 as [h1l h1r]. subst.
apply inj_pair2 in h1r. subst.
assert (h2:@or_introl (T = T) (T = T) (@eq_refl Type T) =
           @or_intror (T = T) (T = T) (@eq_refl Type T)).
  apply proof_irrelevance.
rewrite h2 at 1.
reflexivity.
intro h1.
destruct h1 as [? h1].
apply inj_pair2 in h1.
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)).

---

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

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)).