diff options
author | Tej Chajed <tchajed@mit.edu> | 2018-01-25 17:47:12 -0500 |
---|---|---|
committer | Tej Chajed <tchajed@mit.edu> | 2018-04-11 10:50:46 -0400 |
commit | 26d9acf2418291ab740fedb91233e16445848ea1 (patch) | |
tree | 99c445bcc7400e4847e8684a8124580d60ff66a0 /test-suite/bugs/opened | |
parent | 8059a0efa79fcd72d56c424adf1bea10dae28d6d (diff) |
Fix the status of some resolved bugs
Diffstat (limited to 'test-suite/bugs/opened')
-rw-r--r-- | test-suite/bugs/opened/1501.v | 96 | ||||
-rw-r--r-- | test-suite/bugs/opened/2456.v | 53 | ||||
-rw-r--r-- | test-suite/bugs/opened/2814.v | 5 | ||||
-rw-r--r-- | test-suite/bugs/opened/3100.v | 9 | ||||
-rw-r--r-- | test-suite/bugs/opened/3209.v | 17 | ||||
-rw-r--r-- | test-suite/bugs/opened/3230.v | 14 | ||||
-rw-r--r-- | test-suite/bugs/opened/3320.v | 4 | ||||
-rw-r--r-- | test-suite/bugs/opened/3916.v | 3 | ||||
-rw-r--r-- | test-suite/bugs/opened/3948.v | 25 | ||||
-rw-r--r-- | test-suite/bugs/opened/4813.v | 4 |
10 files changed, 2 insertions, 228 deletions
diff --git a/test-suite/bugs/opened/1501.v b/test-suite/bugs/opened/1501.v deleted file mode 100644 index b36f21da1..000000000 --- a/test-suite/bugs/opened/1501.v +++ /dev/null @@ -1,96 +0,0 @@ -Set Implicit Arguments. - - -Require Export Relation_Definitions. -Require Export Setoid. - - -Section Essais. - -(* Parametrized Setoid *) -Parameter K : Type -> Type. -Parameter equiv : forall A : Type, K A -> K A -> Prop. -Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x. -Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x. -Parameter equiv_trans : forall (A : Type) (x y z : K A), equiv x y -> equiv y z --> equiv x z. - -(* basic operations *) -Parameter val : forall A : Type, A -> K A. -Parameter bind : forall A B : Type, K A -> (A -> K B) -> K B. - -Parameter - bind_compat : - forall (A B : Type) (m1 m2 : K A) (f1 f2 : A -> K B), - equiv m1 m2 -> - (forall x : A, equiv (f1 x) (f2 x)) -> equiv (bind m1 f1) (bind m2 f2). - -(* monad axioms *) -Parameter - bind_val_l : - forall (A B : Type) (a : A) (f : A -> K B), equiv (bind (val a) f) (f a). -Parameter - bind_val_r : - forall (A : Type) (m : K A), equiv (bind m (fun a => val a)) m. -Parameter - bind_assoc : - forall (A B C : Type) (m : K A) (f : A -> K B) (g : B -> K C), - equiv (bind (bind m f) g) (bind m (fun a => bind (f a) g)). - - -Hint Resolve equiv_refl equiv_sym equiv_trans: monad. - -Instance equiv_rel A: Equivalence (@equiv A). -Proof. - constructor. - intros xa; apply equiv_refl. - intros xa xb; apply equiv_sym. - intros xa xb xc; apply equiv_trans. -Defined. - -Definition fequiv (A B: Type) (f g: A -> K B) := forall (x:A), (equiv (f x) (g -x)). - -Lemma fequiv_refl : forall (A B: Type) (f : A -> K B), fequiv f f. -Proof. - unfold fequiv; auto with monad. -Qed. - -Lemma fequiv_sym : forall (A B: Type) (x y : A -> K B), fequiv x y -> fequiv y -x. -Proof. - unfold fequiv; auto with monad. -Qed. - -Lemma fequiv_trans : forall (A B: Type) (x y z : A -> K B), fequiv x y -> -fequiv -y z -> fequiv x z. -Proof. - unfold fequiv; intros; eapply equiv_trans; auto with monad. -Qed. - -Instance fequiv_re A B: Equivalence (@fequiv A B). -Proof. - constructor. - intros f; apply fequiv_refl. - intros f g; apply fequiv_sym. - intros f g h; apply fequiv_trans. -Defined. - -Instance bind_mor A B: Morphisms.Proper (@equiv _ ==> @fequiv _ _ ==> @equiv _) (@bind A B). -Proof. - unfold fequiv; intros x y xy_equiv f g fg_equiv; apply bind_compat; auto. -Qed. - -Lemma test: - forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B), - (equiv m1 m2) -> (equiv m2 m3) -> - equiv (bind m1 (fun a => bind m2 (fun a' => f a a'))) - (bind m2 (fun a => bind m3 (fun a' => f a a'))). -Proof. - intros A B m1 m2 m3 f H1 H2. - setoid_rewrite H1. (* this works *) - Fail setoid_rewrite H2. -Abort. -(* trivial by equiv_refl. -Qed.*) diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v deleted file mode 100644 index 5294adefd..000000000 --- a/test-suite/bugs/opened/2456.v +++ /dev/null @@ -1,53 +0,0 @@ - -Require Import Equality. - -Parameter Patch : nat -> nat -> Set. - -Inductive Catch (from to : nat) : Type - := MkCatch : forall (p : Patch from to), - Catch from to. -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 : <<p, q>> <~> <<q', p'>>) - (commute2 : <<p, q>> <~> <<q'', p''>>), - (p' = p'') /\ (q' = q''). -Proof with auto. -intros. -set (X := commute2). -Fail dependent destruction commute1; -dependent destruction catchCommuteDetails; -dependent destruction commute2; -dependent destruction catchCommuteDetails generalizing X. -Admitted. diff --git a/test-suite/bugs/opened/2814.v b/test-suite/bugs/opened/2814.v deleted file mode 100644 index a740b4384..000000000 --- a/test-suite/bugs/opened/2814.v +++ /dev/null @@ -1,5 +0,0 @@ -Require Import Program. - -Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False. - intros. - Fail induction H. diff --git a/test-suite/bugs/opened/3100.v b/test-suite/bugs/opened/3100.v deleted file mode 100644 index 6f35a74dc..000000000 --- a/test-suite/bugs/opened/3100.v +++ /dev/null @@ -1,9 +0,0 @@ -Fixpoint F (n : nat) (A : Type) : Type := - match n with - | 0 => True - | S n => forall (x : A), F n (x = x) - end. - -Goal forall A n, (forall (x : A) (e : x = x), F n (e = e)). -intros A n. -Fail change (forall x, F n (x = x)) with (F (S n)). diff --git a/test-suite/bugs/opened/3209.v b/test-suite/bugs/opened/3209.v deleted file mode 100644 index 3203afa13..000000000 --- a/test-suite/bugs/opened/3209.v +++ /dev/null @@ -1,17 +0,0 @@ -Inductive eqT {A} (x : A) : A -> Type := - reflT : eqT x x. -Definition Bi_inv (A B : Type) (f : (A -> B)) := - sigT (fun (g : B -> A) => - sigT (fun (h : B -> A) => - sigT (fun (α : forall b : B, eqT (f (g b)) b) => - forall a : A, eqT (h (f a)) a))). -Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f). - -Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B). -Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B := - sigT_rect (fun _ => TEquiv A B) - (fun (f : TEquiv A B -> eqT A B) H => - sigT_rect (fun _ => TEquiv A B) - (fun g _ => g e) - H) - (UA A B). diff --git a/test-suite/bugs/opened/3230.v b/test-suite/bugs/opened/3230.v deleted file mode 100644 index 265310b1a..000000000 --- a/test-suite/bugs/opened/3230.v +++ /dev/null @@ -1,14 +0,0 @@ -Structure type : Type := Pack { ob : Type }. -Polymorphic Record category := { foo : Type }. -Definition FuncComp := Pack category. -Axiom C : category. - -Check (C : ob FuncComp). (* OK *) - -Canonical Structure FuncComp. - -Check (C : ob FuncComp). -(* Toplevel input, characters 15-39: -Error: -The term "C" has type "category" while it is expected to have type - "ob FuncComp". *) diff --git a/test-suite/bugs/opened/3320.v b/test-suite/bugs/opened/3320.v deleted file mode 100644 index 05cf73281..000000000 --- a/test-suite/bugs/opened/3320.v +++ /dev/null @@ -1,4 +0,0 @@ -Goal forall x : nat, True. - fix 1. - assumption. -Fail Qed. diff --git a/test-suite/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v deleted file mode 100644 index fd95503e6..000000000 --- a/test-suite/bugs/opened/3916.v +++ /dev/null @@ -1,3 +0,0 @@ -Require Import List. - -Fail Hint Resolve -> in_map. (* Also happens when using <- instead of -> *) diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v deleted file mode 100644 index 5c4b4277b..000000000 --- a/test-suite/bugs/opened/3948.v +++ /dev/null @@ -1,25 +0,0 @@ -Module Type S. -Parameter t : Type. -End S. - -Module Bar(X : S). -Proof. - Definition elt := X.t. - Axiom fold : elt. -End Bar. - -Module Make (X: S) := Bar(X). - -Declare Module X : S. - -Module Type Interface. - Parameter constant : unit. -End Interface. - -Module DepMap : Interface. - Module Dom := Make(X). - Definition constant : unit := - let _ := @Dom.fold in tt. -End DepMap. - -Print Assumptions DepMap.constant. diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v index b75170179..2ac553593 100644 --- a/test-suite/bugs/opened/4813.v +++ b/test-suite/bugs/opened/4813.v @@ -1,5 +1,5 @@ -(* An example one would like to see succeeding *) +Require Import Program.Tactics. Record T := BT { t : Set }. Record U (x : T) := BU { u : t x -> Prop }. -Fail Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. +Program Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. |