(* This file contains examples of non trivial statements solved by Omega *)

Require Arith.
Require ZArith.
Require Omega.

(*
Set Omega Time.
Set Omega System.
Set Omega Action.
*)


Theorem test1:
(z,y,m,N:Z)
  `0 < z` -> `0 < y` -> `0 < m` -> 
   `0 < N` -> 
   `z < y` /\ `z > N` /\ `y=m` /\ ~`y>m` ->
   `2*z < y` ->
     `2*z < y`
      /\ `2*z > N` /\ `y = m` \/ `y < m`.

Intros; Omega.
Save.

Theorem test2:
 (x,y,t:Z)(x,y,t:Z)~(`3*x+(2*y+5) = 0`/\`t >= 3`/\`3*x+(2*y+(t+6)) <= 2`).

Intros; Omega.
Save.

Theorem test3: (x,y:Z)~( `0<x` /\ `0<y` /\ `y<=x` /\ `x-y>=x`).
Intros; Omega.
Save.

(* Transitivite du lt lexicographique sur les paires *)
Theorem test4:
(y,y0,y1,y2,y3,y4:Z)
   `y < y1`\/`y = y1`/\`y0 < y2`
     ->`y1 < y3`\/`y1 = y3`/\`y2 < y4`->`y < y3`\/`y = y3`/\`y0 < y4`.

Intros; Omega.
Save.

(* Petit test de division par une constante *)

Theorem div_by_c: (x,y:Z)`x*2+(y*2+1) <> 0`.
Intros; Omega.
Save.

(* Cet exemple ne passe pas avec ARITH de Boulton (Bledsoe-Shostak) *)

Theorem fail_arith: (m,n:Z)~`1+2*m <= 2*n <= 1+2*m`.
Intros; Omega.
Save.

(* Ces exemples sont extraits de preuves Unity. On essaie d'avoir le 
 * minimum de traduction. Ces exemples montre la necessite de gerer 
 * efficacement ~ _ = _ *)

Parameter variable:Set.
Parameter y, z: variable.

Theorem test5:
  (m,n,N : nat)
  (s : variable->nat)
  (Depart : ((lt (s y) (s z))/\(gt (s z) N)/\(s y)=m/\(s z)=n)
            /\~((s y)=m/\(lt (s z) n)))
  (Hltb : (lt (s y) (mult (2) (s z))))

  ((lt (s y) N)/\(gt N N)/\(s y)=m/\N=n\/(s y)=m/\(lt N n)).

Intros; Omega.
Save.

Theorem test6:
  (m,n,N : nat)
  (s : variable->nat)
  (Depart : ((lt (s y) (s z))/\(gt (s z) N)/\(s y)=m/\(s z)=n)
           /\~((s y)=m/\(lt (s z) n)))
  (Hltb : (le (mult (2) (s z)) (s y)))
 
  ((lt (s y) (mult (2) (s z)))
   /\(gt (mult (2) (s z)) N)/\(s y)=m/\(mult (2) (s z))=n
   \/(s y)=m/\(lt (mult (2) (s z)) n)).

Intros; Omega.
Save.

Theorem test7:
  (m,n,N : nat)
  (s : variable->nat)
  (Depart : ((lt (s y) (s z))/\(gt (s z) N)/\(s y)=m/\(s z)=n)
           /\~((s y)=m/\(lt (s z) n)))
  (Hltb : (lt (s y) (s z)))

  ((lt (s y) (s z))/\(gt (s z) N)/\(s y)=m/\(s z)=n
   \/(s y)=m/\(lt (s z) n)).

Intros; Omega.
Save.

Theorem test8:
  (m,n,N : nat)
  (s : variable->nat)
  (Depart : ((lt (s y) (s z))/\(gt (s z) N)/\(s y)=m/\(s z)=n)
           /\~((s y)=m/\(lt (s z) n)))
  (Hltb : (le (s z) (s y)))

  ((lt (minus (s y) (s z)) (s z))
   /\(gt (s z) N)/\(minus (s y) (s z))=m/\(s z)=n
   \/(minus (s y) (s z))=m/\(lt (s z) n)).

Intros; Omega.
Save.







