(* Ugly tacty to resolve sign condition for Z *)
Require Import Arith.
Require Import List.
Require Export NatGroundTac.


Theorem mult_lt_compat_l: forall n m p : nat, n < m -> 0 < p -> p * n < p * m.
(* Goal: forall (n m p : nat) (_ : lt n m) (_ : lt O p), lt (Init.Nat.mul p n) (Init.Nat.mul p m) *)
intros n m p H H1; repeat rewrite (mult_comm p); apply mult_lt_compat_r; auto.
Qed.

Theorem mult_ge_compat_l: forall n m p : nat, n >= m -> p * n >= p * m.
(* Goal: forall (n m p : nat) (_ : ge n m), ge (Init.Nat.mul p n) (Init.Nat.mul p m) *)
intros n m p H; auto with arith.
Qed.

Theorem mult_gt_compat_l: forall n m p : nat, n > m -> p > 0 -> p * n > p * m.
(* Goal: forall (n m p : nat) (_ : gt n m) (_ : gt p O), gt (Init.Nat.mul p n) (Init.Nat.mul p m) *)
intros n m p H H1; red; apply mult_lt_compat_l; auto.
Qed.

Theorem mult_lt_compat_rev_l1: forall n m p : nat, p * n < p * m -> 0 < p.
(* Goal: forall (n m p : nat) (_ : gt (Init.Nat.mul p n) (Init.Nat.mul p m)), gt p O *)
intros n m p; case p; auto with arith.
Qed.

Theorem mult_lt_compat_rev_l2: forall n m p : nat, p * n < p * m -> n < m.
(* Goal: forall (n m p : nat) (_ : lt (Init.Nat.mul p n) (Init.Nat.mul p m)), lt n m *)
intros n m p H; case (le_or_lt m n); auto with arith; intros H1.
(* Goal: lt n m *)
absurd (p * n < p * m); auto with arith.
(* Goal: not (lt (Init.Nat.mul p n) (Init.Nat.mul p m)) *)
apply le_not_lt; apply mult_le_compat_l; auto.
Qed.


Theorem mult_gt_compat_rev_l1: forall n m p : nat, p * n > p * m -> p > 0.
(* Goal: forall (n m p : nat) (_ : gt (Init.Nat.mul p n) (Init.Nat.mul p m)), gt p O *)
intros n m p; case p; auto with arith.
Qed.

Theorem mult_gt_compat_rev_l2: forall n m p : nat, p * n > p * m -> n > m.
(* Goal: forall (n m p : nat) (_ : gt (Init.Nat.mul p n) (Init.Nat.mul p m)), gt n m *)
intros n m p H; case (le_or_lt n m); auto with arith; intros H1.
(* Goal: gt n m *)
absurd (p * n > p * m); auto with arith.
Qed.

Theorem mult_le_compat_rev_l: forall n m p : nat, p * n <= p * m -> 0 < p -> n <= m.
(* Goal: forall (n m p : nat) (_ : le (Init.Nat.mul p n) (Init.Nat.mul p m)) (_ : lt O p), le n m *)
intros n m p H H1; case (le_or_lt n m); auto with arith; intros H2; absurd (p * n <= p * m); auto with arith.
(* Goal: not (le (Init.Nat.mul p n) (Init.Nat.mul p m)) *)
apply lt_not_le; apply mult_lt_compat_l; auto.
Qed.

Theorem mult_ge_compat_rev_l: forall n m p : nat, p * n >= p * m -> 0 < p -> n >= m.
(* Goal: forall (n m p : nat) (_ : ge (Init.Nat.mul p n) (Init.Nat.mul p m)) (_ : lt O p), ge n m *)
intros n m p H H1; case (le_or_lt m n); auto with arith; intros H2; absurd (p * n >= p * m); auto with arith.
(* Goal: not (le (Init.Nat.mul p n) (Init.Nat.mul p m)) *)
unfold ge; apply lt_not_le; apply mult_lt_compat_l; auto.
Qed.

Theorem lt_mult_0: forall a b, 0 < a -> 0 < b -> 0 < a * b.
(* Goal: forall (a b : nat) (_ : lt O a) (_ : lt O b), lt O (Init.Nat.mul a b) *)
intros a b; case a ; case b; simpl; auto with arith.
(* Goal: forall (n : nat) (_ : lt O (S n)) (_ : lt O O), lt O (Init.Nat.mul n O) *)
intros n H1 H2; absurd (0 < 0); auto with arith.
Qed.

Theorem gt_mult_0: forall a b, a > 0 -> b > 0 -> a * b > 0.
intros a b H1 H2; red; apply  lt_mult_0; auto with arith.
Qed.


Theorem lt_mult_rev_0_l: forall a b, 0 < a * b ->  0 < a .
(* Goal: forall (a b : nat) (_ : gt (Init.Nat.mul a b) O), gt a O *)
intros a b; case a; simpl; auto with arith.
Qed.

Theorem lt_mult_rev_0_r: forall a b, 0 < a * b ->  0 < b .
(* Goal: forall (a b : nat) (_ : gt (Init.Nat.mul a b) O), gt b O *)
intros a b; case b; simpl; auto with arith.
(* Goal: forall _ : gt (Init.Nat.mul a O) O, gt O O *)
rewrite mult_0_r; auto with arith.
Qed.

Theorem gt_mult_rev_0_l: forall a b, a * b > 0 ->  a > 0.
(* Goal: forall (a b : nat) (_ : gt (Init.Nat.mul a b) O), gt a O *)
intros a b; case a; simpl; auto with arith.
Qed.

