# 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 (, , 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
|| 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 ])

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.