Require Import Arith Lia List Bool Setoid.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_tac gcd prime binomial sums bool_nat rel_iter.

From Undecidability.H10.ArithLibs
  Require Import luca.

From Undecidability.H10.Matija
  Require Import cipher.

From Undecidability.H10.Dio
  Require Import dio_logic dio_expo.

Set Implicit Arguments.

Set Default Proof Using "Type".

Local Infix "≲" := binary_le (at level 70, no associativity).
Local Notation power := (mscal mult 1).
Local Notation "∑" := (msum plus 0).
Local Infix "⇣" := nat_meet (at level 40, left associativity).
Local Infix "⇡" := nat_join (at level 50, left associativity).


Section dio_fun_binomial.

  Let plus_cancel_l : forall a b c, a + b = a + c -> b = c.
  Proof. intros; lia. Qed.

  Hint Resolve Nat.mul_add_distr_r : core.


  Let is_binomial_eq b n k :
         b = binomial n k
     <-> exists q, q = power (1+n) 2
                /\ is_digit (power n (1+q)) q k b.
  Proof.
    split.
    + intros ?; subst.
      set (q := power (1+n) 2).
      assert (Hq : q <> 0).
      { unfold q; generalize (@power_ge_1 (S n) 2); intros; simpl; lia. }
      set (c := power n (1+q)).
      exists q; split; auto; split.
      * apply binomial_lt_power.
      * fold c.
        destruct (le_lt_dec k n) as [ Hk | Hk ].
        - exists (∑ (n-k) (fun i => binomial n (S k+i) * power i q)),
                 (∑ k (fun i => binomial n i * power i q)); split; auto.
          2: { apply sum_power_lt; auto; intros; apply binomial_lt_power. }
          rewrite Nat.mul_add_distr_r, <- mult_assoc, <- power_S.
          rewrite <- sum_0n_distr_r with (1 := Nat_plus_monoid) (3 := Nat_mult_monoid); auto.
          rewrite <- plus_assoc, (plus_comm _ (∑ _ _)).
          rewrite <- msum_plus1 with (f := fun i => binomial n i * power i q); auto.
          rewrite plus_comm.
          unfold c.
          rewrite Newton_nat_S.
          replace (S n) with (S k + (n-k)) by lia.
          rewrite msum_plus; auto; f_equal; apply msum_ext.
          intros; rewrite power_plus; ring.
        - exists 0, c.
          rewrite binomial_gt; auto.
          rewrite Nat.mul_0_l; split; auto.
          unfold c.
          apply lt_le_trans with (power (S n) q).
          ++ rewrite Newton_nat_S.
             apply sum_power_lt; auto.
             intros; apply binomial_lt_power.
          ++ apply power_mono; lia.
    + intros (q & H1 & H3).
      assert (Hq : q <> 0).
      { rewrite H1; generalize (@power_ge_1 (S n) 2); intros; simpl; lia. }
      rewrite Newton_nat_S in H3.
      apply is_digit_fun with (1 := H3).
      destruct (le_lt_dec k n) as [ Hk | Hk ].
      * red; split.
        - subst; apply binomial_lt_power.
        - exists (∑ (n-k) (fun i => binomial n (S k+i) * power i q)),
                 (∑ k (fun i => binomial n i * power i q)); split.
          2: { apply sum_power_lt; auto; intros; subst; apply binomial_lt_power. }
          rewrite Nat.mul_add_distr_r, <- mult_assoc, <- power_S.
          rewrite <- sum_0n_distr_r with (1 := Nat_plus_monoid) (3 := Nat_mult_monoid); auto.
          rewrite <- plus_assoc, (plus_comm _ (∑ _ _)).
          rewrite <- msum_plus1 with (f := fun i => binomial n i * power i q); auto.
          rewrite plus_comm.
          replace (S n) with (S k + (n-k)) by lia.
          rewrite msum_plus; auto; f_equal.
          apply msum_ext.
          intros; rewrite power_plus; ring.
      * rewrite binomial_gt; auto.
        rewrite <- Newton_nat_S.
        split; try lia.
        exists 0, (power n (1+q)); split; auto.
        apply lt_le_trans with (power (S n) q).
        - rewrite Newton_nat_S.
          apply sum_power_lt; auto.
          subst; intros; apply binomial_lt_power.
        - apply power_mono; lia.
  Qed.

  Lemma dio_fun_binomial n k : 𝔻F n -> 𝔻F k -> 𝔻F (fun ν => binomial (n ν) (k ν)).
  Proof.
    dio by lemma (fun ν => is_binomial_eq (ν 0) (n ν⭳) (k ν⭳)).
  Defined.

End dio_fun_binomial.

#[export] Hint Resolve dio_fun_binomial : dio_fun_db.

Local Fact dio_fun_binomial_example : 𝔻F (fun ν => binomial (ν 0) (ν 1)).
Proof. dio auto. Defined.



Theorem binary_le_binomial n m : n ≲ m <-> rem (binomial m n) 2 = 1.
Proof.
  split.
  + induction 1 as [ n | n m H1 H2 IH2 ].
    * rewrite binomial_n0, rem_lt; lia.
    * rewrite lucas_lemma with (1 := prime_2) (2 := div_rem_spec1 m 2) (4 := div_rem_spec1 n 2);
        try (apply div_rem_spec2; lia).
      rewrite mult_comm, <- rem_mult_rem, IH2, Nat.mul_1_r.
      revert H1.
      generalize (rem_2_is_0_or_1 m) (rem_2_is_0_or_1 n).
      intros [ G1 | G1 ] [ G2 | G2 ]; rewrite G1, G2; intros; try lia.
      ++ rewrite binomial_n0, rem_lt; lia.
      ++ rewrite binomial_n0, rem_lt; lia.
      ++ rewrite binomial_n1, rem_lt; lia.
  + induction on n m as IH with measure m.
    destruct (eq_nat_dec m 0) as [ Hm | Hm ].
    * destruct n; try (intros; constructor; fail).
      subst; rewrite binomial_gt, rem_lt; lia.
    * generalize (div_rem_spec1 m 2) (div_rem_spec1 n 2); intros H1 H2.
      rewrite lucas_lemma with (1 := prime_2) (2 := H1) (4 := H2); auto;
        try (apply div_rem_spec2; lia).
      rewrite rem_2_mult; intros (H3 & H4).
      apply IH in H3; try lia.
      constructor 2; auto.
      revert H4.
      generalize (rem_2_is_0_or_1 m) (rem_2_is_0_or_1 n).
      intros [ G1 | G1 ] [ G2 | G2 ]; rewrite G1, G2; intros; try lia.
      rewrite binomial_gt, rem_lt in H4; lia.
Qed.

Theorem dio_rel_binary_le x y : 𝔻F x -> 𝔻F y -> 𝔻R (fun v => x v ≲ y v).
Proof.
  dio by lemma (fun v => binary_le_binomial (x v) (y v)).
Defined.

#[export] Hint Resolve dio_rel_binary_le : dio_rel_db.

Theorem dio_fun_nat_meet a b : 𝔻F a -> 𝔻F b -> 𝔻F (fun ν => a ν ⇣ b ν).
Proof.
  dio by lemma (fun v => nat_meet_dio (v 0) (a v⭳) (b v⭳)).
Defined.

#[export] Hint Resolve dio_fun_nat_meet : dio_fun_db.