From d8825650bd2b7855a92195c032a539aa3f09c9ef Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 8 Jun 2016 17:33:12 -0400 Subject: Unbreak singleton list-like notation (-compat 8.4) With this commit, it is possible to write notations so that singleton lists are usable in both 8.4 and 8.5pl1 -compat. Longer lists await the ability to remove notations from the parser. --- test-suite/bugs/closed/4684.v | 32 ++++++++++++++++++++++++++ test-suite/bugs/closed/4733.v | 52 +++++++++++++++++++++++++++++++++++++++++++ test-suite/bugs/opened/4803.v | 34 ++++++++++++++++++++++++++++ 3 files changed, 118 insertions(+) create mode 100644 test-suite/bugs/closed/4684.v create mode 100644 test-suite/bugs/closed/4733.v create mode 100644 test-suite/bugs/opened/4803.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4684.v b/test-suite/bugs/closed/4684.v new file mode 100644 index 0000000000..9c0bed42c4 --- /dev/null +++ b/test-suite/bugs/closed/4684.v @@ -0,0 +1,32 @@ +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. + +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v new file mode 100644 index 0000000000..ac0653492a --- /dev/null +++ b/test-suite/bugs/closed/4733.v @@ -0,0 +1,52 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. + +(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) + +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. +(* Now these all work, but not so in 8.4. If we get the ability to remove notations, and the above fails can be removed, this section can also just be removed. *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v new file mode 100644 index 0000000000..3ca5c095f5 --- /dev/null +++ b/test-suite/bugs/opened/4803.v @@ -0,0 +1,34 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. + +(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser; it should be added to Compat/Coq84.v *) +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) -- cgit v1.2.3 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 From 57021d22fabb33b281af4de8f3946cb4424c6422 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 5 Jul 2016 18:28:24 +0200 Subject: congruence fix: test-suite code and update CHANGES This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718. --- test-suite/bugs/closed/4069.v | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 11289f7575..61527764e2 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -87,4 +87,18 @@ f_equal. Undo 2. unshelve refine (tequator (X _)); revgoals. f_equal. -Admitted. \ No newline at end of file +Admitted. + +Goal @eq Set nat nat. +congruence. +Qed. + +Goal @eq Type nat nat. +congruence. +Qed. + +Variable T : Type. + +Goal @eq Type T T. +congruence. +Qed. \ No newline at end of file -- cgit v1.2.3 From 0bbc652fc15e1c27b20d3288205079ff295e21da Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 6 Jul 2016 17:37:46 +0200 Subject: Update csdp.cache. --- test-suite/csdp.cache | Bin 76555 -> 79491 bytes 1 file changed, 0 insertions(+), 0 deletions(-) (limited to 'test-suite') diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache index 297ac255d3..75dd38fde8 100644 Binary files a/test-suite/csdp.cache and b/test-suite/csdp.cache differ -- cgit v1.2.3