diff options
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/148.v | 26 | ||||
-rw-r--r-- | test-suite/output/Notations3.out | 4 | ||||
-rw-r--r-- | test-suite/output/Notations3.v | 7 | ||||
-rw-r--r-- | test-suite/success/ROmega4.v | 26 | ||||
-rw-r--r-- | test-suite/success/setoid_test.v | 10 | ||||
-rw-r--r-- | test-suite/success/setoid_test2.v | 16 |
6 files changed, 76 insertions, 13 deletions
diff --git a/test-suite/bugs/closed/148.v b/test-suite/bugs/closed/148.v new file mode 100644 index 000000000..6cafb9f0c --- /dev/null +++ b/test-suite/bugs/closed/148.v @@ -0,0 +1,26 @@ +(** Omega is now aware of the bodies of context variables + (of type Z or nat). *) + +Require Import ZArith Omega. +Open Scope Z. + +Goal let x := 3 in x = 3. +intros. +omega. +Qed. + +Open Scope nat. + +Goal let x := 2 in x = 2. +intros. +omega. +Qed. + +(** NB: this could be disabled for compatibility reasons *) + +Unset Omega UseLocalDefs. + +Goal let x := 4 in x = 4. +intros. +Fail omega. +Abort. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 65efe228a..6ef75dd13 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -124,3 +124,7 @@ return (1, 2, 3, 4) : nat !!! _ _ : nat, True : (nat -> Prop) * ((nat -> Prop) * Prop) +((*1).2).3 + : nat +*(1.2) + : nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index ea372ad1a..8c7bbe591 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -190,3 +190,10 @@ Check 1+1+1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). Check !!! (x y:nat), True. + +(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) + +Notation "* x" := (id x) (only printing, at level 15, format "* x"). +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Check (((id 1) + 2) + 3). +Check (id (1 + 2)). diff --git a/test-suite/success/ROmega4.v b/test-suite/success/ROmega4.v new file mode 100644 index 000000000..58ae5b8fb --- /dev/null +++ b/test-suite/success/ROmega4.v @@ -0,0 +1,26 @@ +(** ROmega is now aware of the bodies of context variables + (of type Z or nat). + See also #148 for the corresponding improvement in Omega. +*) + +Require Import ZArith ROmega. +Open Scope Z. + +Goal let x := 3 in x = 3. +intros. +romega. +Qed. + +(** Example seen in #4132 + (actually solvable even if b isn't known to be 5) *) + +Lemma foo + (x y x' zxy zxy' z : Z) + (b := 5) + (Ry : - b <= y < b) + (Bx : x' <= b) + (H : - zxy' <= zxy) + (H' : zxy' <= x') : - b <= zxy. +Proof. +romega. +Qed. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 1f24ef2a6..c8dfcd2cb 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -33,7 +33,8 @@ Qed. Add Setoid set same setoid_set as setsetoid. -Add Morphism In : In_ext. +Add Morphism In with signature (eq ==> same ==> iff) as In_ext. +Proof. unfold same; intros a s t H; elim (H a); auto. Qed. @@ -50,10 +51,9 @@ simpl; right. apply (H2 H1). Qed. -Add Morphism Add : Add_ext. +Add Morphism Add with signature (eq ==> same ==> same) as Add_ext. split; apply add_aux. assumption. - rewrite H. reflexivity. Qed. @@ -90,7 +90,7 @@ Qed. Parameter P : set -> Prop. Parameter P_ext : forall s t : set, same s t -> P s -> P t. -Add Morphism P : P_extt. +Add Morphism P with signature (same ==> iff) as P_extt. intros; split; apply P_ext; (assumption || apply (Seq_sym _ _ setoid_set); assumption). Qed. @@ -113,7 +113,7 @@ Definition f: forall A : Set, A -> A := fun A x => x. Add Relation (id A) (rel A) as eq_rel. -Add Morphism (@f A) : f_morph. +Add Morphism (@f A) with signature (eq ==> eq) as f_morph. Proof. unfold rel, f. trivial. Qed. diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v index 6baf79701..79467e549 100644 --- a/test-suite/success/setoid_test2.v +++ b/test-suite/success/setoid_test2.v @@ -134,8 +134,8 @@ Axiom SetoidS2 : Setoid_Theory S2 eqS2. Add Setoid S2 eqS2 SetoidS2 as S2setoid. Axiom f : S1 -> nat -> S2. -Add Morphism f : f_compat. Admitted. -Add Morphism f : f_compat2. Admitted. +Add Morphism f with signature (eqS1 ==> eq ==> eqS2) as f_compat. Admitted. +Add Morphism f with signature (eqS1 ==> eq ==> eqS2) as f_compat2. Admitted. Theorem test1: forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)). intros. @@ -151,7 +151,7 @@ Theorem test1': forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)). Qed. Axiom g : S1 -> S2 -> nat. -Add Morphism g : g_compat. Admitted. +Add Morphism g with signature (eqS1 ==> eqS2 ==> eq) as g_compat. Admitted. Axiom P : nat -> Prop. Theorem test2: @@ -190,13 +190,13 @@ Theorem test5: Qed. Axiom f_test6 : S2 -> Prop. -Add Morphism f_test6 : f_test6_compat. Admitted. +Add Morphism f_test6 with signature (eqS2 ==> iff) as f_test6_compat. Admitted. Axiom g_test6 : bool -> S2. -Add Morphism g_test6 : g_test6_compat. Admitted. +Add Morphism g_test6 with signature (eq ==> eqS2) as g_test6_compat. Admitted. Axiom h_test6 : S1 -> bool. -Add Morphism h_test6 : h_test6_compat. Admitted. +Add Morphism h_test6 with signature (eqS1 ==> eq) as h_test6_compat. Admitted. Theorem test6: forall E1 E2, (eqS1 E1 E2) -> (f_test6 (g_test6 (h_test6 E2))) -> @@ -223,7 +223,7 @@ Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid. Instance eqS1_test8_default : DefaultRelation eqS1_test8. Axiom f_test8 : S2 -> S1_test8. -Add Morphism f_test8 : f_compat_test8. Admitted. +Add Morphism f_test8 with signature (eqS2 ==> eqS1_test8) as f_compat_test8. Admitted. Axiom eqS1_test8': S1_test8 -> S1_test8 -> Prop. Axiom SetoidS1_test8' : Setoid_Theory S1_test8 eqS1_test8'. @@ -233,7 +233,7 @@ Add Setoid S1_test8 eqS1_test8' SetoidS1_test8' as S1_test8setoid'. (S1_test8, eqS1_test8'). However this does not happen and there is still no syntax for it ;-( *) Axiom g_test8 : S1_test8 -> S2. -Add Morphism g_test8 : g_compat_test8. Admitted. +Add Morphism g_test8 with signature (eqS1_test8 ==> eqS2) as g_compat_test8. Admitted. Theorem test8: forall x x': S2, (eqS2 x x') -> |