diff options
Diffstat (limited to 'test-suite')
41 files changed, 1449 insertions, 44 deletions
diff --git a/test-suite/bugs/closed/shouldfail/1898.v b/test-suite/bugs/closed/shouldfail/1898.v new file mode 100644 index 00000000..92490eb9 --- /dev/null +++ b/test-suite/bugs/closed/shouldfail/1898.v @@ -0,0 +1,5 @@ +(* folding should not allow circular dependencies *) + +Lemma bug_fold_unfold : True. + set (h := 1). + fold h in h. diff --git a/test-suite/bugs/closed/shouldsucceed/121.v b/test-suite/bugs/closed/shouldsucceed/121.v index d193aa73..8c5a3885 100644 --- a/test-suite/bugs/closed/shouldsucceed/121.v +++ b/test-suite/bugs/closed/shouldsucceed/121.v @@ -4,7 +4,7 @@ Section Setoid_Bug. Variable X:Type -> Type. Variable Xeq : forall A, (X A) -> (X A) -> Prop. -Hypothesis Xst : forall A, Equivalence (X A) (Xeq A). +Hypothesis Xst : forall A, Equivalence (Xeq A). Variable map : forall A B, (A -> B) -> X A -> X B. diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/shouldsucceed/1791.v new file mode 100644 index 00000000..694f056e --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1791.v @@ -0,0 +1,38 @@ +(* simpl performs eta expansion *) + +Set Implicit Arguments. +Require Import List. + +Definition k0 := Set. +Definition k1 := k0 -> k0. + +(** iterating X n times *) +Fixpoint Pow (X:k1)(k:nat){struct k}:k1:= + match k with 0 => fun X => X + | S k' => fun A => X (Pow X k' A) + end. + +Parameter Bush: k1. +Parameter BushToList: forall (A:k0), Bush A -> list A. + +Definition BushnToList (n:nat)(A:k0)(t:Pow Bush n A): list A. +Proof. + intros. + induction n. + exact (t::nil). + simpl in t. + exact (flat_map IHn (BushToList t)). +Defined. + +Parameter bnil : forall (A:k0), Bush A. +Axiom BushToList_bnil: forall (A:k0), BushToList (bnil A) = nil(A:=A). + +Lemma BushnToList_bnil (n:nat)(A:k0): + BushnToList (S n) A (bnil (Pow Bush n A)) = nil. +Proof. + intros. + simpl. + rewrite BushToList_bnil. + simpl. + reflexivity. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v new file mode 100644 index 00000000..11124cdd --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1891.v @@ -0,0 +1,13 @@ +(* Check evar-evar unification *) + Inductive T (A: Set): Set := mkT: unit -> T A. + + Definition f (A: Set) (l: T A): unit := tt. + + Implicit Arguments f [A]. + + Lemma L (x: T unit): (unit -> T unit) -> unit. + Proof. + refine (fun x => match x return _ with mkT n => fun g => f (g _) end). + trivial. + Qed. + diff --git a/test-suite/bugs/closed/shouldsucceed/1900.v b/test-suite/bugs/closed/shouldsucceed/1900.v new file mode 100644 index 00000000..cf03efda --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1900.v @@ -0,0 +1,8 @@ +Parameter A : Type . + +Definition eq_A := @eq A. + +Goal forall x, eq_A x x. +intros. +reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v new file mode 100644 index 00000000..598db366 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1901.v @@ -0,0 +1,11 @@ +Require Import Relations. + +Record Poset{A:Type}(Le : relation A) : Type := + Build_Poset + { + Le_refl : forall x : A, Le x x; + Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; + Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }. + +Definition nat_Poset : Poset Peano.le. +Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1907.v b/test-suite/bugs/closed/shouldsucceed/1907.v new file mode 100644 index 00000000..55fc8231 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1907.v @@ -0,0 +1,7 @@ +(* An example of type inference *) + +Axiom A : Type. +Definition f (x y : A) := x. +Axiom g : forall x y : A, f x y = y -> Prop. +Axiom x : A. +Check (g x _ (refl_equal x)). diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v new file mode 100644 index 00000000..9d4a3e04 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1918.v @@ -0,0 +1,377 @@ +(** Occur-check for Meta (up to delta) *) + +(** LNMItPredShort.v Version 2.0 July 2008 *) +(** does not need impredicative Set, runs under V8.2, tested with SVN 11296 *) + +(** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse*) + + +Set Implicit Arguments. + +(** the universe of all monotypes *) +Definition k0 := Set. + +(** the type of all type transformations *) +Definition k1 := k0 -> k0. + +(** the type of all rank-2 type transformations *) +Definition k2 := k1 -> k1. + +(** polymorphic identity *) +Definition id : forall (A:Set), A -> A := fun A x => x. + +(** composition *) +Definition comp (A B C:Set)(g:B->C)(f:A->B) : A->C := fun x => g (f x). + +Infix "o" := comp (at level 90). + +Definition sub_k1 (X Y:k1) : Type := + forall A:Set, X A -> Y A. + +Infix "c_k1" := sub_k1 (at level 60). + +(** monotonicity *) +Definition mon (X:k1) : Type := forall (A B:Set), (A -> B) -> X A -> X B. + +(** extensionality *) +Definition ext (X:k1)(h: mon X): Prop := + forall (A B:Set)(f g:A -> B), + (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r. + +(** first functor law *) +Definition fct1 (X:k1)(m: mon X) : Prop := + forall (A:Set)(x:X A), m _ _ (id(A:=A)) x = x. + +(** second functor law *) +Definition fct2 (X:k1)(m: mon X) : Prop := + forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A), + m _ _ (g o f) x = m _ _ g (m _ _ f x). + +(** pack up the good properties of the approximation into + the notion of an extensional functor *) +Record EFct (X:k1) : Type := mkEFct + { m : mon X; + e : ext m; + f1 : fct1 m; + f2 : fct2 m }. + +(** preservation of extensional functors *) +Definition pEFct (F:k2) : Type := + forall (X:k1), EFct X -> EFct (F X). + + +(** we show some closure properties of pEFct, depending on such properties + for EFct *) + +Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)). +Proof. + red. + intros X Y mX mY A B f x. + exact (mX (Y A)(Y B) (mY A B f) x). +Defined. + +(** closure under composition *) +Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)). +Proof. + intros X Y ef1 ef2. + apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp. +(* prove ext *) + apply (e ef1). + intro. + apply (e ef2); trivial. +(* prove fct1 *) + rewrite (e ef1 (m ef2 (id (A:=A))) (id(A:=Y A))). + apply (f1 ef1). + intro. + apply (f1 ef2). +(* prove fct2 *) + rewrite (e ef1 (m ef2 (g o f))((m ef2 g)o(m ef2 f))). + apply (f2 ef1). + intro. + unfold comp at 2. + apply (f2 ef2). +Defined. + +Corollary comppEFct (F G:k2): pEFct F -> pEFct G -> + pEFct (fun X A => F X (G X A)). +Proof. + red. + intros. + apply compEFct; auto. +Defined. + +(** closure under sums *) +Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type. +Proof. + intros X Y ef1 ef2. + set (m12:=fun (A B:Set)(f:A->B) x => match x with + | inl y => inl _ (m ef1 f y) + | inr y => inr _ (m ef2 f y) + end). + apply (mkEFct(m:=m12)); red; intros. +(* prove ext *) + destruct r. + simpl. + apply (f_equal (fun x=>inl (A:=X B) (Y B) x)). + apply (e ef1); trivial. + simpl. + apply (f_equal (fun x=>inr (X B) (B:=Y B) x)). + apply (e ef2); trivial. +(* prove fct1 *) + destruct x. + simpl. + apply (f_equal (fun x=>inl (A:=X A) (Y A) x)). + apply (f1 ef1). + simpl. + apply (f_equal (fun x=>inr (X A) (B:=Y A) x)). + apply (f1 ef2). +(* prove fct2 *) + destruct x. + simpl. + rewrite (f2 ef1); reflexivity. + simpl. + rewrite (f2 ef2); reflexivity. +Defined. + +Corollary sumpEFct (F G:k2): pEFct F -> pEFct G -> + pEFct (fun X A => F X A + G X A)%type. +Proof. + red. + intros. + apply sumEFct; auto. +Defined. + +(** closure under products *) +Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type. +Proof. + intros X Y ef1 ef2. + set (m12:=fun (A B:Set)(f:A->B) x => match x with + (x1,x2) => (m ef1 f x1, m ef2 f x2) end). + apply (mkEFct(m:=m12)); red; intros. +(* prove ext *) + destruct r as [x1 x2]. + simpl. + apply injective_projections; simpl. + apply (e ef1); trivial. + apply (e ef2); trivial. +(* prove fct1 *) + destruct x as [x1 x2]. + simpl. + apply injective_projections; simpl. + apply (f1 ef1). + apply (f1 ef2). +(* prove fct2 *) + destruct x as [x1 x2]. + simpl. + apply injective_projections; simpl. + apply (f2 ef1). + apply (f2 ef2). +Defined. + +Corollary prodpEFct (F G:k2): pEFct F -> pEFct G -> + pEFct (fun X A => F X A * G X A)%type. +Proof. + red. + intros. + apply prodEFct; auto. +Defined. + +(** the identity in k2 preserves extensional functors *) +Lemma idpEFct: pEFct (fun X => X). +Proof. + red. + intros. + assumption. +Defined. + +(** a variant for the eta-expanded identity *) +Lemma idpEFct_eta: pEFct (fun X A => X A). +Proof. + red. + intros X ef. + destruct ef as [m0 e0 f01 f02]. + change (mon X) with (mon (fun A => X A)) in m0. + apply (mkEFct (m:=m0) e0 f01 f02). +Defined. + +(** the identity in k1 "is" an extensional functor *) +Lemma idEFct: EFct (fun A => A). +Proof. + set (mId:=fun A B (f:A->B)(x:A) => f x). + apply (mkEFct(m:=mId)). + red. + intros. + unfold mId. + apply H. + red. + reflexivity. + red. + reflexivity. +Defined. + +(** constants in k2 *) +Lemma constpEFct (X:k1): EFct X -> pEFct (fun _ => X). +Proof. + red. + intros. + assumption. +Defined. + +(** constants in k1 *) +Lemma constEFct (C:Set): EFct (fun _ => C). +Proof. + intro. + set (mC:=fun A B (f:A->B)(x:C) => x). + apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity. +Defined. + + +(** the option type *) +Lemma optionEFct: EFct (fun (A:Set) => option A). + apply (mkEFct (X:=fun (A:Set) => option A)(m:=option_map)); red; intros. + destruct r. + simpl. + rewrite H. + reflexivity. + reflexivity. + destruct x; reflexivity. + destruct x; reflexivity. +Defined. + + +(** natural transformations from (X,mX) to (Y,mY) *) +Definition NAT(X Y:k1)(j:X c_k1 Y)(mX:mon X)(mY:mon Y) : Prop := + forall (A B:Set)(f:A->B)(t:X A), j B (mX A B f t) = mY _ _ f (j A t). + + +Module Type LNMIt_Type. + +Parameter F:k2. +Parameter FpEFct: pEFct F. +Parameter mu20: k1. +Definition mu2: k1:= fun A => mu20 A. +Parameter mapmu2: mon mu2. +Definition MItType: Type := + forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G. +Parameter MIt0 : MItType. +Definition MIt : MItType:= fun G s A t => MIt0 s t. +Definition InType : Type := + forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), + NAT j (m ef) mapmu2 -> F X c_k1 mu2. +Parameter In : InType. +Axiom mapmu2Red : forall (A:Set)(X:k1)(ef:EFct X)(j: X c_k1 mu2) + (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B), + mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t). +Axiom MItRed : forall (G : k1) + (s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2) + (n: NAT j (m ef) mapmu2)(A:Set)(t:F X A), + MIt s (In ef n t) = s X (fun A => (MIt s (A:=A)) o (j A)) A t. +Definition mu2IndType : Prop := + forall (P : (forall A : Set, mu2 A -> Prop)), + (forall (X : k1)(ef:EFct X)(j : X c_k1 mu2)(n: NAT j (m ef) mapmu2), + (forall (A : Set) (x : X A), P A (j A x)) -> + forall (A:Set)(t : F X A), P A (In ef n t)) -> + forall (A : Set) (r : mu2 A), P A r. +Axiom mu2Ind : mu2IndType. + +End LNMIt_Type. + +(** BushDepPredShort.v Version 0.2 July 2008 *) +(** does not need impredicative Set, produces stack overflow under V8.2, tested +with SVN 11296 *) + +(** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse *) + +Set Implicit Arguments. + +Require Import List. + +Definition listk1 (A:Set) : Set := list A. +Open Scope type_scope. + +Definition BushF(X:k1)(A:Set) := unit + A * X (X A). + +Definition bushpEFct : pEFct BushF. +Proof. + unfold BushF. + apply sumpEFct. + apply constpEFct. + apply constEFct. + apply prodpEFct. + apply constpEFct. + apply idEFct. + apply comppEFct. + apply idpEFct. + apply idpEFct_eta. +Defined. + +Module Type BUSH := LNMIt_Type with Definition F:=BushF + with Definition FpEFct := +bushpEFct. + +Module Bush (BushBase:BUSH). + +Definition Bush : k1 := BushBase.mu2. + +Definition bush : mon Bush := BushBase.mapmu2. + +End Bush. + + +Definition Id : k1 := fun X => X. + +Fixpoint Pow (X:k1)(k:nat){struct k}:k1:= + match k with 0 => Id + | S k' => fun A => X (Pow X k' A) + end. + +Fixpoint POW (k:nat)(X:k1)(m:mon X){struct k} : mon (Pow X k) := + match k return mon (Pow X k) + with 0 => fun _ _ f => f + | S k' => fun _ _ f => m _ _ (POW k' m f) + end. + +Module Type BushkToList_Type. + +Declare Module Import BP: BUSH. +Definition F:=BushF. +Definition FpEFct:= bushpEFct. +Definition mu20 := mu20. +Definition mu2 := mu2. +Definition mapmu2 := mapmu2. +Definition MItType:= MItType. +Definition MIt0 := MIt0. +Definition MIt := MIt. +Definition InType := InType. +Definition In := In. +Definition mapmu2Red:=mapmu2Red. +Definition MItRed:=MItRed. +Definition mu2IndType:=mu2IndType. +Definition mu2Ind:=mu2Ind. + +Definition Bush:= mu2. +Module BushM := Bush BP. + +Parameter BushkToList: forall(k:nat)(A:k0)(t:Pow Bush k A), list A. +Axiom BushkToList0: forall(A:k0)(t:Pow Bush 0 A), BushkToList 0 A t = t::nil. + +End BushkToList_Type. + +Module BushDep (BushkToListM:BushkToList_Type). + +Module Bush := Bush BushkToListM. + +Import Bush. +Import BushkToListM. + + +Lemma BushkToList0NAT: NAT(Y:=listk1) (BushkToList 0) (POW 0 bush) map. +Proof. + red. + intros. + simpl. + rewrite BushkToList0. +(* stack overflow for coqc and coqtop *) + + +Abort. diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v new file mode 100644 index 00000000..17eb721a --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1925.v @@ -0,0 +1,22 @@ +(* Check that the analysis of projectable rel's in an evar instance is up to + aliases *) + +Require Import List. + +Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := + fun x : A => g(f x). + +Definition map_fuse' : + forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), + (map g (map f xs)) = map (compose _ _ _ g f) xs + := + fun A B C g f => + (fix loop (ys : list A) {struct ys} := + match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys + with + | nil => refl_equal nil + | x :: xs => + match loop xs in eq _ a return eq _ ((g (f x)) :: a) with + | refl_equal => refl_equal (map g (map f (x :: xs))) + end + end). diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/shouldsucceed/1931.v new file mode 100644 index 00000000..bc8be78f --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1931.v @@ -0,0 +1,29 @@ + + +Set Implicit Arguments. + +Inductive T (A:Set) : Set := + app : T A -> T A -> T A. + +Fixpoint map (A B:Set)(f:A->B)(t:T A) : T B := + match t with + app t1 t2 => app (map f t1)(map f t2) + end. + +Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B := + match t with + app t1 t2 => app (subst f t1)(subst f t2) + end. + +(* This is the culprit: *) +Definition k0:=Set. + +(** interaction of subst with map *) +Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A): + subst g (map f t) = subst (fun x => g (f x)) t. +Proof. + intros. + generalize B C f g; clear B C f g. + induction t; intros; simpl. + f_equal. +Admitted. diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v new file mode 100644 index 00000000..641dcb7a --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1935.v @@ -0,0 +1,21 @@ +Definition f (n:nat) := n = n. + +Lemma f_refl : forall n , f n. +intros. reflexivity. +Qed. + +Definition f' (x:nat) (n:nat) := n = n. + +Lemma f_refl' : forall n , f' n n. +Proof. + intros. reflexivity. +Qed. + +Require Import ZArith. + +Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt. + +Lemma f_refl'' : forall n , f'' true n n. +Proof. + intro. reflexivity. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1963.v b/test-suite/bugs/closed/shouldsucceed/1963.v new file mode 100644 index 00000000..11e2ee44 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1963.v @@ -0,0 +1,19 @@ +(* Check that "dependent inversion" behaves correctly w.r.t to universes *) + +Require Import Eqdep. + +Set Implicit Arguments. + +Inductive illist(A:Type) : nat -> Type := + illistn : illist A 0 +| illistc : forall n:nat, A -> illist A n -> illist A (S n). + +Inductive isig (A:Type)(P:A -> Type) : Type := + iexists : forall x : A, P x -> isig P. + +Lemma inv : forall (A:Type)(n n':nat)(ts':illist A n'), n' = S n -> + isig (fun t => isig (fun ts => + eq_dep nat (fun n => illist A n) n' ts' (S n) (illistc t ts))). +Proof. +intros. +dependent inversion ts'. diff --git a/test-suite/bugs/closed/shouldsucceed/1977.v b/test-suite/bugs/closed/shouldsucceed/1977.v new file mode 100644 index 00000000..28715040 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1977.v @@ -0,0 +1,4 @@ +Inductive T {A} : Prop := c : A -> T. +Goal (@T nat). +apply c. exact 0. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v new file mode 100644 index 00000000..0c3b96da --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1981.v @@ -0,0 +1,5 @@ +Implicit Arguments ex_intro [A]. + +Goal exists n : nat, True. + eapply ex_intro. exact 0. exact I. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v new file mode 100644 index 00000000..323021de --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2001.v @@ -0,0 +1,20 @@ +(* Automatic computing of guard in "Theorem with"; check that guard is not + computed when the user explicitly indicated it *) + +Inductive T : Set := +| v : T. + +Definition f (s:nat) (t:T) : nat. +fix 2. +intros s t. +refine + match t with + | v => s + end. +Defined. + +Lemma test : + forall s, f s v = s. +Proof. +reflexivity. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v new file mode 100644 index 00000000..948cea3e --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2017.v @@ -0,0 +1,15 @@ +(* Some check of Miller's pattern inference - used to fail in 8.2 due + first to the presence of aliases, secondly due to the absence of + restriction of the potential interesting variables to the subset of + variables effectively occurring in the term to instantiate *) + +Set Implicit Arguments. + +Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool. + +Variable H : exists x : bool, True. + +Definition coef := +match Some true with + Some _ => @choose _ H |_ => true +end . diff --git a/test-suite/bugs/closed/shouldsucceed/2021.v b/test-suite/bugs/closed/shouldsucceed/2021.v new file mode 100644 index 00000000..e598e5ae --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2021.v @@ -0,0 +1,23 @@ +(* correct failure of injection/discriminate on types whose inductive + status derives from the substitution of an argument *) + +Inductive t : nat -> Type := +| M : forall n: nat, nat -> t n. + +Lemma eq_t : forall n n' m m', + existT (fun B : Type => B) (t n) (M n m) = + existT (fun B : Type => B) (t n') (M n' m') -> True. +Proof. + intros. + injection H. + intro Ht. + exact I. +Qed. + +Lemma eq_t' : forall n n' : nat, + existT (fun B : Type => B) (t n) (M n 0) = + existT (fun B : Type => B) (t n') (M n' 1) -> True. +Proof. + intros. + discriminate H || exact I. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2027.v b/test-suite/bugs/closed/shouldsucceed/2027.v new file mode 100644 index 00000000..fb53c6ef --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2027.v @@ -0,0 +1,11 @@ + +Parameter T : Type -> Type. +Parameter f : forall {A}, T A -> T A. +Parameter P : forall {A}, T A -> Prop. +Axiom f_id : forall {A} (l : T A), f l = l. + +Goal forall A (p : T A), P p. +Proof. + intros. + rewrite <- f_id. +Admitted.
\ No newline at end of file diff --git a/test-suite/check b/test-suite/check index 47960e98..bed86c41 100755 --- a/test-suite/check +++ b/test-suite/check @@ -3,9 +3,9 @@ # Automatic test of Coq if [ "$1" = -byte ]; then - coqtop="../bin/coqtop.byte -q -batch" + coqtop="../bin/coqtop.byte -boot -q -batch" else - coqtop="../bin/coqtop -q -batch" + coqtop="../bin/coqtop -boot -q -batch" fi command="$coqtop -top Top -load-vernac-source" diff --git a/test-suite/complexity/autodecomp.v b/test-suite/complexity/autodecomp.v new file mode 100644 index 00000000..8916b104 --- /dev/null +++ b/test-suite/complexity/autodecomp.v @@ -0,0 +1,11 @@ +(* This example used to be in (at least) exponential time in the number of + conjunctive types in the hypotheses before revision 11713 *) +(* Expected time < 1.50s *) + +Goal +True/\True-> +True/\True-> +True/\True-> +False/\False. + +Time auto decomp. diff --git a/test-suite/failure/Reordering.v b/test-suite/failure/Reordering.v new file mode 100644 index 00000000..7b36d1c3 --- /dev/null +++ b/test-suite/failure/Reordering.v @@ -0,0 +1,5 @@ +(* Testing that hypothesis order (following a conversion/folding) is checked *) + +Goal forall (A:Set) (x:A) (A':=A), True. +intros. +change ((fun (_:A') => Set) x) in (type of A). diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 46208c29..7e07a905 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -8,3 +8,14 @@ Fixpoint F (n:nat) : False := F (match F n with end). +(* de Bruijn mix-up *) +(* If accepted, Eval compute in f 0. loops *) +Definition f := + let f (f1 f2:nat->nat) := f1 in + let _ := 0 in + let _ := 0 in + let g (f1 f2:nat->nat) := f2 in + let h := f in (* h = Rel 4 *) + fix F (n:nat) : nat := + h F S n. (* here Rel 4 = g *) + diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v index 13b5e13d..1ff53294 100644 --- a/test-suite/output/ArgumentsScope.v +++ b/test-suite/output/ArgumentsScope.v @@ -1,4 +1,4 @@ -(* A few tests to check Argument Scope Global command *) +(* A few tests to check Global Argument Scope command *) Section A. Variable a : bool -> bool. @@ -11,11 +11,11 @@ About b. About negb''. About negb'. About negb. -Arguments Scope Global negb'' [ _ ]. -Arguments Scope Global negb' [ _ ]. -Arguments Scope Global negb [ _ ]. -Arguments Scope Global a [ _ ]. -Arguments Scope Global b [ _ ]. +Global Arguments Scope negb'' [ _ ]. +Global Arguments Scope negb' [ _ ]. +Global Arguments Scope negb [ _ ]. +Global Arguments Scope a [ _ ]. +Global Arguments Scope b [ _ ]. About a. About b. About negb. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 995754a6..1f0e12d3 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -28,3 +28,5 @@ fix foo (A : Type) (l : list A) {struct l} : option A := : forall A : Type, list A -> option A Argument scopes are [type_scope list_scope] +foo' = if A 0 then true else false + : bool diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 61f89d40..37ee71e9 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -33,3 +33,16 @@ Fixpoint foo (A:Type) (l:list A) : option A := end. Print foo. + +(* Do not duplicate the matched term *) + +Axiom A : nat -> bool. + +Definition foo' := + match A 0 with + | true => true + | x => x + end. + +Print foo'. + diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 2066a7ef..42858304 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -50,3 +50,10 @@ Nil : forall A : Type, list A NIL:list nat : list nat +Defining 'I' as keyword +(false && I 3)%bool /\ I 6 + : Prop +[|1, 2, 3; 4, 5, 6|] + : Z * Z * Z * (Z * Z * Z) +fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z + : (Z -> Z -> Z -> Z) -> Z diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 6e637aca..b37c3638 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -129,3 +129,33 @@ Check Nil. Notation NIL := nil. Check NIL : list nat. + + +(**********************************************************************) +(* Test printing of notation with coercions in scope of a coercion *) + +Open Scope nat_scope. + +Coercion is_true := fun b => b=true. +Coercion of_nat n := match n with 0 => true | _ => false end. +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10). + +Check (false && I 3)%bool /\ I 6. + +(**********************************************************************) +(* Check notations with several recursive patterns *) + +Open Scope Z_scope. + +Notation "[| x , y , .. , z ; a , b , .. , c |]" := + (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)). +Check [|1,2,3;4,5,6|]. + +(**********************************************************************) +(* Test recursive notations involving applications *) +(* Caveat: does not work for applied constant because constants are *) +(* classified as notations for the particular constant while this *) +(* generic application notation is classified as generic *) + +Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y). +Check fun f => {| f; 0; 1; 2 |} : Z. diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v new file mode 100644 index 00000000..e31135c2 --- /dev/null +++ b/test-suite/success/Equations.v @@ -0,0 +1,321 @@ +Require Import Program. + +Equations neg (b : bool) : bool := +neg true := false ; +neg false := true. + +Eval compute in neg. + +Require Import Coq.Lists.List. + +Equations head A (default : A) (l : list A) : A := +head A default nil := default ; +head A default (cons a v) := a. + +Eval compute in head. + +Equations tail {A} (l : list A) : (list A) := +tail A nil := nil ; +tail A (cons a v) := v. + +Eval compute in @tail. + +Eval compute in (tail (cons 1 nil)). + +Reserved Notation " x ++ y " (at level 60, right associativity). + +Equations app' {A} (l l' : list A) : (list A) := +app' A nil l := l ; +app' A (cons a v) l := cons a (app' v l). + +Equations app (l l' : list nat) : list nat := + [] ++ l := l ; + (a :: v) ++ l := a :: (v ++ l) + +where " x ++ y " := (app x y). + +Eval compute in @app'. + +Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) := +zip' A f nil nil := nil ; +zip' A f (cons a v) (cons b w) := cons (f a b) (zip' f v w) ; +zip' A f nil (cons b w) := nil ; +zip' A f (cons a v) nil := nil. + + +Eval compute in @zip'. + +Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) := +zip'' A f nil nil def := nil ; +zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' f v w def) ; +zip'' A f nil (cons b w) def := def ; +zip'' A f (cons a v) nil def := def. + +Eval compute in @zip''. + +Inductive fin : nat -> Set := +| fz : Π {n}, fin (S n) +| fs : Π {n}, fin n -> fin (S n). + +Inductive finle : Π (n : nat) (x : fin n) (y : fin n), Prop := +| leqz : Π {n j}, finle (S n) fz j +| leqs : Π {n i j}, finle n i j -> finle (S n) (fs i) (fs j). + +Scheme finle_ind_dep := Induction for finle Sort Prop. + +Instance finle_ind_pack n x y : DependentEliminationPackage (finle n x y) := + { elim_type := _ ; elim := finle_ind_dep }. + +Implicit Arguments finle [[n]]. + +Require Import Bvector. + +Implicit Arguments Vnil [[A]]. +Implicit Arguments Vcons [[A] [n]]. + +Equations vhead {A n} (v : vector A (S n)) : A := +vhead A n (Vcons a v) := a. + +Equations vmap {A B} (f : A -> B) {n} (v : vector A n) : (vector B n) := +vmap A B f 0 Vnil := Vnil ; +vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap f v). + +Eval compute in (vmap id (@Vnil nat)). +Eval compute in (vmap id (@Vcons nat 2 _ Vnil)). +Eval compute in @vmap. + +Equations Below_nat (P : nat -> Type) (n : nat) : Type := +Below_nat P 0 := unit ; +Below_nat P (S n) := prod (P n) (Below_nat P n). + +Equations below_nat (P : nat -> Type) n (step : Π (n : nat), Below_nat P n -> P n) : Below_nat P n := +below_nat P 0 step := tt ; +below_nat P (S n) step := let rest := below_nat P n step in + (step n rest, rest). + +Class BelowPack (A : Type) := + { Below : Type ; below : Below }. + +Instance nat_BelowPack : BelowPack nat := + { Below := Π P n step, Below_nat P n ; + below := λ P n step, below_nat P n (step P) }. + +Definition rec_nat (P : nat -> Type) n (step : Π n, Below_nat P n -> P n) : P n := + step n (below_nat P n step). + +Fixpoint Below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n) : Type := + match v with Vnil => unit | Vcons a n' v' => prod (P A n' v') (Below_vector P A n' v') end. + +Equations below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n) + (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : Below_vector P A n v := +below_vector P A ?(0) Vnil step := tt ; +below_vector P A ?(S n) (Vcons a v) step := + let rest := below_vector P A n v step in + (step A n v rest, rest). + +Instance vector_BelowPack : BelowPack (Π A n, vector A n) := + { Below := Π P A n v step, Below_vector P A n v ; + below := λ P A n v step, below_vector P A n v (step P) }. + +Instance vector_noargs_BelowPack A n : BelowPack (vector A n) := + { Below := Π P v step, Below_vector P A n v ; + below := λ P v step, below_vector P A n v (step P) }. + +Definition rec_vector (P : Π A n, vector A n -> Type) A n v + (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : P A n v := + step A n v (below_vector P A n v step). + +Class Recursor (A : Type) (BP : BelowPack A) := + { rec_type : Π x : A, Type ; rec : Π x : A, rec_type x }. + +Instance nat_Recursor : Recursor nat nat_BelowPack := + { rec_type := λ n, Π P step, P n ; + rec := λ n P step, rec_nat P n (step P) }. + +(* Instance vect_Recursor : Recursor (Π A n, vector A n) vector_BelowPack := *) +(* rec_type := Π (P : Π A n, vector A n -> Type) step A n v, P A n v; *) +(* rec := λ P step A n v, rec_vector P A n v step. *) + +Instance vect_Recursor_noargs A n : Recursor (vector A n) (vector_noargs_BelowPack A n) := + { rec_type := λ v, Π (P : Π A n, vector A n -> Type) step, P A n v; + rec := λ v P step, rec_vector P A n v step }. + +Implicit Arguments Below_vector [P A n]. + +Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity). + +(** Won't pass the guardness check which diverges anyway. *) + +(* Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k := *) +(* trans ?(S n) ?(fz) ?(j) ?(k) leqz q := leqz ; *) +(* trans ?(S n) ?(fs i) ?(fs j) ?(fs k) (leqs p) (leqs q) := leqs (trans p q). *) + +(* Lemma trans_eq1 n (j k : fin (S n)) (q : finle j k) : trans leqz q = leqz. *) +(* Proof. intros. simplify_equations ; reflexivity. Qed. *) + +(* Lemma trans_eq2 n i j k p q : @trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans p q). *) +(* Proof. intros. simplify_equations ; reflexivity. Qed. *) + +Section Image. + Context {S T : Type}. + Variable f : S -> T. + + Inductive Imf : T -> Type := imf (s : S) : Imf (f s). + + Equations inv (t : T) (im : Imf t) : S := + inv (f s) (imf s) := s. + +End Image. + +Section Univ. + + Inductive univ : Set := + | ubool | unat | uarrow (from:univ) (to:univ). + + Equations interp (u : univ) : Type := + interp ubool := bool ; interp unat := nat ; + interp (uarrow from to) := interp from -> interp to. + + Equations foo (u : univ) (el : interp u) : interp u := + foo ubool true := false ; + foo ubool false := true ; + foo unat t := t ; + foo (uarrow from to) f := id ∘ f. + + Eval lazy beta delta [ foo foo_obligation_1 foo_obligation_2 ] iota zeta in foo. + +End Univ. + +Eval compute in (foo ubool false). +Eval compute in (foo (uarrow ubool ubool) negb). +Eval compute in (foo (uarrow ubool ubool) id). + +Inductive foobar : Set := bar | baz. + +Equations bla (f : foobar) : bool := +bla bar := true ; +bla baz := false. + +Eval simpl in bla. +Print refl_equal. + +Notation "'refl'" := (@refl_equal _ _). + +Equations K {A} (x : A) (P : x = x -> Type) (p : P (refl_equal x)) (p : x = x) : P p := +K A x P p refl := p. + +Equations eq_sym {A} (x y : A) (H : x = y) : y = x := +eq_sym A x x refl := refl. + +Equations eq_trans {A} (x y z : A) (p : x = y) (q : y = z) : x = z := +eq_trans A x x x refl refl := refl. + +Lemma eq_trans_eq A x : @eq_trans A x x x refl refl = refl. +Proof. reflexivity. Qed. + +Equations nth {A} {n} (v : vector A n) (f : fin n) : A := +nth A (S n) (Vcons a v) fz := a ; +nth A (S n) (Vcons a v) (fs f) := nth v f. + +Equations tabulate {A} {n} (f : fin n -> A) : vector A n := +tabulate A 0 f := Vnil ; +tabulate A (S n) f := Vcons (f fz) (tabulate (f ∘ fs)). + +Equations vlast {A} {n} (v : vector A (S n)) : A := +vlast A 0 (Vcons a Vnil) := a ; +vlast A (S n) (Vcons a (n:=S n) v) := vlast v. + +Print Assumptions vlast. + +Equations vlast' {A} {n} (v : vector A (S n)) : A := +vlast' A ?(0) (Vcons a Vnil) := a ; +vlast' A ?(S n) (Vcons a (n:=S n) v) := vlast' v. + +Lemma vlast_equation1 A (a : A) : vlast' (Vcons a Vnil) = a. +Proof. intros. simplify_equations. reflexivity. Qed. + +Lemma vlast_equation2 A n a v : @vlast' A (S n) (Vcons a v) = vlast' v. +Proof. intros. simplify_equations ; reflexivity. Qed. + +Print Assumptions vlast'. +Print Assumptions nth. +Print Assumptions tabulate. + +Extraction vlast. +Extraction vlast'. + +Equations vliat {A} {n} (v : vector A (S n)) : vector A n := +vliat A 0 (Vcons a Vnil) := Vnil ; +vliat A (S n) (Vcons a v) := Vcons a (vliat v). + +Eval compute in (vliat (Vcons 2 (Vcons 5 (Vcons 4 Vnil)))). + +Equations vapp' {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m) := +vapp' A ?(0) m Vnil w := w ; +vapp' A ?(S n) m (Vcons a v) w := Vcons a (vapp' v w). + +Eval compute in @vapp'. + +Fixpoint vapp {A n m} (v : vector A n) (w : vector A m) : vector A (n + m) := + match v with + | Vnil => w + | Vcons a n' v' => Vcons a (vapp v' w) + end. + +Lemma JMeq_Vcons_inj A n m a (x : vector A n) (y : vector A m) : n = m -> JMeq x y -> JMeq (Vcons a x) (Vcons a y). +Proof. intros until y. simplify_dep_elim. reflexivity. Qed. + +Equations NoConfusion_fin (P : Prop) {n : nat} (x y : fin n) : Prop := +NoConfusion_fin P (S n) fz fz := P -> P ; +NoConfusion_fin P (S n) fz (fs y) := P ; +NoConfusion_fin P (S n) (fs x) fz := P ; +NoConfusion_fin P (S n) (fs x) (fs y) := (x = y -> P) -> P. + +Eval compute in NoConfusion_fin. +Eval compute in NoConfusion_fin_comp. + +Print Assumptions NoConfusion_fin. + +Eval compute in (fun P n => NoConfusion_fin P (n:=S n) fz fz). + +(* Equations noConfusion_fin P (n : nat) (x y : fin n) (H : x = y) : NoConfusion_fin P x y := *) +(* noConfusion_fin P (S n) fz fz refl := λ p _, p ; *) +(* noConfusion_fin P (S n) (fs x) (fs x) refl := λ p : x = x -> P, p refl. *) + +Equations_nocomp NoConfusion_vect (P : Prop) {A n} (x y : vector A n) : Prop := +NoConfusion_vect P A 0 Vnil Vnil := P -> P ; +NoConfusion_vect P A (S n) (Vcons a x) (Vcons b y) := (a = b -> x = y -> P) -> P. + +Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoConfusion_vect P x y := +noConfusion_vect P A 0 Vnil Vnil refl := λ p, p ; +noConfusion_vect P A (S n) (Vcons a v) (Vcons a v) refl := λ p : a = a -> v = v -> P, p refl refl. + +(* Instance fin_noconf n : NoConfusionPackage (fin n) := *) +(* NoConfusion := λ P, Π x y, x = y -> NoConfusion_fin P x y ; *) +(* noConfusion := λ P x y, noConfusion_fin P n x y. *) + +Instance vect_noconf A n : NoConfusionPackage (vector A n) := + { NoConfusion := λ P, Π x y, x = y -> NoConfusion_vect P x y ; + noConfusion := λ P x y, noConfusion_vect P A n x y }. + +Equations fog {n} (f : fin n) : nat := +fog (S n) fz := 0 ; fog (S n) (fs f) := S (fog f). + +Inductive Split {X : Set}{m n : nat} : vector X (m + n) -> Set := + append : Π (xs : vector X m)(ys : vector X n), Split (vapp xs ys). + +Implicit Arguments Split [[X]]. + +Equations_nocomp split {X : Set}(m n : nat) (xs : vector X (m + n)) : Split m n xs := +split X 0 n xs := append Vnil xs ; +split X (S m) n (Vcons x xs) := + let 'append xs' ys' in Split _ _ vec := split m n xs return Split (S m) n (Vcons x vec) in + append (Vcons x xs') ys'. + +Eval compute in (split 0 1 (vapp Vnil (Vcons 2 Vnil))). +Eval compute in (split _ _ (vapp (Vcons 3 Vnil) (Vcons 2 Vnil))). + +Extraction Inline split_obligation_1 split_obligation_2. +Recursive Extraction split. + +Eval compute in @split. diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v new file mode 100644 index 00000000..6b503e95 --- /dev/null +++ b/test-suite/success/Generalization.v @@ -0,0 +1,13 @@ + +Check `(a = 0). +Check `(a = 0)%type. +Definition relation A := A -> A -> Prop. +Definition equivalence `(R : relation A) := True. +Check (`(@equivalence A R)). + +Definition a_eq_b : `( a = 0 /\ a = b /\ b > c \/ d = e /\ d = 1). +Admitted. +Print a_eq_b. + + + diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index f83328e8..b08ffcc3 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -99,3 +99,11 @@ Lemma depinv : forall a b, foo a b -> True. intros a b H. inversion H. Abort. + +(* Check non-regression of bug #1968 *) + +Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t). +Goal forall o, foo2 o -> 0 = 1. +intros. +eapply trans_eq. +inversion H. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 6dce0401..4bdd579a 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -26,3 +26,8 @@ Notation "x +1" := (S x) (at level 8, right associativity). right order *) Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2). + +(* Check import of notations from within a section *) + +Notation "+1 x" := (S x) (at level 25, x at level 9). +Section A. Global Notation "'Z'" := O (at level 9). End A. diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index 7fdbcda7..885fff48 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -1,3 +1,82 @@ (* Nijmegen expects redefinition of sorts *) Definition CProp := Prop. -Record test : CProp := {n : nat}. +Record test : CProp := {n : nat ; m : bool ; _ : n <> 0 }. +Require Import Program. +Require Import List. + +Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }. +Implicit Arguments vector []. + +Coercion vec_list : vector >-> list. + +Hint Rewrite @vec_len : datatypes. + +Ltac crush := repeat (program_simplify ; autorewrite with list datatypes ; auto with *). + +Obligation Tactic := crush. + +Program Definition vnil {A} : vector A 0 := {| vec_list := [] |}. + +Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) := + {| vec_list := cons a (vec_list v) |}. + +Hint Rewrite map_length rev_length : datatypes. + +Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n := + {| vec_list := map f v |}. + +Program Definition vreverse {A n} (v : vector A n) : vector A n := + {| vec_list := rev v |}. + +Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B := + match v, w with + | nil, nil => nil + | cons f fs, cons x xs => cons (f x) (va_list fs xs) + | _, _ => nil + end. + +Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n := + {| vec_list := va_list v w |}. + +Next Obligation. + destruct v as [v Hv]; destruct w as [w Hw] ; simpl. + subst n. revert w Hw. induction v ; destruct w ; crush. + rewrite IHv ; auto. +Qed. + +(* Correct type inference of record notation. Initial example by Spiwack. *) + +Inductive Machin := { + Bazar : option Machin +}. + +Definition bli : Machin := + {| Bazar := Some ({| Bazar := None |}:Machin) |}. + +Definition bli' : option (option Machin) := + Some (Some {| Bazar := None |} ). + +Definition bli'' : Machin := + {| Bazar := Some {| Bazar := None |} |}. + +Definition bli''' := {| Bazar := Some {| Bazar := None |} |}. + +(** Correctly use scoping information *) + +Require Import ZArith. + +Record Foo := { bar : Z }. +Definition foo := {| bar := 0 |}. + +(** Notations inside records *) + +Require Import Relation_Definitions. + +Record DecidableOrder : Type := +{ A : Type +; le : relation A where "x <= y" := (le x y) +; le_refl : reflexive _ le +; le_antisym : antisymmetric _ le +; le_trans : transitive _ le +; le_total : forall x y, {x <= y}+{y <= x} +}. diff --git a/test-suite/success/Reordering.v b/test-suite/success/Reordering.v new file mode 100644 index 00000000..de9b9975 --- /dev/null +++ b/test-suite/success/Reordering.v @@ -0,0 +1,15 @@ +(* Testing the reordering of hypothesis required by pattern, fold and change. *) +Goal forall (A:Set) (x:A) (A':=A), True. +intros. +fold A' in x. (* suceeds: x is moved after A' *) +Undo. +pattern A' in x. +Undo. +change A' in x. +Abort. + +(* p and m should be moved before H *) +Goal forall n:nat, n=n -> forall m:nat, let p := (m,n) in True. +intros. +change n with (snd p) in H. +Abort. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index fcce68b9..952890ee 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -12,6 +12,44 @@ intros; apply Znot_le_gt, Zgt_lt in H. apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto. Qed. +(* Test application under tuples *) + +Goal (forall x, x=0 <-> 0=x) -> 1=0 -> 0=1. +intros H H'. +apply H in H'. +exact H'. +Qed. + +(* Test as clause *) + +Goal (forall x, x=0 <-> (0=x /\ True)) -> 1=0 -> True. +intros H H'. +apply H in H' as (_,H'). +exact H'. +Qed. + +(* Test application modulo conversion *) + +Goal (forall x, id x = 0 -> 0 = x) -> 1 = id 0 -> 0 = 1. +intros H H'. +apply H in H'. +exact H'. +Qed. + +(* Check apply/eapply distinction in presence of open terms *) + +Parameter h : forall x y z : nat, x = z -> x = y. +Implicit Arguments h [[x] [y]]. +Goal 1 = 0 -> True. +intro H. +apply h in H || exact I. +Qed. + +Goal False -> 1 = 0. +intro H. +apply h || contradiction. +Qed. + (* Check if it unfolds when there are not enough premises *) Goal forall n, n = S n -> False. @@ -201,3 +239,18 @@ Axiom silly_axiom : forall v : exp, v = v -> False. Lemma silly_lemma : forall x : atom, False. intros x. apply silly_axiom with (v := x). (* fails *) + +(* Test non-regression of (temporary) bug 1981 *) + +Goal exists n : nat, True. +eapply ex_intro. +exact O. +trivial. +Qed. + +(* Test non-regression of (temporary) bug 1980 *) + +Goal True. +try eapply ex_intro. +trivial. +Qed. diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 48255386..488b057f 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -1,10 +1,10 @@ Require Import Coq.Program.Program. -Set Implicit Arguments. -Unset Strict Implicit. +Set Manual Implicit Arguments. + Variable A : Set. -Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall n, vector n -> vector (S n). +Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n). Goal forall n, forall v : vector (S n), vector n. Proof. @@ -35,51 +35,55 @@ Inductive ctx : Type := | empty : ctx | snoc : ctx -> type -> ctx. -Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity). +Bind Scope context_scope with ctx. +Delimit Scope context_scope with ctx. + +Arguments Scope snoc [context_scope]. + +Notation " Γ ,, τ " := (snoc Γ τ) (at level 25, t at next level, left associativity). -Fixpoint conc (Γ Δ : ctx) : ctx := +Fixpoint conc (Δ Γ : ctx) : ctx := match Δ with | empty => Γ - | snoc Δ' x => snoc (conc Γ Δ') x + | snoc Δ' x => snoc (conc Δ' Γ) x end. -Notation " Γ ; Δ " := (conc Γ Δ) (at level 25, left associativity). +Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope. Inductive term : ctx -> type -> Type := -| ax : forall Γ τ, term (Γ, τ) τ -| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ, τ') τ -| abs : forall Γ τ τ', term (Γ , τ) τ' -> term Γ (τ --> τ') +| ax : forall Γ τ, term (snoc Γ τ) τ +| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ ,, τ') τ +| abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ') | app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'. -Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ -> - forall τ', term (Γ , τ' ; Δ) τ. -Proof with simpl in * ; auto ; simpl_depind. +Hint Constructors term : lambda. + +Open Local Scope context_scope. + +Notation " Γ |-- τ " := (term Γ τ) (at level 0) : type_scope. + +Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> + forall τ', term (Γ ,, τ' ;; Δ) τ. +Proof with simpl in * ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda. intros Γ Δ τ H. dependent induction H. destruct Δ... - apply weak ; apply ax. - - apply ax. - - destruct Δ... - specialize (IHterm Γ empty)... - apply weak... - - apply weak... destruct Δ... - apply weak ; apply abs ; apply H. + destruct Δ... apply abs... - specialize (IHterm Γ0 (Δ, t, τ))... + + specialize (IHterm (Δ,, t,, τ)%ctx Γ0)... + intro. apply app with τ... Qed. -Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. -Proof with simpl in * ; simpl_depind ; auto. +Lemma exchange : forall Γ Δ α β τ, term (Γ,, α,, β ;; Δ) τ -> term (Γ,, β,, α ;; Δ) τ. +Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; auto. intros until 1. dependent induction H. @@ -89,12 +93,37 @@ Proof with simpl in * ; simpl_depind ; auto. apply ax. destruct Δ... - pose (weakening (Γ:=Γ0) (Δ:=(empty, α)))... + pose (weakening Γ0 (empty,, α))... apply weak... - apply abs... - specialize (IHterm Γ0 α β (Δ, τ))... + apply abs... + specialize (IHterm (Δ ,, τ))... eapply app with τ... Save. + +(** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *) + +Unset Manual Implicit Arguments. + +Inductive Ty := + | Nat : Ty + | Prod : Ty -> Ty -> Ty. + +Inductive Exp : Ty -> Type := +| Const : nat -> Exp Nat +| Pair : forall t1 t2, Exp t1 -> Exp t2 -> Exp (Prod t1 t2) +| Fst : forall t1 t2, Exp (Prod t1 t2) -> Exp t1. + +Inductive Ev : forall t, Exp t -> Exp t -> Prop := +| EvConst : forall n, Ev (Const n) (Const n) +| EvPair : forall t1 t2 (e1:Exp t1) (e2:Exp t2) e1' e2', + Ev e1 e1' -> Ev e2 e2' -> Ev (Pair e1 e2) (Pair e1' e2') +| EvFst : forall t1 t2 (e:Exp (Prod t1 t2)) e1 e2, + Ev e (Pair e1 e2) -> + Ev (Fst e) e1. + +Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2). +intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption. +Qed. diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v new file mode 100644 index 00000000..b9181d43 --- /dev/null +++ b/test-suite/success/guard.v @@ -0,0 +1,11 @@ +(* Specific tests about guard condition *) + +(* f must unfold to x, not F (de Bruijn mix-up!) *) +Check let x (f:nat->nat) k := f k in + fun (y z:nat->nat) => + let f:=x in (* f := Rel 3 *) + fix F (n:nat) : nat := + match n with + | 0 => 0 + | S k => f F k (* here Rel 3 = F ! *) + end. diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 4b636618..b654277c 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -117,3 +117,8 @@ refine let fn := fact_rec (n-1) _ in n * fn). Abort. + +(* Wish 1988: that fun forces unfold in refine *) + +Goal (forall A : Prop, A -> ~~A). +Proof. refine(fun A a f => _). diff --git a/test-suite/success/rewrite_iterated.v b/test-suite/success/rewrite_iterated.v new file mode 100644 index 00000000..962dada3 --- /dev/null +++ b/test-suite/success/rewrite_iterated.v @@ -0,0 +1,30 @@ +Require Import Arith Omega. + +Lemma test : forall p:nat, p<>0 -> p-1+1=p. +Proof. + intros; omega. +Qed. + +(** Test of new syntax for rewrite : ! ? and so on... *) + +Lemma but : forall a b c, a<>0 -> b<>0 -> c<>0 -> + (a-1+1)+(b-1+1)+(c-1+1)=a+b+c. +Proof. +intros. +rewrite test. +Undo. +rewrite test,test. +Undo. +rewrite 2 test. (* or rewrite 2test or rewrite 2!test *) +Undo. +rewrite 2!test,2?test. +Undo. +(*rewrite 4!test. --> error *) +rewrite 3!test. +Undo. +rewrite <- 3?test. +Undo. +(*rewrite <-?test. --> loops*) +rewrite !test by auto. +reflexivity. +Qed. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index f49f58e5..be5999df 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -116,3 +116,17 @@ Add Morphism (@f A) : f_morph. Proof. unfold rel, f. trivial. Qed. + +(* Submitted by Nicolas Tabareau *) +(* Needs unification.ml to support environments with de Bruijn *) + +Goal forall + (f : Prop -> Prop) + (Q : (nat -> Prop) -> Prop) + (H : forall (h : nat -> Prop), Q (fun x : nat => f (h x)) <-> True) + (h:nat -> Prop), + Q (fun x : nat => f (Q (fun b : nat => f (h x)))) <-> True. +intros f0 Q H. +setoid_rewrite H. +tauto. +Qed. diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index 8d32b1d9..b4de4932 100644 --- a/test-suite/success/simpl.v +++ b/test-suite/success/simpl.v @@ -21,4 +21,27 @@ with copy_of_compute_size_tree (t:tree) : nat := Eval simpl in (copy_of_compute_size_forest leaf). +(* Another interesting case: Hrec has to occurrences: one cannot be folded + back to f while the second can. *) +Parameter g : (nat->nat)->nat->nat->nat. +Definition f (n n':nat) := + nat_rec (fun _ => nat -> nat) + (fun x => x) + (fun k Hrec => g Hrec (Hrec k)) + n n'. + +Goal forall a b, f (S a) b = b. +intros. +simpl. +admit. +Qed. (* Qed will fail if simpl performs eta-expansion *) + +(* Yet another example. *) + +Require Import List. + +Goal forall A B (a:A) l f (i:B), fold_right f i ((a :: l))=i. +simpl. +admit. +Qed. (* Qed will fail if simplification is incorrect (de Bruijn!) *) diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v index 19e306fe..8b7764e5 100644 --- a/test-suite/success/unicode_utf8.v +++ b/test-suite/success/unicode_utf8.v @@ -1,12 +1,104 @@ -(* Check correct separation of identifiers followed by unicode symbols *) - Notation "x 〈 w" := (plus x w) (at level 30). - Check fun x => x〈x. +(** PARSER TESTS *) -(* Check Greek letters *) +(** Check correct separation of identifiers followed by unicode symbols *) +Notation "x ⊕ w" := (plus x w) (at level 30). +Check fun x => x⊕x. + +(** Check Greek letters *) Definition test_greek : nat -> nat := fun Δ => Δ. Parameter ℝ : Set. Parameter π : ℝ. -(* Check indices *) +(** Check indices *) Definition test_indices : nat -> nat := fun x₁ => x₁. Definition π₂ := snd. + +(** More unicode in identifiers *) +Definition αβ_áà_אב := 0. + + +(** UNICODE IN STRINGS *) + +Require Import List Ascii String. +Open Scope string_scope. + +Definition test_string := "azertyαβ∀ééé". +Eval compute in length test_string. + (** last six "chars" are unicode, hence represented by 2 bytes, + except the forall which is 3 bytes *) + +Fixpoint string_to_list s := + match s with + | EmptyString => nil + | String c s => c :: string_to_list s + end. + +Eval compute in (string_to_list test_string). + (** for instance, α is \206\177 whereas ∀ is \226\136\128 *) +Close Scope string_scope. + + + +(** INTERFACE TESTS *) + +Require Import Utf8. + +(** Printing of unicode notation, in *goals* *) +Lemma test : forall A:Prop, A -> A. +Proof. +auto. +Qed. + +(** Parsing of unicode notation, in *goals* *) +Lemma test2 : ∀A:Prop, A → A. +Proof. +intro. +intro. +auto. +Qed. + +(** Printing of unicode notation, in *response* *) +Check fun (X:Type)(x:X) => x. + +(** Parsing of unicode notation, in *response* *) +Check ∀Δ, Δ → Δ. +Check ∀x, x=0 ∨ x=0 → x=0. + + +(** ISSUES: *) + +Notation "x ≠ y" := (x<>y) (at level 70). + +Notation "x ≤ y" := (x<=y) (at level 70, no associativity). + +(** First Issue : ≤ is attached to "le" of nat, not to notation <= *) + +Require Import ZArith. +Open Scope Z_scope. +Locate "≤". (* still le, not Zle *) +Notation "x ≤ y" := (x<=y) (at level 70, no associativity). +Locate "≤". +Close Scope Z_scope. + +(** ==> How to proceed modularly ? *) + + +(** Second Issue : notation for -> generates useless parenthesis + if followed by a binder *) + +Check 0≠0 → ∀x:nat,x=x. + +(** Example of real situation : *) + +Definition pred : ∀x, x≠0 → ∃y, x = S y. +Proof. +destruct x. +destruct 1; auto. +intros _. +exists x; auto. +Defined. + +Print pred. + + + |