diff options
| -rw-r--r-- | test-suite/bugs/opened/3944.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/opened/3946.v | 11 | ||||
| -rw-r--r-- | test-suite/bugs/opened/3948.v | 70 | ||||
| -rw-r--r-- | test-suite/bugs/opened/3953.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/opened/3956.v | 141 |
5 files changed, 230 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3944.v b/test-suite/bugs/opened/3944.v new file mode 100644 index 000000000..3d0deb4c5 --- /dev/null +++ b/test-suite/bugs/opened/3944.v @@ -0,0 +1,4 @@ +Require Import Setoid. +Class C (T : Type) := c : T. +Goal forall T (i : C T) (v : T), True. +setoid_rewrite plus_n_Sm. diff --git a/test-suite/bugs/opened/3946.v b/test-suite/bugs/opened/3946.v new file mode 100644 index 000000000..e77bdbc65 --- /dev/null +++ b/test-suite/bugs/opened/3946.v @@ -0,0 +1,11 @@ +Require Import ZArith. + +Inductive foo := Foo : Z.le 0 1 -> foo. + +Definition bar (f : foo) := let (f) := f in f. + +(* Doesn't work: *) +(* Arguments bar f.*) + +(* Does work *) +Arguments bar f _. diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v new file mode 100644 index 000000000..e5bca6e52 --- /dev/null +++ b/test-suite/bugs/opened/3948.v @@ -0,0 +1,70 @@ +Require Import MSets. +Require Import Utf8. +Require FMaps. +Import Orders. + +Set Implicit Arguments. + +(* Conversion between the two kinds of OrderedType. *) +Module OTconvert (O : OrderedType) : OrderedType.OrderedType + with Definition t := O.t + with Definition eq := O.eq + with Definition lt := O.lt. + + Definition t := O.t. + Definition eq := O.eq. + Definition lt := O.lt. + Definition eq_refl := reflexivity. + Lemma eq_sym : forall x y : t, eq x y -> eq y x. + Admitted. + Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + Admitted. + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Admitted. + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Admitted. + Lemma compare : forall x y : t, OrderedType.Compare lt eq x y. + Admitted. + Definition eq_dec := O.eq_dec. +End OTconvert. + +(* Dependent Maps *) +Module Type Interface (X : OrderedType). + Module Dom : MSetInterface.SetsOn(X) with Definition elt := X.t := MSetAVL.Make(X). + Definition key := X.t. + Parameter t : forall (A : Type) (dom : Dom.t), Type. + Parameter constant : forall A dom, A -> t A dom. +End Interface. + +Module DepMap (X : OrderedType) : (Interface X) with Definition key := X.t. + Module Dom := MSetAVL.Make(X). + Module XOT := OTconvert X. + Module S := FMapList.Make(XOT). + Definition key := X.t. + Definition OK {A} dom (map : S.t A) := ∀ x, S.In x map <-> Dom.In x dom. + Definition t := fun A dom => { map : S.t A | OK dom map}. + Corollary constant_OK : forall A dom v, OK dom (Dom.fold (fun x m => S.add x v m) dom (S.empty A)). + Admitted. + Definition constant (A : Type) dom (v : A) : t A dom := + exist (OK dom) (Dom.fold (fun x m => S.add x v m) dom (@S.empty A)) (constant_OK dom v). +End DepMap. + + +Declare Module Signal : OrderedType. +Module S := DepMap(Signal). +Notation "∅" := (S.constant _ false). + +Definition I2Kt {dom} (E : S.t (option bool) dom) : S.t bool dom := S.constant dom false. +Arguments I2Kt {dom} E. + +Inductive cmd := nothing. + +Definition semantics (A T₁ T₂ : Type) := forall dom, T₁ -> S.t A dom -> S.t A dom -> nat -> T₂ -> Prop. + +Inductive LBS : semantics bool cmd cmd := LBSnothing dom (E : S.t bool dom) : LBS nothing E ∅ 0 nothing. + +Theorem CBS_LBS : forall dom p (E E' : S.t _ dom) k p', LBS p (I2Kt E) (I2Kt E') k p'. +admit. +Defined. + +Print Assumptions CBS_LBS. diff --git a/test-suite/bugs/opened/3953.v b/test-suite/bugs/opened/3953.v new file mode 100644 index 000000000..d90ae31e8 --- /dev/null +++ b/test-suite/bugs/opened/3953.v @@ -0,0 +1,4 @@ +Goal forall (a b : unit), a = b -> exists c, b = c. +intros. +eexists. +Fail subst. diff --git a/test-suite/bugs/opened/3956.v b/test-suite/bugs/opened/3956.v new file mode 100644 index 000000000..94c0c6744 --- /dev/null +++ b/test-suite/bugs/opened/3956.v @@ -0,0 +1,141 @@ +(* -*- mode: coq; mode: visual-line -*- *) +Set Universe Polymorphism. +Set Primitive Projections. +Close Scope nat_scope. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Arguments pair {A B} _ _. +Arguments fst {A B} _ / . +Arguments snd {A B} _ / . +Notation "x * y" := (prod x y) : type_scope. +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. + +Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. +Definition Type2 := Eval hnf in let gt := (Type1 : Type@{i}) in Type@{i}. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (@paths _ x y) : type_scope. +Definition concat {A} {x y z : A} (p : x = y) (q : y = z) : x = z + := match p, q with idpath, idpath => idpath end. + +Definition path_prod {A B : Type} (z z' : A * B) +: (fst z = fst z') -> (snd z = snd z') -> (z = z'). +Proof. + destruct z, z'; simpl; intros [] []; reflexivity. +Defined. + +Module Type TypeM. + Parameter m : Type2. +End TypeM. + +Module ProdM (XM : TypeM) (YM : TypeM) <: TypeM. + Definition m := XM.m * YM.m. +End ProdM. + +Module Type FunctionM (XM YM : TypeM). + Parameter m : XM.m -> YM.m. +End FunctionM. + +Module IdmapM (XM : TypeM) <: FunctionM XM XM. + Definition m := (fun x => x) : XM.m -> XM.m. +End IdmapM. + +Module Type HomotopyM (XM YM : TypeM) (fM gM : FunctionM XM YM). + Parameter m : forall x, fM.m x = gM.m x. +End HomotopyM. + +Module ComposeM (XM YM ZM : TypeM) + (gM : FunctionM YM ZM) (fM : FunctionM XM YM) + <: FunctionM XM ZM. + Definition m := (fun x => gM.m (fM.m x)). +End ComposeM. + +Module Type CorecM (YM ZM : TypeM) (fM : FunctionM YM ZM) + (XM : TypeM) (gM : FunctionM XM ZM). + Parameter m : XM.m -> YM.m. + Parameter m_beta : forall x, fM.m (m x) = gM.m x. +End CorecM. + +Module Type CoindpathsM (YM ZM : TypeM) (fM : FunctionM YM ZM) + (XM : TypeM) (hM kM : FunctionM XM YM). + Module fhM := ComposeM XM YM ZM fM hM. + Module fkM := ComposeM XM YM ZM fM kM. + Declare Module mM (pM : HomotopyM XM ZM fhM fkM) + : HomotopyM XM YM hM kM. +End CoindpathsM. + +Module Type Comodality (XM : TypeM). + Parameter m : Type2. + Module mM <: TypeM. + Definition m := m. + End mM. + Parameter from : m -> XM.m. + Module fromM <: FunctionM mM XM. + Definition m := from. + End fromM. + Declare Module corecM : CorecM mM XM fromM. + Declare Module coindpathsM : CoindpathsM mM XM fromM. +End Comodality. + +Module Comodality_Theory (F : Comodality). + + Module F_functor_M (XM YM : TypeM) (fM : FunctionM XM YM) + (FXM : Comodality XM) (FYM : Comodality YM). + Module f_o_from_M <: FunctionM FXM.mM YM. + Definition m := fun x => fM.m (FXM.from x). + End f_o_from_M. + Module mM := FYM.corecM FXM.mM f_o_from_M. + Definition m := mM.m. + End F_functor_M. + + Module F_prod_cmp_M (XM YM : TypeM) + (FXM : Comodality XM) (FYM : Comodality YM). + Module PM := ProdM XM YM. + Module PFM := ProdM FXM FYM. + Module fstM <: FunctionM PM XM. + Definition m := @fst XM.m YM.m. + End fstM. + Module sndM <: FunctionM PM YM. + Definition m := @snd XM.m YM.m. + End sndM. + Module FPM := F PM. + Module FfstM := F_functor_M PM XM fstM FPM FXM. + Module FsndM := F_functor_M PM YM sndM FPM FYM. + Definition m : FPM.m -> PFM.m + := fun z => (FfstM.m z , FsndM.m z). + End F_prod_cmp_M. + + Module isequiv_F_prod_cmp_M + (XM YM : TypeM) + (FXM : Comodality XM) (FYM : Comodality YM). + (** The comparison map *) + Module cmpM := F_prod_cmp_M XM YM FXM FYM. + Module FPM := cmpM.FPM. + (** We construct an inverse to it using corecursion. *) + Module prod_from_M <: FunctionM cmpM.PFM cmpM.PM. + Definition m : cmpM.PFM.m -> cmpM.PM.m + := fun z => ( FXM.from (fst z) , FYM.from (snd z) ). + End prod_from_M. + Module cmpinvM <: FunctionM cmpM.PFM FPM + := FPM.corecM cmpM.PFM prod_from_M. + (** We prove the first homotopy *) + Module cmpinv_o_cmp_M <: FunctionM FPM FPM + := ComposeM FPM cmpM.PFM FPM cmpinvM cmpM. + Module idmap_FPM <: FunctionM FPM FPM + := IdmapM FPM. + Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM. + Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM. + Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x. + Proof. + intros x. + refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _). + apply path_prod@{i i i}; simpl. + - exact (cmpM.FfstM.mM.m_beta@{i j} x). + - exact (cmpM.FsndM.mM.m_beta@{i j} x). + Defined. + Fail End cip_FPHM. +(* End isequiv_F_prod_cmp_M. + +End Comodality_Theory.*) |