Library NatOrders


Require Import Utf8 Setoid.
Require Import Omega.
Require Import NPeano.
Require Import Classes.RelationClasses.
Require Export Compare_dec Arith.Euclid.
Require Export Orders OrderProduct OrderCoproduct.
Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.

Orders on the natural numbers

The order "less than or equal to"

Section nat_le_order.
  Local Obligation Tactic := Tactics.program_simpl; repeat (omega || compute || intro || split).

  Global Program Instance le_refl' : RelationClasses.Reflexive le.
  Global Program Instance le_trans' : RelationClasses.Transitive le.
  Global Program Instance le_pre_order' : RelationClasses.PreOrder le.
  Global Program Instance le_antisym' : RelationClasses.Antisymmetric _ _ le.
  Global Program Instance le_partial_order' : RelationClasses.PartialOrder _ le.
  Global Program Instance le_comp' : Comparable le.
  Global Program Instance le_linear_order' : LinearOrder le.
  Global Instance le_dec' : RelationDecidable le := le_dec.
End nat_le_order.

The order "divides"

Definition divides n m := p, m = (p × n)%nat.
Notation "( x | y )" := (divides x y) (at level 0) : nat_scope.

Create HintDb nat_orders discriminated.
Create HintDb nat_orders_simple discriminated.

Hint Rewrite mult_assoc plus_assoc mult_0_r plus_0_r : nat_orders_simple.
Hint Rewrite mult_assoc plus_assoc mult_0_r plus_0_r mult_plus_distr_l : nat_orders.

Section nat_le_div.
  Local Open Scope nat_scope.

  Local Ltac t := repeat ((abstract omega)
                            || (simpl in *; cbv beta iota zeta delta -[mult plus] in *; idtac)
                            || intro
                            || split
                            || split_and
                            || destruct_head_hnf @ex
                            || subst
                            || (progress autorewrite with nat_orders_simple; idtac)
                            || (eexists; eassumption)
                            || ( 0; solve [ t ])
                            || ( 1; solve [ t ])
                            || ( 2; solve [ t ])
                            || (esplit; solve [ eauto; t; eauto ])
                            || match goal with
                                 | [ H : _ |- _ ] ⇒ ( H; solve [ t ])
                                 | [ H : _ |- _ ] ⇒ solve [ inversion H ]
                                 | [ H : S ?x = S ?y |- _ ] ⇒ assert (x = y) by (abstract omega); clear H
                               end).
  Local Obligation Tactic :=
    Tactics.program_simpl; t.

  Local Ltac t2 :=
    repeat (t
              || (progress autorewrite with nat_orders in *; idtac)
              || (match goal with
                    | [ H : context[?x × S ?y] |- _ ] ⇒ (rewrite (mult_comm x (S y)) in H; simpl in H)
                    | [ |- context[?x × S ?y] ] ⇒ (rewrite (mult_comm x (S y)); simpl)
                    | [ H : context[?x + S ?y] |- _ ] ⇒ (rewrite (plus_comm x (S y)) in H; simpl in H)
                    | [ |- context[?x + S ?y] ] ⇒ (rewrite (plus_comm x (S y)); simpl)
                  end)).

  Global Program Instance divides_refl : RelationClasses.Reflexive divides.
  Global Program Instance divides_trans : RelationClasses.Transitive divides.
  Global Program Instance divides_pre_order : RelationClasses.PreOrder divides.
  Global Program Instance divides_antisym : RelationClasses.Antisymmetric _ _ divides.
  Next Obligation.
    match goal with
      | [ |- ?x = _ ] ⇒ destruct x; t
    end.
    match goal with
      | [ a : , b : , c : |- _ ] ⇒ (destruct a; t; try destruct a; t);
                                       (destruct b; t; try destruct b; t);
                                       (destruct c; t; try destruct c; t)
    end.
    match goal with
      | [ H : ?x = ?x + S ?y + ?z |- _ ] ⇒ destruct z; destruct y; t
    end.
  Qed.
  Global Program Instance divides_partial_order : RelationClasses.PartialOrder _ divides.
  Next Obligation.
    apply divides_antisym; t.
  Qed.
  Global Instance divides_dec : RelationDecidable divides.
  hnf.
  refine (fun x ymatch x, y with
                       | _, 0 ⇒ left (ex_intro _ 0 eq_refl)
                       | 0, S y'right (fun Hmatch H return False with
                                                      | ex_intro p H'_
                                                    end)
                       | S x', S y'match Euclid.modulo (S x') _ (S y') with
                                         | exist r Hmatch r as n
                                                              return
                                                              (( q : , S y' = q × S x' + n S x' > n)
                                                                {divides (S x') (S y')} + {¬divides (S x') (S y')})
                                                        with
                                                          | 0 ⇒ fun H'left _
                                                          | S r'fun H'right _
                                                        end H
                                       end
                     end);
    try abstract t2;
    abstract (
        intro;
        destruct_head_hnf @ex;
        split_and;
        match goal with
          | [ H : ?x = ?y, H' : ?x = ?z |- _ ] ⇒ let x' := fresh in
                                                  set (x' := x) in *;
                                                    clearbody x';
          subst x'
        end;
        match goal with
          | [ H : (?x × S ?x' = ?x0 × S ?x' + _)%nat |- _ ] ⇒
            assert (x < S x0) by (apply (Nat.mul_lt_mono_pos_r (S x')); simpl; omega);
          assert (x0 < x) by (apply (Nat.mul_lt_mono_pos_r (S x')); simpl; omega);
          omega
        end
      ).
  Defined.
End nat_le_div.