From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- test-suite/success/ROmega0.v | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) (limited to 'test-suite/success/ROmega0.v') diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v index 86cf49cb..1348bb62 100644 --- a/test-suite/success/ROmega0.v +++ b/test-suite/success/ROmega0.v @@ -3,24 +3,24 @@ Open Scope Z_scope. (* Pierre L: examples gathered while debugging romega. *) -Lemma test_romega_0 : - forall m m', +Lemma test_romega_0 : + forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros. romega. Qed. -Lemma test_romega_0b : - forall m m', +Lemma test_romega_0b : + forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros m m'. romega. Qed. -Lemma test_romega_1 : - forall (z z1 z2 : Z), +Lemma test_romega_1 : + forall (z z1 z2 : Z), z2 <= z1 -> z1 <= z2 -> z1 >= 0 -> @@ -32,8 +32,8 @@ intros. romega. Qed. -Lemma test_romega_1b : - forall (z z1 z2 : Z), +Lemma test_romega_1b : + forall (z z1 z2 : Z), z2 <= z1 -> z1 <= z2 -> z1 >= 0 -> @@ -45,42 +45,42 @@ intros z z1 z2. romega. Qed. -Lemma test_romega_2 : forall a b c:Z, +Lemma test_romega_2 : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros. romega. Qed. -Lemma test_romega_2b : forall a b c:Z, +Lemma test_romega_2b : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros a b c. romega. Qed. -Lemma test_romega_3 : forall a b h hl hr ha hb, - 0 <= ha - hl <= 1 -> +Lemma test_romega_3 : forall a b h hl hr ha hb, + 0 <= ha - hl <= 1 -> -2 <= hl - hr <= 2 -> h =b+1 -> (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) -> (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) -> (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) -> - (-2 <= ha-hr <=2 -> hb = a + 1) -> + (-2 <= ha-hr <=2 -> hb = a + 1) -> 0 <= hb - h <= 1. Proof. intros. romega. Qed. -Lemma test_romega_3b : forall a b h hl hr ha hb, - 0 <= ha - hl <= 1 -> +Lemma test_romega_3b : forall a b h hl hr ha hb, + 0 <= ha - hl <= 1 -> -2 <= hl - hr <= 2 -> h =b+1 -> (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) -> (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) -> (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) -> - (-2 <= ha-hr <=2 -> hb = a + 1) -> + (-2 <= ha-hr <=2 -> hb = a + 1) -> 0 <= hb - h <= 1. Proof. intros a b h hl hr ha hb. @@ -88,18 +88,18 @@ romega. Qed. -Lemma test_romega_4 : forall hr ha, +Lemma test_romega_4 : forall hr ha, ha = 0 -> - (ha = 0 -> hr =0) -> + (ha = 0 -> hr =0) -> hr = 0. Proof. intros hr ha. romega. Qed. -Lemma test_romega_5 : forall hr ha, +Lemma test_romega_5 : forall hr ha, ha = 0 -> - (~ha = 0 \/ hr =0) -> + (~ha = 0 \/ hr =0) -> hr = 0. Proof. intros hr ha. @@ -118,14 +118,14 @@ intros z. romega. Qed. -Lemma test_romega_7 : forall z, +Lemma test_romega_7 : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. romega. Qed. -Lemma test_romega_7b : forall z, +Lemma test_romega_7b : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -- cgit v1.2.3