diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-02 15:45:17 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-02 15:47:09 +0200 |
commit | b46020a6ea52d77b49a12e6891575b3516b8d766 (patch) | |
tree | bf1fe9bc6d70ac44111f755dca30ed3c4d90b286 /test-suite/bugs | |
parent | d02c9c566c58e566a1453827038f2b49b695c0a5 (diff) | |
parent | decdd5b3cc322936f7d1e7cc3bb363a2957d404e (diff) |
Merge branch 'v8.6'
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/3045.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/3753.v (renamed from test-suite/bugs/opened/3753.v) | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/4471.v | 6 | ||||
-rw-r--r-- | test-suite/bugs/closed/4527.v | 267 | ||||
-rw-r--r-- | test-suite/bugs/closed/4661.v | 10 | ||||
-rw-r--r-- | test-suite/bugs/closed/4723.v | 28 | ||||
-rw-r--r-- | test-suite/bugs/closed/4762.v | 24 | ||||
-rw-r--r-- | test-suite/bugs/closed/4798.v | 3 | ||||
-rw-r--r-- | test-suite/bugs/closed/4869.v | 18 | ||||
-rw-r--r-- | test-suite/bugs/closed/4877.v | 12 | ||||
-rw-r--r-- | test-suite/bugs/closed/5011.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/5036.v | 10 | ||||
-rw-r--r-- | test-suite/bugs/closed/5045.v | 3 |
13 files changed, 385 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3045.v b/test-suite/bugs/closed/3045.v index ef110ad0d..5f80013df 100644 --- a/test-suite/bugs/closed/3045.v +++ b/test-suite/bugs/closed/3045.v @@ -12,7 +12,7 @@ Record SpecializedCategory (obj : Type) := Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' }. -Arguments Compose {obj} [C s d d'] m1 m2 : rename. +Arguments Compose {obj} [C s d d'] _ _ : rename. Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type := | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'. diff --git a/test-suite/bugs/opened/3753.v b/test-suite/bugs/closed/3753.v index 05d77c831..5bfbee949 100644 --- a/test-suite/bugs/opened/3753.v +++ b/test-suite/bugs/closed/3753.v @@ -1,4 +1,4 @@ Axiom foo : Type -> Type. Axiom bar : forall (T : Type), T -> foo T. Arguments bar A x : rename. -Fail About bar. +About bar.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4471.v b/test-suite/bugs/closed/4471.v new file mode 100644 index 000000000..36efc42d4 --- /dev/null +++ b/test-suite/bugs/closed/4471.v @@ -0,0 +1,6 @@ +Goal forall (A B : Type) (P : forall _ : prod A B, Type) (a : A) (b : B) (p p0 : forall (x : A) (x' : B), P (@pair A B x x')), + @eq (P (@pair A B a b)) (p (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))) + (p0 (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))). +Proof. + intros. + Fail generalize dependent (a, b). diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v new file mode 100644 index 000000000..4ca6fe78c --- /dev/null +++ b/test-suite/bugs/closed/4527.v @@ -0,0 +1,267 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) +(* File reduced by coq-bug-finder from original input, then from 1199 lines to +430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, +then from 269 lines to 255 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml +4.01.0 + coqtop version 8.5 (January 2016) *) +Inductive False := . +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Init.Datatypes. + +Import Coq.Init.Notations. + +Global Set Universe Polymorphism. + +Notation "A -> B" := (forall (_ : A), B) : type_scope. + +Inductive True : Type := + I : True. +Module Export Datatypes. + +Set Implicit Arguments. +Notation nat := Coq.Init.Datatypes.nat. +Notation S := Coq.Init.Datatypes.S. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. + +Notation "x * y" := (prod x y) : type_scope. + +Open Scope nat_scope. + +End Datatypes. +Module Export Specif. + +Set Implicit Arguments. + +Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P +proj1_sig }. + +Notation sigT := sig (only parsing). + +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. + +Notation projT1 := proj1_sig (only parsing). +Notation projT2 := proj2_sig (only parsing). + +End Specif. +Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in +Type@{i}. + +Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in + let ge := ((fun x => x) : Type1@{j} -> +Type@{i}) in Type@{i}. + +Notation idmap := (fun x => x). +Delimit Scope function_scope with function. +Delimit Scope path_scope with path. +Delimit Scope fibration_scope with fibration. +Open Scope fibration_scope. +Open Scope function_scope. + +Notation pr1 := projT1. +Notation pr2 := projT2. + +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left +associativity) : function_scope. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope. + +Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : +type_scope. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) +}. + +Arguments eisretr {A B}%type_scope f%function_scope {_} _. +Arguments eissect {A B}%type_scope f%function_scope {_} _. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : +function_scope. + +Inductive Unit : Type1 := + tt : Unit. + +Local Open Scope path_scope. + +Section EquivInverse. + + Context {A B : Type} (f : A -> B) {feq : IsEquiv f}. + + Theorem other_adj (b : B) : eissect f (f^-1 b) = ap f^-1 (eisretr f b). +admit. +Defined. + + Global Instance isequiv_inverse : IsEquiv f^-1 | 10000 + := BuildIsEquiv B A f^-1 f (eissect f) (eisretr f) other_adj. +End EquivInverse. + +Section Adjointify. + + Context {A B : Type} (f : A -> B) (g : B -> A). + Context (isretr : Sect g f) (issect : Sect f g). + + Let issect' := fun x => + ap g (ap f (issect x)^) @ ap g (isretr (f x)) @ issect x. + + Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a). +admit. +Defined. + + Definition isequiv_adjointify : IsEquiv f + := BuildIsEquiv A B f g isretr issect' is_adjoint'. + +End Adjointify. + + Definition ExtensionAlong {A B : Type} (f : A -> B) + (P : B -> Type) (d : forall x:A, P (f x)) + := { s : forall y:B, P y & forall x:A, s (f x) = d x }. + + Fixpoint ExtendableAlong@{i j k l} + (n : nat) {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := match n with + | 0 => Unit@{l} + | S n => (forall (g : forall a, C (f a)), + ExtensionAlong@{i j k l l} f C g) * + forall (h k : forall b, C b), + ExtendableAlong n f (fun b => h b = k b) + end. + + Definition ooExtendableAlong@{i j k l} + {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := forall n, ExtendableAlong@{i j k l} n f C. + +Module Type ReflectiveSubuniverses. + + Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). + + Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter inO_equiv_inO@{u a i j k} : + forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + + let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + In@{u a j} O U. + + Parameter extendable_to_O@{u a i j k} + : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : +Type2le@{j a}} {Q_inO : In@{u a j} O Q}, + ooExtendableAlong@{i i j k} (to O P) (fun _ => Q). + +End ReflectiveSubuniverses. + +Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). +Export Os. + +Existing Class In. + + Coercion O_reflector : ReflectiveSubuniverse >-> Funclass. + +Arguments inO_equiv_inO {O} T {U} {_} f {_}. +Global Existing Instance O_inO. + +Section ORecursion. + Context {O : ReflectiveSubuniverse}. + + Definition O_indpaths {P Q : Type} {Q_inO : In O Q} + (g h : O P -> Q) (p : g o to O P == h o to O P) + : g == h + := (fst (snd (extendable_to_O O 2) g h) p).1. + + Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q} + (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) + : O_indpaths g h p (to O P x) = p x + := (fst (snd (extendable_to_O O 2) g h) p).2 x. + +End ORecursion. + +Section Reflective_Subuniverse. + Universes Ou Oa. + Context (O : ReflectiveSubuniverse@{Ou Oa}). + + Definition inO_isequiv_to_O (T:Type) + : IsEquiv (to O T) -> In O T + := fun _ => inO_equiv_inO (O T) (to O T)^-1. + + Definition inO_to_O_retract (T:Type) (mu : O T -> T) + : Sect (to O T) mu -> In O T. + Proof. + unfold Sect; intros H. + apply inO_isequiv_to_O. + apply isequiv_adjointify with (g:=mu). + - + refine (O_indpaths (to O T o mu) idmap _). + intros x; exact (ap (to O T) (H x)). + - + exact H. + Defined. + + Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : +S) : In@{Ou Oa i} O (x=y). + Proof. + simple refine (inO_to_O_retract@{i j} _ _ _); intro u. + - + assert (p : (fun _ : O (x=y) => x) == (fun _=> y)). + { + refine (O_indpaths _ _ _); simpl. + intro v; exact v. +} + exact (p u). + - + hnf. + rewrite O_indpaths_beta; reflexivity. + Qed. + Check inO_paths@{Type Type}. diff --git a/test-suite/bugs/closed/4661.v b/test-suite/bugs/closed/4661.v new file mode 100644 index 000000000..03d2350a6 --- /dev/null +++ b/test-suite/bugs/closed/4661.v @@ -0,0 +1,10 @@ +Module Type Test. + Parameter t : Type. +End Test. + +Module Type Func (T:Test). + Parameter x : Type. +End Func. + +Module Shortest_path (T : Test). +Print Func. diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v new file mode 100644 index 000000000..888481210 --- /dev/null +++ b/test-suite/bugs/closed/4723.v @@ -0,0 +1,28 @@ + +Require Coq.Program.Tactics. + +Record Matrix (m n : nat). + +Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q): + Matrix (m*p) (n*q). Admitted. + +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Ltac Obligation Tactic := admit. +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Axiom cheat : forall {A}, A. +Obligation Tactic := apply cheat. + +Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. +admit. +Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v new file mode 100644 index 000000000..7a87b07a8 --- /dev/null +++ b/test-suite/bugs/closed/4762.v @@ -0,0 +1,24 @@ +Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q. + +Lemma foo P Q R : R = myand P Q -> P -> Q -> R. +Proof. intros ->; constructor; auto. Qed. + +Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test1. +Qed. + +Hint Extern 0 => + match goal with + | |- myand _ _ => eapply foo; [reflexivity| |] + end : test2. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test2. (* works *) +Qed. + diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v new file mode 100644 index 000000000..dbc3d46fc --- /dev/null +++ b/test-suite/bugs/closed/4798.v @@ -0,0 +1,3 @@ +Check match 2 with 0 => 0 | S n => n end. +Notation "|" := 1 (compat "8.4"). +Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v new file mode 100644 index 000000000..6d21b66fe --- /dev/null +++ b/test-suite/bugs/closed/4869.v @@ -0,0 +1,18 @@ +Universes i. + +Fail Constraint i < Set. +Fail Constraint i <= Set. +Fail Constraint i = Set. +Constraint Set <= i. +Constraint Set < i. +Fail Constraint i < j. (* undeclared j *) +Fail Constraint i < Type. (* anonymous *) + +Set Universe Polymorphism. + +Section Foo. + Universe j. + Constraint Set < j. + + Definition foo := Type@{j}. +End Foo.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v new file mode 100644 index 000000000..7e3c78dc2 --- /dev/null +++ b/test-suite/bugs/closed/4877.v @@ -0,0 +1,12 @@ +Ltac induction_last := + let v := match goal with + | |- forall x y, _ = _ -> _ => 1 + | |- forall x y, _ -> _ = _ -> _ => 2 + | |- forall x y, _ -> _ -> _ = _ -> _ => 3 + end in + induction v. + +Goal forall n m : nat, True -> n = m -> m = n. + induction_last. + reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5011.v b/test-suite/bugs/closed/5011.v new file mode 100644 index 000000000..c3043ca5d --- /dev/null +++ b/test-suite/bugs/closed/5011.v @@ -0,0 +1,2 @@ +Record decoder (n : nat) W := { decode : W -> nat }. +Existing Class decoder. diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v new file mode 100644 index 000000000..12c958be6 --- /dev/null +++ b/test-suite/bugs/closed/5036.v @@ -0,0 +1,10 @@ +Section foo. + Context (F : Type -> Type). + Context (admit : forall {T}, F T = True). + Hint Rewrite (fun T => @admit T). + Lemma bad : F False. + Proof. + autorewrite with core. + constructor. + Qed. +End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/5045.v b/test-suite/bugs/closed/5045.v new file mode 100644 index 000000000..dc38738d8 --- /dev/null +++ b/test-suite/bugs/closed/5045.v @@ -0,0 +1,3 @@ +Axiom silly : 1 = 1 -> nat -> nat. +Goal forall pf : 1 = 1, silly pf 0 = 0 -> True. + Fail generalize (@eq nat). |