Require Import Lia Factorial.
Require Extraction.

Definition Q : Type := nat * nat.

Definition is_q (q : Q) := Nat.eqb (snd q) 0 = false.

Definition binom (n k: nat): Q :=
  if Nat.leb k n then (fact n,fact k * fact (n - k)) else (0,1).

Lemma prod_pos : forall n m:nat, 0 < n -> 0 < m -> Nat.eqb (n * m) 0 = false.
Proof.
  intros.
  apply PeanoNat.Nat.eqb_neq.
  cut (n * m > 0).
  lia.
  apply PeanoNat.Nat.mul_pos_pos; trivial.
Defined.

Lemma facprod_pos : forall n m:nat, Nat.eqb (fact n * fact m) 0 = false.
Proof.
intros.
apply prod_pos; apply lt_O_fact;trivial.
Defined.


Lemma binom_q : forall n k:nat, is_q (binom n k).
Proof.
unfold binom, is_q; intros.
case (Nat.leb k n); simpl;trivial.
apply facprod_pos.
Defined.


Definition n2q (n : nat) : Q := (n,1).

Lemma n_q : forall n:nat, is_q (n2q n).
Proof.
unfold is_q, n2q. simpl. trivial.
Defined.


Definition eq_q (x y : Q) : Prop :=
  snd y * fst x = snd x * fst y.

Lemma eq_q_sym : forall x y: Q, eq_q x y -> eq_q y x.
Proof.
unfold eq_q, is_q;simpl.
intros x y.
generalize (fst x) (snd x) (fst y) (snd y).
intros.
lia.
Defined.


Lemma eq_q_trans : forall x y z : Q, is_q y -> eq_q x y -> eq_q y z ->  eq_q x z.
Proof.
unfold eq_q, is_q;simpl.
intros x y z.
generalize (fst x), (snd x), (fst y), (snd y), (fst z), (snd z).
intros.
cut (0 < n2).
intro.
cut (n4 * n * n2 = n0 * n3 * n2).
intro.
apply PeanoNat.Nat.mul_cancel_r in H3.
trivial.
lia.
transitivity (n4 * (n2 * n)).
lia.
rewrite H0.
transitivity ((n4 * n1) * n0).
lia.
rewrite H1.
lia.
apply EqNat.beq_nat_false in H.
lia.
Defined.


Lemma eq_nq : forall n m:nat, n = m <-> eq_q (n2q n) (n2q m).
Proof.
unfold eq_q, n2q; intros; simpl; lia.
Defined.


Definition plus_q (x y : Q) : Q :=
  match x, y with
  | (n1,d1),(n2,d2) => (n1*d2+n2*d1,d1*d2)
end.

Lemma plus_is_q : forall x y:Q, is_q x -> is_q y -> is_q (plus_q x y).
Proof.
unfold is_q, plus_q.
intros x y.
case x;case y;simpl; intros.
apply EqNat.beq_nat_false in H.
apply EqNat.beq_nat_false in H0.
apply prod_pos; lia.
Defined.


Lemma plus_nq : forall n m:nat, eq_q (n2q (n+m)) (plus_q (n2q n) (n2q m)).
Proof.
unfold plus_q, n2q, eq_q;intros; simpl; lia.
Defined.


Lemma plus_cong : forall x y x' y' : Q, eq_q x x' -> eq_q y y' -> 
  eq_q (plus_q x y) (plus_q x' y').
Proof.
  unfold plus_q, eq_q; case x,y,x',y'; simpl; intros.
  transitivity ((n4 * n) * n6 * n2 + ((n6 * n1) * n4 * n0)).
  lia.
  rewrite H , H0.
  lia.
Defined.


Lemma plus_num : forall n k m:nat, eq_q (n+k,m) (plus_q (n,m) (k,m)).
Proof.
unfold plus_q, eq_q; simpl; intros.
lia.
Defined.


Lemma fivea : forall n k: nat, 
  eq_q (binom (S n) (S k)) (plus_q (binom n k) (binom n (S k))).
