From 321249f0ccc9b7b6fedbab411fac4aa443e0dd43 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 27 Feb 2015 13:25:11 +0100 Subject: Moving test of #3848 to "opened". --- test-suite/bugs/opened/3848.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 test-suite/bugs/opened/3848.v (limited to 'test-suite/bugs/opened') diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v new file mode 100644 index 0000000000..b66aeccaff --- /dev/null +++ b/test-suite/bugs/opened/3848.v @@ -0,0 +1,21 @@ +Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing). +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x. +Class IsEquiv {A B} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }. +Arguments eisretr {A B} f {_} _. +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'"). +Generalizable Variables A B f g e n. +Definition functor_forall `{P : A -> Type} `{Q : B -> Type} + (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b) +: (forall a:A, P a) -> (forall b:B, Q b). + admit. +Defined. + +Lemma isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type} + `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)} +: (forall b : B, Q b) -> forall a : A, P a. +Proof. + refine (functor_forall + (f^-1) + (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)). +Defined. (* Error: Attempt to save an incomplete proof *) -- cgit v1.2.3 From 7012d65f71752a89cded69d6c2e7045f3a7cadde Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 27 Feb 2015 13:29:11 +0100 Subject: Moving tests for #2456 and #3593 to "opened" until they're fixed. --- test-suite/bugs/opened/2456.v | 53 +++++++++++++++++++++++++++++++++++++++++++ test-suite/bugs/opened/3593.v | 10 ++++++++ 2 files changed, 63 insertions(+) create mode 100644 test-suite/bugs/opened/2456.v create mode 100644 test-suite/bugs/opened/3593.v (limited to 'test-suite/bugs/opened') diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v new file mode 100644 index 0000000000..56f046c4d7 --- /dev/null +++ b/test-suite/bugs/opened/2456.v @@ -0,0 +1,53 @@ + +Require Import Equality. + +Parameter Patch : nat -> nat -> Set. + +Inductive Catch (from to : nat) : Type + := MkCatch : forall (p : Patch from to), + Catch from to. +Implicit Arguments MkCatch [from to]. + +Inductive CatchCommute5 + : forall {from mid1 mid2 to : nat}, + Catch from mid1 + -> Catch mid1 to + -> Catch from mid2 + -> Catch mid2 to + -> Prop + := MkCatchCommute5 : + forall {from mid1 mid2 to : nat} + (p : Patch from mid1) + (q : Patch mid1 to) + (q' : Patch from mid2) + (p' : Patch mid2 to), + CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p'). + +Inductive CatchCommute {from mid1 mid2 to : nat} + (p : Catch from mid1) + (q : Catch mid1 to) + (q' : Catch from mid2) + (p' : Catch mid2 to) + : Prop + := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'), + CatchCommute p q q' p'. +Notation "<< p , q >> <~> << q' , p' >>" + := (CatchCommute p q q' p') + (at level 60, no associativity). + +Lemma CatchCommuteUnique2 : + forall {from mid mid' to : nat} + {p : Catch from mid} {q : Catch mid to} + {q' : Catch from mid'} {p' : Catch mid' to} + {q'' : Catch from mid'} {p'' : Catch mid' to} + (commute1 : <> <~> <>) + (commute2 : <> <~> <>), + (p' = p'') /\ (q' = q''). +Proof with auto. +intros. +set (X := commute2). +dependent destruction commute1; +dependent destruction catchCommuteDetails; +dependent destruction commute2; +dependent destruction catchCommuteDetails generalizing X. +Admitted. \ No newline at end of file diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/opened/3593.v new file mode 100644 index 0000000000..25f9db6b28 --- /dev/null +++ b/test-suite/bugs/opened/3593.v @@ -0,0 +1,10 @@ +Set Universe Polymorphism. +Set Printing All. +Set Implicit Arguments. +Record prod A B := pair { fst : A ; snd : B }. +Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x. +simpl; intros. + constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x). + Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). + reflexivity. +Qed. -- cgit v1.2.3 From 3248466ca57b5121e5a29bf6fd6619c512a52349 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 27 Feb 2015 16:23:36 +0100 Subject: Fix test-suite files for bugs #2456 and #3593, still open. --- test-suite/bugs/opened/2456.v | 4 ++-- test-suite/bugs/opened/3593.v | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'test-suite/bugs/opened') diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v index 56f046c4d7..6cca5c9fba 100644 --- a/test-suite/bugs/opened/2456.v +++ b/test-suite/bugs/opened/2456.v @@ -46,8 +46,8 @@ Lemma CatchCommuteUnique2 : Proof with auto. intros. set (X := commute2). -dependent destruction commute1; +Fail dependent destruction commute1; dependent destruction catchCommuteDetails; dependent destruction commute2; dependent destruction catchCommuteDetails generalizing X. -Admitted. \ No newline at end of file +Admitted. diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/opened/3593.v index 25f9db6b28..d83b900607 100644 --- a/test-suite/bugs/opened/3593.v +++ b/test-suite/bugs/opened/3593.v @@ -5,6 +5,6 @@ Record prod A B := pair { fst : A ; snd : B }. Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x. simpl; intros. constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x). - Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). + Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). reflexivity. Qed. -- cgit v1.2.3 From 926fcf01baecd01c2e46d17a31077b942d01971d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 27 Feb 2015 16:46:41 +0100 Subject: Moving test for #3467 to closed after PMP's fix. --- test-suite/bugs/opened/3467.v | 6 ------ 1 file changed, 6 deletions(-) delete mode 100644 test-suite/bugs/opened/3467.v (limited to 'test-suite/bugs/opened') diff --git a/test-suite/bugs/opened/3467.v b/test-suite/bugs/opened/3467.v deleted file mode 100644 index 900bfc34b3..0000000000 --- a/test-suite/bugs/opened/3467.v +++ /dev/null @@ -1,6 +0,0 @@ -Module foo. - Notation x := $(exact I)$. -End foo. -Module bar. - Fail Include foo. -End bar. -- cgit v1.2.3 From 1019a654a8262ee1b8b1e1a7f652a7e3d111d20e Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 27 Feb 2015 16:47:43 +0100 Subject: Fix test for #3848, still open. --- test-suite/bugs/opened/3848.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/bugs/opened') diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v index b66aeccaff..9413daa041 100644 --- a/test-suite/bugs/opened/3848.v +++ b/test-suite/bugs/opened/3848.v @@ -18,4 +18,4 @@ Proof. refine (functor_forall (f^-1) (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)). -Defined. (* Error: Attempt to save an incomplete proof *) +Fail Defined. (* Error: Attempt to save an incomplete proof *) -- cgit v1.2.3