UIP in SProp

5 files changed, 154 insertions, 0 deletions

diff --git a/test-suite/failure/uip_loop.v b/test-suite/failure/uip_loop.v
new file mode 100644
index 0000000000..5b4a88e7cc
--- /dev/null
+++ b/test-suite/failure/uip_loop.v
@@ -0,0 +1,24 @@
+Set Definitional UIP.
+
+Inductive seq {A} (a:A) : A -> SProp :=
+  srefl : seq a a.
+Arguments srefl {_ _}.
+
+(* Axiom implied by propext (so consistent) *)
+Axiom all_eq : forall (P Q:Prop), P -> Q -> seq P Q.
+
+Definition transport (P Q:Prop) (x:P) (y:Q) : Q
+  := match all_eq P Q x y with srefl => x end.
+
+Definition top : Prop := forall P : Prop, P -> P.
+
+Definition c : top :=
+  fun P p =>
+    transport
+      (top -> top)
+      P
+      (fun x : top => x (top -> top) (fun x => x) x)
+      p.
+
+Fail Timeout 1 Eval lazy in c (top -> top) (fun x => x) c.
+(* loops *)
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index ca4858d7a7..ba316ceb64 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -7,6 +7,8 @@ bli : Type
 Axioms:
 bli : Type
 Axioms:
+@seq relies on definitional UIP.
+Axioms:
 extensionality
   : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g
 Axioms:
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index 4c980fddba..71e642519c 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -45,6 +45,32 @@ Module Poly.
 
 End Poly.
 
+Module UIP.
+  Set Definitional UIP.
+
+  Inductive seq {A} (a:A) : A -> SProp :=
+    srefl : seq a a.
+  Arguments srefl {_ _}.
+
+  Definition eq_to_seq {A x y} (e:x = y :> A) : seq x y
+    := match e with eq_refl => srefl end.
+  Definition seq_to_eq {A x y} (e:seq x y) : x = y :> A
+    := match e with srefl => eq_refl end.
+
+  Definition norm {A x y} (e:x = y :> A) : x = y
+    := seq_to_eq (eq_to_seq e).
+
+  Definition norm_id {A x y} (e:x = y :> A) : norm e = e
+    := match e with eq_refl => eq_refl end.
+
+  Theorem UIP {A x y} (e e':x = y :> A) : e = e'.
+  Proof.
+    rewrite <-(norm_id e), <-(norm_id e').
+    reflexivity.
+  Defined.
+
+  Print Assumptions UIP.
+End UIP.
 
 (* The original test-case of the bug-report *)
 
diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
index 268c1880d2..d3e2749088 100644
--- a/test-suite/success/sprop.v
+++ b/test-suite/success/sprop.v
@@ -112,6 +112,7 @@ Inductive Istrue : bool -> SProp := istrue : Istrue true.
 Definition Istrue_sym (b:bool) := if b then sUnit else sEmpty.
 Definition Istrue_to_sym b (i:Istrue b) : Istrue_sym b := match i with istrue => stt end.
 
+(* We don't need primitive elimination to relevant types for this *)
 Definition Istrue_rec (P:forall b, Istrue b -> Set) (H:P true istrue) b (i:Istrue b) : P b i.
 Proof.
   destruct b.
diff --git a/test-suite/success/sprop_uip.v b/test-suite/success/sprop_uip.v
new file mode 100644
index 0000000000..508cc2be7d
--- /dev/null
+++ b/test-suite/success/sprop_uip.v
@@ -0,0 +1,101 @@
+
+Set Allow StrictProp.
+Set Definitional UIP.
+
+Set Warnings "+bad-relevance".
+
+(** Case inversion, conversion and universe polymorphism. *)
+Set Universe Polymorphism.
+Inductive IsTy@{i j} : Type@{j} -> SProp :=
+  isty : IsTy Type@{i}.
+
+Definition IsTy_rec_red@{i j+} (P:forall T : Type@{j}, IsTy@{i j} T -> Set)
+           v (e:IsTy@{i j} Type@{i})
+  : IsTy_rec P v _ e = v
+  := eq_refl.
+
+
+(** Identity! Currently we have UIP. *)
+Inductive seq {A} (a:A) : A -> SProp :=
+  srefl : seq a a.
+
+Definition transport {A} (P:A -> Type) {x y} (e:seq x y) (v:P x) : P y :=
+  match e with
+    srefl _ => v
+  end.
+
+Definition transport_refl {A} (P:A -> Type) {x} (e:seq x x) v
+  : transport P e v = v
+  := @eq_refl (P x) v.
+
+Definition id_unit (x : unit) := x.
+Definition transport_refl_id {A} (P : A -> Type) {x : A} (u : P x)
+  : P (transport (fun _ => A) (srefl _ : seq (id_unit tt) tt) x)
+  := u.
+
+(** We don't ALWAYS reduce (this uses a constant transport so that the
+    equation is well-typed) *)
+Fail Definition transport_block A B (x y:A) (e:seq x y) v
+  : transport (fun _ => B) e v = v
+  := @eq_refl B v.
+
+Inductive sBox (A:SProp) : Prop
+  := sbox : A -> sBox A.
+
+Definition transport_refl_box (A:SProp) P (x y:A) (e:seq (sbox A x) (sbox A y)) v
+  : transport P e v = v
+  := eq_refl.
+
+(** TODO? add tests for binders which aren't lambda. *)
+Definition transport_box :=
+  Eval lazy in (fun (A:SProp) P (x y:A) (e:seq (sbox A x) (sbox A y)) v =>
+                  transport P e v).
+
+Lemma transport_box_ok : transport_box = fun A P x y e v => v.
+Proof.
+  unfold transport_box.
+  match goal with |- ?x = ?x => reflexivity end.
+Qed.
+
+(** Play with UIP *)
+Lemma of_seq {A:Type} {x y:A} (p:seq x y) : x = y.
+Proof.
+  destruct p. reflexivity.
+Defined.
+
+Lemma to_seq {A:Type} {x y:A} (p: x = y) : seq x y.
+Proof.
+  destruct p. reflexivity.
+Defined.
+
+Lemma eq_srec (A:Type) (x y:A) (P:x=y->Type) : (forall e : seq x y, P (of_seq e)) -> forall e, P e.
+Proof.
+  intros H e. destruct e.
+  apply (H (srefl _)).
+Defined.
+
+Lemma K : forall {A x} (p:x=x:>A), p = eq_refl.
+Proof.
+  intros A x. apply eq_srec. intros;reflexivity.
+Defined.
+
+Definition K_refl : forall {A x}, @K A x eq_refl = eq_refl
+  := fun A x => eq_refl.
+
+Section funext.
+
+  Variable sfunext : forall {A B} (f g : A -> B), (forall x, seq (f x) (g x)) -> seq f g.
+
+  Lemma funext {A B} (f g : A -> B) (H:forall x, (f x) = (g x)) : f = g.
+  Proof.
+    apply of_seq,sfunext;intros x;apply to_seq,H.
+  Defined.
+
+  Definition funext_refl A B (f : A -> B) : funext f f (fun x => eq_refl) = eq_refl
+    := eq_refl.
+End funext.
+
+(* check that extraction doesn't fall apart on matches with special reduction *)
+Require Extraction.
+
+Extraction seq_rect.