Library Exercise_4_5_1_16


Require Import Utf8.
Require Import Arith.
Require Import Category PreOrderCategory Product Orders NatOrders.
Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.5.1.16

Problem

Consider the preorder (, divides), discussed in Exercise 4.5.1.4, where e.g. 5 15 but 5 6.
(a) What is the product of 9 and 12 in this category?
(b) Is there a standard name for products in this category?

  Local Infix "≤" := divides.
  Class is_gcd (n m gcd_value : ) :=
    {
      gcd_divides_first : divides gcd_value n;
      gcd_divides_second : divides gcd_value m;
      gcd_maximal : v,
                      divides v n
                      → divides v m
                      → divides v gcd_value
    }.

  Local Ltac t :=
    repeat (split
              || intro
              || eassumption
              || (progress destruct_head_hnf @ex)
              || omega
              || ( 0; solve [ t ])
              || ( 1; solve [ t ])
              || (eexists; solve [ t ])
              || (match goal with
                    | [ n : _ |- _ ] ⇒ ( n; solve [ t ])
                    | [ H : _ |- _ ] ⇒ apply H; solve [ t ]
                  end)
              || (solve [ progress (hnf in *; subst); t ])
              || (progress destruct_head_hnf @is_gcd)).

  Local Ltac t' :=
    match goal with
      | [ a : _, b : _ |- _ ] ⇒
        ( (a + b);
                rewrite mult_plus_distr_r;
                solve [ t
                      | apply f_equal2; eassumption ])
      | [ H : _ |- _ ] ⇒
        apply H;
          solve [ t
                | eexists (_ - _);
                  rewrite mult_minus_distr_r;
                  apply f_equal2;
                  eassumption ]
    end.

  Local Obligation Tactic :=
    t;
    try t'.

  Global Program Instance gcd_0_n n : is_gcd 0 n n | 0.
  Global Program Instance gcd_n_0 n : is_gcd n 0 n | 0.
  Global Program Instance gcd_1_n n : is_gcd 1 n 1 | 0.
  Global Program Instance gcd_n_1 n : is_gcd n 1 1 | 0.
  Global Program Instance gcd_n_n n : is_gcd n n n | 0.
  Global Program Instance gcd_n_m_flip
         g `(le m n) `(is_gcd n m g)
  : is_gcd m n g | 1.
  Global Program Instance gcd_n_m
         g `(le n m) `(is_gcd (m - n) n g)
  : is_gcd m n g | 1.
  Global Instance gcd_is_product n m g `(H : is_gcd n m g)
  : is_product (PreOrderCategory (R := divides) _) n m g.
   gcd_divides_first gcd_divides_second gcd_maximal;
    abstract (intros; simpl; apply ProofIrrelevance.proof_irrelevance).
  Defined.

  Local Ltac try_solve_gcd :=
    match goal with
      | _solve [ eauto with typeclass_instances | hnf; omega ]
      | [ |- is_gcd _ _ _ ] ⇒ apply gcd_n_m_flip; simpl; try_solve_gcd
      | [ |- is_gcd _ _ _ ] ⇒ apply gcd_n_m; simpl; try_solve_gcd
      | [ |- is_gcd _ _ _ ] ⇒ idtac
    end.

  Definition gcd_9_12 : { n | is_gcd 9 12 n }.
    eexists.
    try_solve_gcd.
  Defined.
  Eval hnf in (proj1_sig gcd_9_12).
End Exercise_4_5_1_16.