From a5b631f7260e7d29defd8bd5c67db543742c9ecd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 17:40:04 +0200
Subject: congruence/univs: properly refresh (fix #4609)

In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
---
 test-suite/bugs/closed/4069.v   | 39 +++++++++++++++++++++++++++++++++++++++
 test-suite/success/congruence.v | 21 +++++++++++++++++++++
 2 files changed, 60 insertions(+)
 create mode 100644 test-suite/success/congruence.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v
index 21b03ce541..11289f7575 100644
--- a/test-suite/bugs/closed/4069.v
+++ b/test-suite/bugs/closed/4069.v
@@ -49,3 +49,42 @@ Lemma bar {A} n m (x : A) :
   skipn n (replicate m x) = replicate (m - n) x.
 Proof. intros. f_equal.
 (* 8.5: one goal, n = m - n *)
+Abort.
+
+Variable F : nat -> Set.
+Variable X : forall n, F (n + 1).
+
+Definition sequator{X Y: Set}{eq:X=Y}(x:X) : Y := eq_rec _ _ x _ eq.
+Definition tequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq.
+Polymorphic Definition pequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq.
+
+Goal {n:nat & F (S n)}.
+eexists.
+unshelve eapply (sequator (X _)).
+f_equal. (*behaves*)
+Undo 2.
+unshelve eapply (pequator (X _)).
+f_equal. (*behaves*)
+Undo 2.
+unshelve eapply (tequator (X _)).
+f_equal. (*behaves now *)
+Focus 2. exact 0.
+simpl.
+reflexivity.
+Defined.
+
+(* Part 2: modulo casts introduced by refine due to reductions in goals *)
+
+Goal {n:nat & F (S n)}.
+eexists.
+(*misbehaves, although same goal as above*)
+Set Printing All.
+unshelve refine (sequator (X _)); revgoals.
+2:exact 0. reflexivity.
+Undo 3. 
+unshelve refine (pequator (X _)); revgoals.
+f_equal.
+Undo 2.
+unshelve refine (tequator (X _)); revgoals.
+f_equal.
+Admitted.
\ No newline at end of file
diff --git a/test-suite/success/congruence.v b/test-suite/success/congruence.v
new file mode 100644
index 0000000000..873d2f9f7e
--- /dev/null
+++ b/test-suite/success/congruence.v
@@ -0,0 +1,21 @@
+(* Example by Jonathan Leivant, congruence and tauto up to universes *)
+Variables S1 S2 : Set.
+
+Goal @eq Type S1 S2 -> @eq Type S1 S2.
+intro H.
+tauto.
+Qed.
+
+Definition T1 : Type := S1.
+Definition T2 : Type := S2.
+
+Goal T1 = T1.
+congruence.
+Undo.
+tauto.
+Undo.
+unfold T1.
+congruence.
+Undo.
+tauto.
+Qed.
-- 
cgit v1.2.3


From 71d4c435e42c24c21ae43f0ddcc7a71bee1009f5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 18:31:01 +0200
Subject: congruence: Restrict refreshing to Set

Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
---
 test-suite/success/cc.v         | 14 ++++++++++++++
 test-suite/success/congruence.v | 21 ---------------------
 2 files changed, 14 insertions(+), 21 deletions(-)
 delete mode 100644 test-suite/success/congruence.v

(limited to 'test-suite')

diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index a70d919635..0b0e93eb56 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -131,3 +131,17 @@ End bug_2447.
 
 
 
+(* Example by Jonathan Leivant, congruence up to universes *)
+Section JLeivant.
+  Variables S1 S2 : Set.
+
+  Definition T1 : Type := S1.
+  Definition T2 : Type := S2.
+
+  Goal T1 = T1.
+    congruence.
+    Undo.
+    unfold T1.
+    congruence.
+  Qed.
+End JLeivant.
diff --git a/test-suite/success/congruence.v b/test-suite/success/congruence.v
deleted file mode 100644
index 873d2f9f7e..0000000000
--- a/test-suite/success/congruence.v
+++ /dev/null
@@ -1,21 +0,0 @@
-(* Example by Jonathan Leivant, congruence and tauto up to universes *)
-Variables S1 S2 : Set.
-
-Goal @eq Type S1 S2 -> @eq Type S1 S2.
-intro H.
-tauto.
-Qed.
-
-Definition T1 : Type := S1.
-Definition T2 : Type := S2.
-
-Goal T1 = T1.
-congruence.
-Undo.
-tauto.
-Undo.
-unfold T1.
-congruence.
-Undo.
-tauto.
-Qed.
-- 
cgit v1.2.3