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'.