From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 25 Dec 2011 13:19:42 +0100 Subject: Imported Upstream version 8.3.pl3 --- test-suite/bench/lists-100.v | 2 +- test-suite/bench/lists_100.v | 2 +- test-suite/bugs/closed/shouldsucceed/2464.v | 39 ++++++++++ test-suite/bugs/closed/shouldsucceed/2467.v | 49 +++++++++++++ test-suite/bugs/closed/shouldsucceed/2608.v | 34 +++++++++ test-suite/bugs/closed/shouldsucceed/808_2411.v | 27 +++++++ test-suite/failure/Tauto.v | 2 +- test-suite/failure/clash_cons.v | 2 +- test-suite/failure/fixpoint1.v | 2 +- test-suite/failure/guard.v | 2 +- test-suite/failure/illtype1.v | 2 +- test-suite/failure/positivity.v | 2 +- test-suite/failure/redef.v | 2 +- test-suite/failure/search.v | 2 +- test-suite/ideal-features/Apply.v | 2 +- test-suite/misc/berardi_test.v | 2 +- test-suite/output/PrintAssumptions.out | 18 +++++ test-suite/output/PrintAssumptions.v | 96 +++++++++++++++++++++++++ test-suite/success/Check.v | 2 +- test-suite/success/Field.v | 4 +- test-suite/success/LegacyField.v | 2 +- test-suite/success/Tauto.v | 4 +- test-suite/success/TestRefine.v | 2 +- test-suite/success/eauto.v | 2 +- test-suite/success/eqdecide.v | 2 +- test-suite/success/extraction.v | 2 +- test-suite/success/inds_type_sec.v | 2 +- test-suite/success/induct.v | 2 +- test-suite/success/mutual_ind.v | 2 +- test-suite/success/unfold.v | 2 +- test-suite/typeclasses/NewSetoid.v | 2 +- 31 files changed, 290 insertions(+), 27 deletions(-) create mode 100644 test-suite/bugs/closed/shouldsucceed/2464.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2467.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2608.v create mode 100644 test-suite/bugs/closed/shouldsucceed/808_2411.v create mode 100644 test-suite/output/PrintAssumptions.out create mode 100644 test-suite/output/PrintAssumptions.v (limited to 'test-suite') diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v index 3d145d96..490de2a6 100644 --- a/test-suite/bench/lists-100.v +++ b/test-suite/bench/lists-100.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* o}. + +Module DecidableName. +Definition t := Name. +Definition eq := @eq Name. +Definition eq_refl := @refl_equal Name. +Definition eq_sym := @sym_eq Name. +Definition eq_trans := @trans_eq Name. +Definition eq_dec := eq_Name_dec. +End DecidableName. + +Module NameSetMod := Make(DecidableName). + +Module NameSetDec := WDecide (NameSetMod). + +Class PartPatchUniverse (pu_type1 pu_type2 : Type) + : Type := mkPartPatchUniverse { +}. +Class PatchUniverse {pu_type : Type} + (ppu : PartPatchUniverse pu_type pu_type) + : Type := mkPatchUniverse { + pu_nameOf : pu_type -> Name +}. + +Lemma foo : forall (pu_type : Type) + (ppu : PartPatchUniverse pu_type pu_type) + (patchUniverse : PatchUniverse ppu) + (ns ns1 ns2 : NameSetMod.t) + (containsOK : NameSetMod.Equal ns1 ns2) + (p : pu_type) + (HX1 : NameSetMod.Equal ns1 (NameSetMod.add (pu_nameOf p) ns)), + NameSetMod.Equal ns2 (NameSetMod.add (pu_nameOf p) ns). +Proof. +NameSetDec.fsetdec. +Qed. \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2467.v b/test-suite/bugs/closed/shouldsucceed/2467.v new file mode 100644 index 00000000..ad17814a --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2467.v @@ -0,0 +1,49 @@ +(* +In the code below, I would expect the + NameSetDec.fsetdec. +to solve the Lemma, but I need to do it in steps instead. + +This is a regression relative to FSet, + +I have v8.3 (13702). +*) + +Require Import Coq.MSets.MSets. + +Parameter Name : Set. +Parameter Name_compare : Name -> Name -> comparison. +Parameter Name_compare_sym : forall {x y : Name}, + Name_compare y x = CompOpp (Name_compare x y). +Parameter Name_compare_trans : forall {c : comparison} + {x y z : Name}, + Name_compare x y = c + -> Name_compare y z = c + -> Name_compare x z = c. +Parameter Name_eq_leibniz : forall {s s' : Name}, + Name_compare s s' = Eq + -> s = s'. + +Module NameOrderedTypeAlt. +Definition t := Name. +Definition compare := Name_compare. +Definition compare_sym := @Name_compare_sym. +Definition compare_trans := @Name_compare_trans. +End NameOrderedTypeAlt. + +Module NameOrderedType := OT_from_Alt(NameOrderedTypeAlt). + +Module NameOrderedTypeWithLeibniz. +Include NameOrderedType. +Definition eq_leibniz := @Name_eq_leibniz. +End NameOrderedTypeWithLeibniz. + +Module NameSetMod := MSetList.MakeWithLeibniz(NameOrderedTypeWithLeibniz). +Module NameSetDec := WDecide (NameSetMod). + +Lemma foo : forall (xs ys : NameSetMod.t) + (n : Name) + (H1 : NameSetMod.Equal xs (NameSetMod.add n ys)), + NameSetMod.In n xs. +Proof. +NameSetDec.fsetdec. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2608.v b/test-suite/bugs/closed/shouldsucceed/2608.v new file mode 100644 index 00000000..a4c95ff9 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2608.v @@ -0,0 +1,34 @@ + +Module Type T. + Parameter Inline t : Type. +End T. + +Module M. + Definition t := nat. +End M. + +Module Make (X:T). + Include X. + + (* here t is : (Top.Make.t,Top.X.t) *) + + (* in libobject HEAD : EvalConstRef (Top.X.t,Top.X.t) + which is substituted by : {Top.X |-> Top.Make [, Top.Make.t=>Top.X.t]} + which gives : EvalConstRef (Top.Make.t,Top.X.t) *) + +End Make. + +Module P := Make M. + + (* resolver returned by add_module : Top.P.t=>inline *) + (* then constant_of_delta_kn P.t produces (Top.P.t,Top.P.t) *) + + (* in libobject HEAD : EvalConstRef (Top.Make.t,Top.X.t) + given to subst = { |-> Top.M [, Top.M.t=>inline]} + which used to give : EvalConstRef (Top.Make.t,Top.M.t) + given to subst = {Top.Make |-> Top.P [, Top.P.t=>inline]} + which used to give : EvalConstRef (Top.P.t,Top.M.t) *) + +Definition u := P.t. + (* was raising Not_found since Heads.head_map knows of (Top.P.t,Top.M.t) + and not of (Top.P.t,Top.P.t) *) diff --git a/test-suite/bugs/closed/shouldsucceed/808_2411.v b/test-suite/bugs/closed/shouldsucceed/808_2411.v new file mode 100644 index 00000000..1c13e745 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/808_2411.v @@ -0,0 +1,27 @@ +Section test. +Variable n:nat. +Lemma foo: 0 <= n. +Proof. +(* declaring an Axiom during a proof makes it immediatly + usable, juste as a full Definition. *) +Axiom bar : n = 1. +rewrite bar. +now apply le_S. +Qed. + +Lemma foo' : 0 <= n. +Proof. +(* Declaring an Hypothesis during a proof is ok, + but this hypothesis won't be usable by the current proof(s), + only by later ones. *) +Hypothesis bar' : n = 1. +Fail rewrite bar'. +Abort. + +Lemma foo'' : 0 <= n. +Proof. +rewrite bar'. +now apply le_S. +Qed. + +End test. \ No newline at end of file diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index a08c5154..96e66a0d 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Q), + (forall x : P, f x = g x) -> f = g +Axioms: +extensionality : forall (P Q : Type) (f g : P -> Q), + (forall x : P, f x = g x) -> f = g +Axioms: +extensionality : forall (P Q : Type) (f g : P -> Q), + (forall x : P, f x = g x) -> f = g +Axioms: +extensionality : forall (P Q : Type) (f g : P -> Q), + (forall x : P, f x = g x) -> f = g +Closed under the global context +Closed under the global context diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v new file mode 100644 index 00000000..f23bc498 --- /dev/null +++ b/test-suite/output/PrintAssumptions.v @@ -0,0 +1,96 @@ + +(** Print Assumption and opaque modules : + + Print Assumption used to consider as axioms the modular fields + unexported by their signature, cf bug report #2186. This should + now be fixed, let's test this here. *) + +(* First, a minimal test-case *) + +Axiom foo : nat. + +Module Type T. + Parameter bar : nat. +End T. + +Module M : T. + Module Hide. (* An entire sub-module could be hidden *) + Definition x := foo. + End Hide. + Definition bar := Hide.x. +End M. + +Module N (X:T) : T. + Definition y := X.bar. (* A non-exported field *) + Definition bar := y. +End N. + +Module P := N M. + +Print Assumptions M.bar. (* Should answer: foo *) +Print Assumptions P.bar. (* Should answer: foo *) + + +(* The original test-case of the bug-report *) + +Require Import Arith. + +Axiom extensionality : forall P Q (f g:P -> Q), + (forall x, f x = g x) -> f = g. + +Module Type ADD_COMM_EXT. + Axiom add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x). +End ADD_COMM_EXT. + +Module AddCommExt_Opaque : ADD_COMM_EXT. + Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x). + Proof. + intro n; apply extensionality; auto with arith. + Qed. +End AddCommExt_Opaque. + +Module AddCommExt_Transparent <: ADD_COMM_EXT. + Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x). + Proof. + intro n; apply extensionality; auto with arith. + Qed. +End AddCommExt_Transparent. + +Print Assumptions AddCommExt_Opaque.add_comm_ext. +(* Should answer: extensionality *) + +Print Assumptions AddCommExt_Transparent.add_comm_ext. +(* Should answer: extensionality *) + +Lemma add1_comm_ext_opaque : + (fun x => x + 1) = (fun x => 1 + x). +Proof (AddCommExt_Opaque.add_comm_ext 1). + +Lemma add1_comm_ext_transparent : + (fun x => x + 1) = (fun x => 1 + x). +Proof (AddCommExt_Transparent.add_comm_ext 1). + +Print Assumptions add1_comm_ext_opaque. +(* Should answer: extensionality *) + +Print Assumptions add1_comm_ext_transparent. +(* Should answer: extensionality *) + +Module Type FALSE_POSITIVE. + Axiom add_comm : forall n x, x + n = n + x. +End FALSE_POSITIVE. + +Module false_positive : FALSE_POSITIVE. + Lemma add_comm : forall n x, x + n = n + x. + Proof. auto with arith. Qed. + + Print Assumptions add_comm. + (* Should answer : Closed under the global context *) +End false_positive. + +Lemma comm_plus5 : forall x, + x + 5 = 5 + x. +Proof (false_positive.add_comm 5). + +Print Assumptions comm_plus5. +(* Should answer : Closed under the global context *) diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 47180ef6..d5b94ab4 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*