Theorem gt_mult_rev_0_r: forall a b, a * b > 0  ->  b > 0 .
(* Goal: forall (a b : nat) (_ : gt (Init.Nat.mul a b) O), gt b O *)
intros a b; case b; simpl; auto with arith.
(* Goal: forall _ : gt (Init.Nat.mul a O) O, gt O O *)
rewrite mult_0_r; auto with arith.
Qed.

Theorem le_0_eq_0: forall n, n <= 0 -> n = 0.
(* Goal: forall (n : nat) (_ : le n O), @eq nat n O *)
intros n; case n; auto with arith.
Qed.

Ltac nsign_tac :=
 repeat (apply mult_le_compat_l || apply mult_lt_compat_l ||
              apply mult_ge_compat_l || apply mult_gt_compat_l ||
              apply lt_mult_0 || apply gt_mult_0); auto with arith.

Ltac hyp_nsign_tac H :=
  match type of H with
   0 <= _ => clear H
| ?X1 <= 0 => generalize (le_0_eq_0 _ H); clear H; intros H; subst X1
|  ?X1 * _ <= ?X1 * _ => 
             let s1 := fresh "NS" in
                   (assert (s1: 0 < X1); [nsign_tac; fail |
                   generalize (mult_le_compat_rev_l _ _ _ H s1);
                   clear H s1; intros H])
|   0  < ?X1 * _ => 
              let s1 := fresh "NS" in
                   (generalize (lt_mult_rev_0_l _ _ H);
                    generalize (lt_mult_rev_0_r _ _ H); clear H;
                    intros H s1; hyp_nsign_tac s1; hyp_nsign_tac H)
|  ?X1 < 0 => absurd (~ (X1 < 0)); auto with arith
| ?X1 * _  < ?X1 * _ => 
              let s1 := fresh "NS" in
                   (generalize (mult_lt_compat_rev_l1 _ _ _ H);
                    generalize (mult_lt_compat_rev_l2 _ _ _ H); clear H;
                    intros H s1; hyp_nsign_tac s1; hyp_nsign_tac H)
|  ?X1 >= 0 => clear H
| 0 >= ?X1  => generalize (le_0_eq_0 _ H); clear H; intros H; subst X1
|  ?X1 * _ >= ?X1 * _ => 
             let s1 := fresh "NS" in
                   (assert (s1: 0 < X1); [nsign_tac; fail |
                   generalize (mult_ge_compat_rev_l _ _ _ H s1);
                   clear H s1; intros H])
|  ?X1 * _ > 0 => 
              let s1 := fresh "NS" in
                   (generalize (gt_mult_rev_0_l _ _ H);
                    generalize (gt_mult_rev_0_r _ _ H); clear H;
                    intros H s1; hyp_nsign_tac s1; hyp_nsign_tac H)
|  0 > ?X1 => absurd (~ (0 > X1)); auto with arith
| ?X1 * _  > ?X1 * _ => 
              let s1 := fresh "NS" in
                   (generalize (mult_gt_compat_rev_l1 _ _ _ H);
                    generalize (mult_gt_compat_rev_l2 _ _ _ H); clear H;
                    intros H s1; hyp_nsign_tac s1; hyp_nsign_tac H)
  |  _ => (let u := type of H in (clear H; assert (H: u); [auto with arith; fail | clear H]) || idtac)
              
   end.

(* Test *)
Section Test.

Let hyp_test : forall a b c d e, 
  0 <= a -> 0 < a -> a * b <= a * c  -> b * a <= b * c -> d <= 0 -> e < 0 -> d = 0.
(* Goal: forall (a b c d e : nat) (_ : ge a O) (_ : gt a O) (_ : gt (Init.Nat.mul a b) (Init.Nat.mul a c)) (_ : ge (Init.Nat.mul b a) (Init.Nat.mul b c)) (_ : ge O d) (_ : gt O e), @eq nat d O *)
intros a b c d e H H1 H2 H3 H4 H5.
(* H should disappear *)
(* Goal: @eq nat d O *)
hyp_nsign_tac H.
(* a in H2 should disappear *)
(* Goal: @eq nat d O *)
hyp_nsign_tac H2.
(* H3 unchanged *)
(* Goal: @eq nat d O *)
try hyp_nsign_tac H3.
(* d should disappear *)
(* Goal: @eq nat d O *)
hyp_nsign_tac H4.
(* Prove it *)
(* Goal: @eq nat O O *)
hyp_nsign_tac H5.
Qed.


Let hyp_test1 : forall a b c d e, 
  a >= 0 -> a > 0 -> a * b > a * c  -> b * a >= b * c -> 0 >= d -> 0 > e -> d = 0.
(* Goal: forall (a b c d e : nat) (_ : ge a O) (_ : gt a O) (_ : gt (Init.Nat.mul a b) (Init.Nat.mul a c)) (_ : ge (Init.Nat.mul b a) (Init.Nat.mul b c)) (_ : ge O d) (_ : gt O e), @eq nat d O *)
intros a b c d e H H1 H2 H3 H4 H5.
(* H should disappear *)
(* Goal: @eq nat d O *)
hyp_nsign_tac H.
(* a in H2 should disappear *)
(* Goal: @eq nat d O *)
hyp_nsign_tac H2.
(* H3 unchanged *)
(* Goal: @eq nat d O *)
try hyp_nsign_tac H3.
(* d should disappear *)
(* Goal: @eq nat d O *)
hyp_nsign_tac H4.
(* Prove it *)
(* Goal: @eq nat O O *)
hyp_nsign_tac H5.
Qed.

End Test.
