Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ROmega0.v Sprache: Coq

Original von: Coq^©

Require Import ZArith Lia.
Open Scope Z_scope.

(* Pierre L: examples gathered while debugging romega. *)
(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated.
   The tests in this file remain but now call the `lia` tactic. *)

Lemma test_lia_0 :
forall m m',
  0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
Proof.
intros.
lia.
Qed.

Lemma test_lia_0b :
forall m m',
  0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
Proof.
intros m m'.
lia.
Qed.

Lemma test_lia_1 :
forall (z z1 z2 : Z),
    z2 <= z1 ->
    z1 <= z2 ->
    z1 >= 0 ->
    z2 >= 0 ->
    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
    z >= 0.
Proof.
intros.
lia.
Qed.

Lemma test_lia_1b :
forall (z z1 z2 : Z),
    z2 <= z1 ->
    z1 <= z2 ->
    z1 >= 0 ->
    z2 >= 0 ->
    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
    z >= 0.
Proof.
intros z z1 z2.
lia.
Qed.

Lemma test_lia_2 : forall a b c:Z,
0<=a-b<=1 -> b-c<=2 -> a-c<=3.
Proof.
intros.
lia.
Qed.

Lemma test_lia_2b : forall a b c:Z,
0<=a-b<=1 -> b-c<=2 -> a-c<=3.
Proof.
intros a b c.
lia.
Qed.

Lemma test_lia_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) ->
0 <= hb - h <= 1.
Proof.
intros.
lia.
Qed.

Lemma test_lia_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) ->
0 <= hb - h <= 1.
Proof.
intros a b h hl hr ha hb.
lia.
Qed.

Lemma test_lia_4 : forall hr ha,
ha = 0 ->
(ha = 0 -> hr =0) ->
hr = 0.
Proof.
intros hr ha.
lia.
Qed.

Lemma test_lia_5 : forall hr ha,
ha = 0 ->
(~ha = 0 \/ hr =0) ->
hr = 0.
Proof.
intros hr ha.
lia.
Qed.

Lemma test_lia_6 : forall z, z>=0 -> 0>z+2 -> False.
Proof.
intros.
lia.
Qed.

Lemma test_lia_6b : forall z, z>=0 -> 0>z+2 -> False.
Proof.
intros z.
lia.
Qed.

Lemma test_lia_7 : forall z,
  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
Proof.
intros.
lia.
Qed.

Lemma test_lia_7b : forall z,
  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
Proof.
intros.
lia.
Qed.

(* Magaud BZ#240 *)

Lemma test_lia_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
Proof.
intros.
lia.
Qed.

Lemma test_lia_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
Proof.
intros x y.
lia.
Qed.

(* Besson BZ#1298 *)

Lemma test_lia9 : forall z z':Z, z<>z' -> z'=z -> False.
Proof.
intros.
lia.
Qed.

(* Letouzey, May 2017 *)

Lemma test_lia10 : forall x a a' b b',
a' <= b ->
a <= b' ->
b < b' ->
a < a' ->
a <= x < b' <-> a <= x < b \/ a' <= x < b'.
Proof.
intros.
lia.
Qed.

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.