Proof.
  intros n k.
  unfold binom.
  replace (Nat.leb (S k) (S n)) with (Nat.leb k n).
  case_eq (Nat.leb k n); case_eq (Nat.leb (S k) n); intros.
  - clear H0.
    apply Compare_dec.leb_complete in H.
   replace (S n - S k) with (n - k).
  replace (fact (S n)) with ((fact n) * (k+1) + (fact n) * (n-k)).
  apply eq_q_trans with (y := plus_q ((fact n) * (k+1) ,fact (S k) * fact (n - k)) 
      ((fact n) * (n-k),fact (S k) * fact (n - k))).
  apply plus_is_q; unfold is_q; unfold snd; apply facprod_pos.
  apply plus_num.
  apply plus_cong; unfold eq_q; simpl; try lia.
  replace (fact (n - k)) with ((n-k) * fact (n - S k)).
  lia.
  replace (n - S k) with ((n - k) -1).
  case_eq (n - k).
  intro.
  lia.
  intros.
  simpl.
  replace (n0 - 0) with n0; lia.
  lia.
  simpl.
  generalize (fact n); intro.
  cut (k <= n).
  intro.
  clear H.
  rewrite Coq.Arith.Mult.mult_minus_distr_l .
  rewrite Coq.Arith.Mult.mult_plus_distr_l .
  cut (n0 * k <= n0 * n).
  replace (n * n0) with (n0 * n);try lia.
  apply Coq.Arith.Mult.mult_le_compat_l; trivial.
  lia.
  lia.
  - apply Compare_dec.leb_complete_conv in H.
  apply Compare_dec.leb_complete in H0.
  cut (k = n); intros; try lia.
  rewrite H1.
  unfold eq_q; simpl.
  lia.
  -  apply Compare_dec.leb_complete_conv in H0.
  apply Compare_dec.leb_complete in H.
  lia.
 - unfold eq_q; simpl; trivial.
 - simpl; trivial.
Defined.


Lemma fiveba : forall n k: nat, { m:nat | eq_q (n2q m) (binom n k) }.
Proof.
  induction n.
  intro k; case k; unfold binom;simpl.
  exists 1.
  unfold eq_q, n2q; simpl; trivial.
  intro.
  exists 0.
  unfold eq_q, n2q; simpl;trivial.
  intro k.
  case k.
  exists 1.
  unfold eq_q, n2q; simpl;lia.
  intro.
  elim IHn with (k := n0).
  elim IHn with (k := S n0).
  intros.
  exists (x0 + x).
  apply eq_q_trans with (y :=  plus_q (binom n n0) (binom n (S n0))).
  apply plus_is_q; apply binom_q.
  apply eq_q_trans with (y := plus_q (n2q x0) (n2q x)).
   apply plus_is_q; apply n_q.
  apply plus_nq.
  apply plus_cong; assumption.
  apply eq_q_sym.
  apply fivea.
Defined.


Lemma fiveb : forall n k: nat, { m:nat | m * (snd (binom n k)) = fst (binom n k)}.
Proof.
 intros.
  cut (forall n k: nat, { m:nat | eq_q (n2q m) (binom n k) }).
  intro.
  elim H with (n := n)(k := k).
  intros.
  exists x.
  unfold eq_q, n2q in p; simpl in p.
  lia.
  apply fiveba.
Defined.

Lemma fiveb' : forall n k: nat, let b := binom n k in let f := fst b in let s := snd b in 
  { m : nat | Nat.div f s = m /\ Nat.modulo f s = 0 }.
Proof.
intros n k.
simpl.
exists (Nat.div (fst (binom n k)) (snd (binom n k))).
split;trivial.
cut (forall n k: nat, { m:nat | m * (snd (binom n k)) = fst (binom n k)}); intros.
elim H with (n := n) (k := k).
intros.
rewrite <- p.
cut (snd (binom n k) <> 0).
generalize (snd (binom n k)).
intro.
apply PeanoNat.Nat.mod_mul.
cut (is_q (binom n k)).
generalize (binom n k).
intro q.
case q.
unfold is_q.
simpl.
intros.
apply EqNat.beq_nat_false in H0; trivial.
apply binom_q.
apply fiveb.
Defined.

Extraction Language Haskell.

Recursive Extraction fiveb'.