From f0ff590f380fb3d9fac6ebfdd6cfd7bf6874658e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 10 Nov 2015 18:43:07 +0100 Subject: Updating test-suite after Bracketing Last Introduction Pattern set by default. Interestingly, there is an example where it makes the rest of the proof less natural. Goal forall x y:Z, ... intros [y|p1[|p2|p2]|p1[|p2|p2]]. where case analysis on y is not only in the 2nd and 3rd case, is not anymore easy to do. Still, I find the bracketing of intro-patterns a natural property, and its generalization in all situations a natural expectation for uniformity. So, what to do? The following is e.g. not as compact and "one-shot": intros [|p1|p1]; [intros y|intros [|p2|p2] ..]. --- test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'test-suite/stm') diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v index 0d75d52a3..06357cfc2 100644 --- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v +++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v @@ -1902,14 +1902,14 @@ Qed. Lemma Zsgn_15 : forall x y : Z, Zsgn (x * y) = (Zsgn x * Zsgn y)%Z. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; constructor. + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; constructor. Qed. Lemma Zsgn_16 : forall x y : Z, Zsgn (x * y) = 1%Z -> {(0 < x)%Z /\ (0 < y)%Z} + {(x < 0)%Z /\ (y < 0)%Z}. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H; try discriminate H; [ left | right ]; repeat split. Qed. @@ -1917,13 +1917,13 @@ Lemma Zsgn_17 : forall x y : Z, Zsgn (x * y) = (-1)%Z -> {(0 < x)%Z /\ (y < 0)%Z} + {(x < 0)%Z /\ (0 < y)%Z}. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H; try discriminate H; [ left | right ]; repeat split. Qed. Lemma Zsgn_18 : forall x y : Z, Zsgn (x * y) = 0%Z -> {x = 0%Z} + {y = 0%Z}. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H; try discriminate H; [ left | right | right ]; constructor. Qed. @@ -1932,40 +1932,40 @@ Qed. Lemma Zsgn_19 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 < x + y)%Z. Proof. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H; discriminate H || (constructor || apply Zsgn_12; assumption). Qed. Lemma Zsgn_20 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (x + y < 0)%Z. Proof. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H; discriminate H || (constructor || apply Zsgn_11; assumption). Qed. Lemma Zsgn_21 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 <= x)%Z. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intros H H0; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0; discriminate H || discriminate H0. Qed. Lemma Zsgn_22 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (x <= 0)%Z. Proof. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intros H H0; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0; discriminate H || discriminate H0. Qed. Lemma Zsgn_23 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 <= y)%Z. Proof. - intros [[| p2| p2]| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; + intros [|p1|p1] [|p2|p2]; simpl in |- *; intros H H0; discriminate H || discriminate H0. Qed. Lemma Zsgn_24 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (y <= 0)%Z. Proof. - intros [[| p2| p2]| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; + intros [|p1|p1] [|p2|p2]; simpl in |- *; intros H H0; discriminate H || discriminate H0. Qed. -- cgit v1.2.3