diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_5617.v | 8 | ||||
| -rw-r--r-- | test-suite/micromega/bug_11436.v | 19 | ||||
| -rw-r--r-- | test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v | 4 | ||||
| -rw-r--r-- | test-suite/micromega/square.v | 10 | ||||
| -rw-r--r-- | test-suite/output/Notations5.out | 248 | ||||
| -rw-r--r-- | test-suite/output/Notations5.v | 340 |
6 files changed, 622 insertions, 7 deletions
diff --git a/test-suite/bugs/closed/bug_5617.v b/test-suite/bugs/closed/bug_5617.v new file mode 100644 index 0000000000..c18e79295c --- /dev/null +++ b/test-suite/bugs/closed/bug_5617.v @@ -0,0 +1,8 @@ +Set Primitive Projections. +Record T X := { F : X }. + +Fixpoint f (n : nat) : nat := +match n with +| 0 => 0 +| S m => F _ {| F := f |} m +end. diff --git a/test-suite/micromega/bug_11436.v b/test-suite/micromega/bug_11436.v new file mode 100644 index 0000000000..fc6ccbb233 --- /dev/null +++ b/test-suite/micromega/bug_11436.v @@ -0,0 +1,19 @@ +Require Import ZArith Lia. +Local Open Scope Z_scope. + +Unset Lia Cache. + +Goal forall a q q0 q1 r r0 r1: Z, + 0 <= a < 2 ^ 64 -> + r1 = 4 * q + r -> + 0 <= r < 4 -> + a = 4 * q0 + r0 -> + 0 <= r0 < 4 -> + a + 4 = 2 ^ 64 * q1 + r1 -> + 0 <= r1 < 2 ^ 64 -> + r = r0. +Proof. + intros. + (* subst. *) + Time lia. +Qed. diff --git a/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v new file mode 100644 index 0000000000..a53c160e45 --- /dev/null +++ b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v @@ -0,0 +1,4 @@ +Require Import Lia. +Goal forall n (B: n >= 0), exists Goal1 Goal2 Goal3, + (0 * (Goal1 * Goal2 + Goal1) <> Goal3 * 0 * (Goal1 * S Goal2)). +Proof. eexists _, _, _. Fail lia. Abort. diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 9efb81a901..36b4243ef8 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -11,15 +11,14 @@ Open Scope Z_scope. Lemma Zabs_square : forall x, (Z.abs x)^2 = x^2. Proof. - intros ; case (Zabs_dec x) ; intros ; nia. + intros ; nia. Qed. -Hint Resolve Z.abs_nonneg Zabs_square. Lemma integer_statement : ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0. Proof. intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p). assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2 - /\ Z.abs p^2 = p^2) by auto. + /\ Z.abs p^2 = p^2) by auto using Z.abs_nonneg, Zabs_square. assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; nia). generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear. @@ -45,10 +44,7 @@ Proof. intros. destruct x. simpl. - unfold Z.pow_pos. - simpl. - rewrite Pos.mul_1_r. - reflexivity. + lia. Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out new file mode 100644 index 0000000000..83dd2f40fb --- /dev/null +++ b/test-suite/output/Notations5.out @@ -0,0 +1,248 @@ +p 0 0 true + : 0 = 0 /\ true = true +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +p 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p (A:=nat) + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +p (A:=nat) + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@p + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +p + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 0 true + : 0 = 0 /\ true = true +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +p + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +p + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@p + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +f x true + : 0 = 0 /\ true = true +f x (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +f x (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +@f nat + : forall a1 a2 : nat, + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +@f + : forall (A : Type) (a1 a2 : A), + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +x.(f) true + : 0 = 0 /\ true = true +x.(f) (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +x.(f) (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +@f nat + : forall a1 a2 : nat, + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +@f + : forall (A : Type) (a1 a2 : A), + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +p + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +p + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +u + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +u + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +u 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +u 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +@u nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@u nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +u 0 0 true + : 0 = 0 /\ true = true +u 0 0 true + : 0 = 0 /\ true = true +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 (B:=bool) true + : 0 = 0 /\ true = true +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +v 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 (B:=bool) true + : 0 = 0 /\ true = true +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +v 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +## + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +## 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +## + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +## + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p 0 0 true + : 0 = 0 /\ true = true +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v new file mode 100644 index 0000000000..b3bea929ba --- /dev/null +++ b/test-suite/output/Notations5.v @@ -0,0 +1,340 @@ +Module AppliedTermsPrinting. + +(* Test different printing paths for applied terms *) + + Module InferredGivenImplicit. + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Check p 0 0 true. + (* p 0 0 true *) + Check p 0 0. + (* p 0 0 *) + Check p 0. + (* p 0 *) + Check @p _ 0 0 bool. + (* p 0 0 (B:=bool) *) + Check p 0 0 (B:=bool). + (* p 0 0 (B:=bool) *) + Check @p nat. + (* p (A:=nat) *) + Check p (A:=nat). + (* p (A:=nat) *) + Check @p _ 0 0. + (* @p nat 0 0 *) + Check @p. + (* @p *) + + Unset Printing Implicit Defensive. + Check @p _ 0 0 bool. + (* p 0 0 *) + Check @p nat. + (* p *) + Set Printing Implicit Defensive. + End InferredGivenImplicit. + + Module ManuallyGivenImplicit. + Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b. + + Check p 0 0 true. + (* p 0 0 true *) + Check p 0 0. + (* p 0 0 *) + Check p 0. + (* p 0 *) + Check @p _ 0 0 bool. + (* p 0 0 *) + Check p 0 0 (B:=bool). + (* p 0 0 *) + Check @p nat. + (* p *) + Check p (A:=nat). + (* p *) + Check @p _ 0 0. + (* @p nat 0 0 *) + Check @p. + (* @p *) + + End ManuallyGivenImplicit. + + Module ProjectionWithImplicits. + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Record T {A} (a1 a2:A) := { f : forall B (b:B), a1 = a2 /\ b = b }. + Parameter x : T 0 0. + Check f x true. + (* f x true *) + Check @f _ _ _ x bool. + (* f x (B:=bool) *) + Check f x (B:=bool). + (* f x (B:=bool) *) + Check @f nat. + (* @f nat *) + Check @f _ 0 0. + (* f (a1:=0) (a2:=0) *) + Check f (a1:=0) (a2:=0). + (* f (a1:=0) (a2:=0) *) + Check @f. + (* @f *) + + Unset Printing Implicit Defensive. + Check f (a1:=0) (a2:=0). + (* f *) + Set Printing Implicit Defensive. + + Set Printing Projections. + + Check x.(f) true. + (* x.(f) true *) + Check x.(@f _ _ _) bool. + (* x.(f) (B:=bool) *) + Check x.(f) (B:=bool). + (* x.(f) (B:=bool) *) + Check @f nat. + (* @f nat *) + Check @f _ 0 0. + (* f (a1:=0) (a2:=0) *) + Check f (a1:=0) (a2:=0). + (* f (a1:=0) (a2:=0) *) + Check @f. + (* @f *) + + Unset Printing Implicit Defensive. + Check f (a1:=0) (a2:=0). + (* f *) + + End ProjectionWithImplicits. + + Module AtAbbreviationForApplicationHead. + + Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b. + + Notation u := @p. + + Check u _. + (* p *) + Check p. + (* p *) + Check @p. + (* u *) + Check u. + (* u *) + Check p 0 0. + (* p 0 0 *) + Check u nat 0 0 bool. + (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *) + Check u nat 0 0. + (* @p nat 0 0 *) + Check @p nat 0 0. + (* @p nat 0 0 *) + + End AtAbbreviationForApplicationHead. + + Module AbbreviationForApplicationHead. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation u := p. + + Check p. + (* u *) + Check @p. + (* u -- BUG *) + Check @u. + (* u -- BUG *) + Check u. + (* u *) + Check p 0 0. + (* u 0 0 *) + Check u 0 0. + (* u 0 0 *) + Check @p nat 0 0. + (* @u nat 0 0 *) + Check @u nat 0 0. + (* @u nat 0 0 *) + Check p 0 0 true. + (* u 0 0 true *) + Check u 0 0 true. + (* u 0 0 true *) + + End AbbreviationForApplicationHead. + + Module AtAbbreviationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation v := (@p _ 0). + + Check v. + (* v *) + Check p 0 0. + (* v 0 *) + Check v 0. + (* v 0 *) + Check v 0 true. + (* v 0 (B:=bool) true -- BUG *) + Check @p nat 0. + (* v *) + Check @p nat 0 0. + (* @v 0 *) + Check @v 0. + (* @v 0 *) + Check @p nat 0 0 bool. + (* v 0 (B:=bool) *) + + End AtAbbreviationForPartialApplication. + + Module AbbreviationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation v := (p 0). + + Check v. + (* v *) + Check p 0 0. + (* v 0 *) + Check v 0. + (* v 0 *) + Check v 0 true. + (* v 0 (B:=bool) true -- BUG *) + Check @p nat 0. + (* v *) + Check @p nat 0 0. + (* @v 0 *) + Check @v 0. + (* @v 0 *) + Check @p nat 0 0 bool. + (* v 0 (B:=bool) *) + + End AbbreviationForPartialApplication. + + Module NotationForHeadApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "##" := p (at level 0). + + Check p. + (* ## *) + Check ##. + (* ## *) + Check p 0. + (* ## 0 *) + Check ## 0. + (* ## 0 *) + Check p 0 0. + (* ## 0 0 *) + Check ## 0 0. + (* ## 0 0 *) + Check p 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check ## 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check p 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + Check ## 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + + End NotationForHeadApplication. + + Module AtNotationForHeadApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "##" := @p (at level 0). + + Check p. + (* p *) + Check @p. + (* ## *) + Check ##. + (* ## *) + Check p 0. + (* p 0 -- why not "## nat 0" *) + Check ## nat 0. + (* p 0 *) + Check ## nat 0 0. + (* @p nat 0 0 *) + Check p 0 0. + (* p 0 0 *) + Check ## nat 0 0 _. + (* p 0 0 *) + Check ## nat 0 0 bool. + (* p 0 0 (B:=bool) *) + Check ## nat 0 0 bool true. + (* p 0 0 true *) + + End AtNotationForHeadApplication. + + Module NotationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "## q" := (p q) (at level 0, q at level 0). + + Check p 0. + (* ## 0 *) + Check ## 0. + (* ## 0 *) + (* Check ## 0 0. *) + (* Anomaly *) + Check p 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + Check ## 0 0 bool. + (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) + Check p 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check ## 0 0 bool true. + (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *) + + End NotationForPartialApplication. + + Module AtNotationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "## q" := (@p _ q) (at level 0, q at level 0). + + Check p 0. + (* ## 0 *) + Check ## 0. + (* ## 0 *) + (* Check ## 0 0. *) + (* Anomaly *) + Check p 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + Check ## 0 0 bool. + (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) + Check p 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check ## 0 0 bool true. + (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *) + + End AtNotationForPartialApplication. + +End AppliedTermsPrinting. |