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/closed | |
parent | 8059a0efa79fcd72d56c424adf1bea10dae28d6d (diff) |
Fix the status of some resolved bugs
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r-- | test-suite/bugs/closed/1501.v | 67 | ||||
-rw-r--r-- | test-suite/bugs/closed/2456.v | 58 | ||||
-rw-r--r-- | test-suite/bugs/closed/2814.v | 6 | ||||
-rw-r--r-- | test-suite/bugs/closed/3100.v | 9 | ||||
-rw-r--r-- | test-suite/bugs/closed/3230.v | 14 | ||||
-rw-r--r-- | test-suite/bugs/closed/3320.v | 5 |
6 files changed, 159 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/1501.v b/test-suite/bugs/closed/1501.v new file mode 100644 index 000000000..e771e192d --- /dev/null +++ b/test-suite/bugs/closed/1501.v @@ -0,0 +1,67 @@ +Set Implicit Arguments. + + +Require Export Relation_Definitions. +Require Export Setoid. +Require Import Morphisms. + + +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. + +Add Parametric Relation A : (K A) (@equiv A) + reflexivity proved by (@equiv_refl A) + symmetry proved by (@equiv_sym A) + transitivity proved by (@equiv_trans A) + as equiv_rel. + +Add Parametric Morphism A B : (@bind A B) + with signature (@equiv A) ==> (pointwise_relation A (@equiv B)) ==> (@equiv B) + as bind_mor. +Proof. + unfold pointwise_relation; intros; 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 *) + setoid_rewrite H2. + reflexivity. +Qed. diff --git a/test-suite/bugs/closed/2456.v b/test-suite/bugs/closed/2456.v new file mode 100644 index 000000000..e5a392c4d --- /dev/null +++ b/test-suite/bugs/closed/2456.v @@ -0,0 +1,58 @@ + +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. +revert X. +dependent destruction commute1; +dependent destruction catchCommuteDetails; +dependent destruction commute2; +dependent destruction catchCommuteDetails. +Abort. diff --git a/test-suite/bugs/closed/2814.v b/test-suite/bugs/closed/2814.v new file mode 100644 index 000000000..99da1e3e4 --- /dev/null +++ b/test-suite/bugs/closed/2814.v @@ -0,0 +1,6 @@ +Require Import Program. + +Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False. + intros. + Fail induction H. +Abort. diff --git a/test-suite/bugs/closed/3100.v b/test-suite/bugs/closed/3100.v new file mode 100644 index 000000000..6f35a74dc --- /dev/null +++ b/test-suite/bugs/closed/3100.v @@ -0,0 +1,9 @@ +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/closed/3230.v b/test-suite/bugs/closed/3230.v new file mode 100644 index 000000000..265310b1a --- /dev/null +++ b/test-suite/bugs/closed/3230.v @@ -0,0 +1,14 @@ +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/closed/3320.v b/test-suite/bugs/closed/3320.v new file mode 100644 index 000000000..0aac3c1b0 --- /dev/null +++ b/test-suite/bugs/closed/3320.v @@ -0,0 +1,5 @@ +Goal forall x : nat, True. + fix 1. + assumption. +Fail Qed. +Undo. |