(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(** ** Object-level encoding of bounded universal quantification III *)

Require Import Arith Nat Omega List Bool.

Require Import utils_tac utils_list sums bounded_quantification.
Require Import cipher.
Require Import dio_logic dio_cipher dio_elem.

Set Implicit Arguments.

Local Notation power := (mscal mult 1).
Local Notation "âˆ‘" := (msum plus 0).

(** We show the elimination of bounded universal quantification. The proof is
    based on the paper 

       "A new technique for obtaining diophantine representations via elimination
        of bounded universal quantifiers" by Matiyasevich 

    with two noticable differences

    a) we use r = 2^(4*q) instead of r = 2^(2*q)
       2*q could work but I think the proof implied by the paper (it is not
       given) that cc = aa * bb is simulated does not work well because
       masked digits are can be of the form f i * g j + f j * g i
       and f _ < 2^q,  g _ < 2^q implies f _ * g _ < 2^(2*q) which is
       good but *does not* imply  f _ * g _ + f _ * g _ < 2^(2*q) !!
       The argument could still work though it is going to be much
       more complicated to establish formally, so I raised 2*q to 4*q
       to solve straightforwardly the overflow problem of masked digits
       Anyway, this 2*q value was arbitrary so it only impacts the 
       proof in minor ways

    b) The arguments outlined between (26) and (31) are flawed I think
       One should first split the k_i's in 0 <= k_2 < .... < k_d <= 2^l+1 < .... < k_{m+1}
       to do the computation. The upper k_i's are masked out and then you can show
       that d must be m+1 with the other constraints.

*)

Section df_mconj.

  Fixpoint df_mconj k f :=
    match k with 
      | 0   => df_true
      | S k => df_conj (f 0) (df_mconj k (fun i => f (S i)))
    end.

  Fact df_mconj_size k f : df_size (df_mconj k f) = 3+k+âˆ‘ k (fun i => df_size (f i)).
  Proof.
    revert f; induction k as [ | k IHk ]; intros f; simpl; auto.
    rewrite IHk; ring.
  Qed.

  Fact df_mconj_spec k f Î½ : df_pred (df_mconj k f) Î½ <-> forall i, i < k -> df_pred (f i) Î½.
  Proof.
    revert f Î½; induction k as [ | k IHk ]; intros f phi; simpl.
    + split; auto; intros; omega.
    + rewrite IHk; split.
      * intros (? & H2) [ | i ] ?; auto; apply H2; omega.
      * intros H; split; intros; apply H; omega.
  Qed.

  Lemma dio_rel_mconj k (P : nat -> (nat -> nat) -> Prop) :
         (forall i, i < k -> dio_rel (P i))
      -> dio_rel (fun Î½ => forall i, i < k -> P i Î½).
  Proof.
    intros H.
    apply fmap_reifier_t_default with (1 := df_true) in H.
    destruct H as (f & Hf).
    exists (df_mconj k f).
    intros v; rewrite df_mconj_spec; split;
      intros E i Hi; generalize (E _ Hi); apply Hf; trivial. 
  Defined.

End df_mconj.

Section dio_bounded_fall.

  Section dio_bounded_elem.

    Variable (k : nat).

    (* Ï‰ : nat -> nat
       for i < k, Ï‰ represents the cipher of the corresponding variable x_i
       for i = k, Ï‰ represents the cipher of <0,...,l-1> 
       for i = k+1, Ï‰ contains the value q 
       for i = k+2, Ï‰ contains the value l   
       for k+2 < i, Ï‰ represents the value of parameter i-k-2>0  *)

    Notation iq := (k+1).  (* The index of q in Ï‰ *)
    Notation il := (k+2).  (* The index of l in Ï‰ *)

    Let dc_Code (c : dio_constraint) Ï‰ :=
      match c with
       | (u, dee_nat n)           => Const (Ï‰ il) (Ï‰ iq) n (Ï‰ u)
       | (u, dee_var v)           => Ï‰ u = Ï‰ v
       | (u, dee_par 0)           => Ï‰ u = Ï‰ k
       | (u, dee_par (S p))       => Const (Ï‰ il) (Ï‰ iq) (Ï‰ (k+2+p)) (Ï‰ u)
       | (u, dee_comp do_add v w) => Code_plus (Ï‰ u) (Ï‰ v) (Ï‰ w)  
       | (u, dee_comp do_mul v w) => Code_mult (Ï‰ il) (Ï‰ iq) (Ï‰ u) (Ï‰ v) (Ï‰ w)
      end.

    Let dio_rel_dc_Code c : dio_rel (dc_Code c).
    Proof. 
      destruct c as (u & [ n | v | [] | [] v w ]); unfold dc_Code; auto.
    Defined.

    (* Case of do_mul gives the overall bound of 70074  *)

    Let dc_Code_size_Z c : (df_size_Z (proj1_sig (dio_rel_dc_Code c)) <= 70074)%Z.
    Proof.
      destruct c as (u & [ n | v | [] | [] v w ]); compute; discriminate.
    Qed.

    (*  Ï‰         | (Ï† _)    ~  Ï€    |  Î½
        i < k     | i        |  i    | 
        i = k     | <0,..,l> |  ?    |
        i = k+1   |          |  q    |  
        i = k+2   |          |  l    |  0
        i > k+2   |          |       |  i-(k+2)  *)

    Let dc_Code_spec c Ï† Ï€ Î½ Ï‰ : (forall i, i < k -> is_cipher_of (Î½ 0) (Ï€ iq) (Ï† i) (Ï€ i))
                              -> (is_cipher_of (Î½ 0) (Ï€ iq) (fun n => n) (Ï€ k))
                              -> (forall x, dc_vars c x -> x < k)
                              -> (forall i, i < il -> Ï‰ i = Ï€ i)
                              -> (forall i, il <= i -> Ï‰ i = Î½ (i-il))
                             -> dc_Code c Ï‰ <-> forall j, j < Î½ 0 -> dc_eval (fun i => Ï† i j) (dv_lift Î½ j) c.
    Proof.
      intros G1 G2 G3 G4 G5.
      assert (Ï‰ il = Î½ 0) as G0.
      { rewrite G5; try omega; f_equal; omega. }
      destruct c as (u & [ n | v | [ | p ] | [] v w ]); simpl.
      + assert (u < k) as Hu. { apply G3; left; auto. }
        rewrite G0, G4, G4; try omega.
        specialize (G1 _ Hu).
        unfold dc_eval; simpl; split.
        * intros (g & Hg1 & Hg4).
          generalize (is_cipher_of_inj G1 Hg1); intros G6.
          intros; rewrite G6, Hg4; auto; omega.
        * intros; exists (Ï† u); split; auto.
      + assert (u < k) as Hu. { apply G3; cbv; auto. }
        assert (v < k) as Hv. { apply G3; cbv; auto. }
        do 2 (rewrite G4; try omega).
        unfold dc_eval; simpl.
        apply G1 in Hu.
        apply G1 in Hv.
        apply (is_cipher_of_equiv Hu Hv). 
      + assert (u < k) as Hu. { apply G3; cbv; auto. }
        do 2 (rewrite G4; try omega).
        unfold dc_eval; simpl.
        apply G1 in Hu.
        apply (is_cipher_of_equiv Hu G2).
      + rewrite G0, G4; try omega.
        rewrite G5; try omega.
        replace (il+p-il) with p by omega.
        assert (u < k) as Hu. { apply G3; cbv; auto. }
        rewrite G4; try omega.
        apply G1 in Hu.
        unfold dc_eval; simpl; split.
        * intros (g & Hg1 & Hg2).
          generalize (proj1 (is_cipher_of_equiv Hu Hg1) eq_refl); intros G6.
          intros; rewrite G6, Hg2; auto.
        * intro; exists (Ï† u); auto.
      + assert (Hu : u < k). { apply G3; cbv; auto. }
        assert (Hv : v < k). { apply G3; cbv; auto. }
        assert (Hw : w < k). { apply G3; cbv; auto. }
        do 3 (rewrite G4; try omega).
        apply G1 in Hu; apply G1 in Hv; apply G1 in Hw.
        rewrite Code_plus_spec with (1 := Hu) (2 := Hv) (3 := Hw).
        unfold dc_eval; simpl; tauto.
      + assert (Hu : u < k). { apply G3; cbv; auto. }
        assert (Hv : v < k). { apply G3; cbv; auto. }
        assert (Hw : w < k). { apply G3; cbv; auto. }
        rewrite G0; do 4 (rewrite G4; try omega).
        apply G1 in Hu; apply G1 in Hv; apply G1 in Hw.
        rewrite Code_mult_spec with (1 := Hu) (2 := Hv) (3 := Hw).
        unfold dc_eval; simpl; tauto.
    Qed.

    Let dc_list_Code ll Î½ := fold_right (fun c P => dc_Code c Î½ /\ P) True ll.

    Let dio_rel_dc_list_Code ll : dio_rel (dc_list_Code ll).
    Proof. induction ll; unfold dc_list_Code; simpl; auto. Qed.

    Let dc_list_Code_spec ll Ï† Ï€ Î½ Ï‰ : (forall i, i < k -> is_cipher_of (Î½ 0) (Ï€ iq) (Ï† i) (Ï€ i))
                                    -> (is_cipher_of (Î½ 0) (Ï€ iq) (fun n => n) (Ï€ k))
                                    -> (forall c, In c ll -> forall x, dc_vars c x -> x < k)
                                    -> (forall i, i < il  -> Ï‰ i = Ï€ i)
                                    -> (forall i, il <= i -> Ï‰ i = Î½ (i-il))
                                    -> dc_list_Code ll Ï‰ 
                                   <-> forall j, j < Î½ 0 -> Forall (dc_eval (fun i => Ï† i j) (dv_lift Î½ j)) ll.
    Proof.
      intros G1 G2 G3 G4 G5; revert G3.
      rewrite <- Forall_forall.
      induction 1 as [ | c ll F1 F2 IF2 ]; simpl.
      + split; auto.
      + rewrite IF2, dc_Code_spec; auto. 
        split.
        * intros (E1 & E2) j Hj; constructor; auto.
        * intros E1; split; intros j Hj; specialize (E1 _ Hj);
            rewrite Forall_cons_inv in E1; tauto.
    Qed.

    Let ciphers Î½ := CodeNat (Î½ il) (Î½ iq) (Î½ k) /\ forall i, i < k -> Code (Î½ il) (Î½ iq) (Î½ i).

    Let dio_rel_ciphers : dio_rel ciphers.
    Proof. 
      apply dio_rel_conj.
      + auto.
      + apply dio_rel_mconj; intros; auto. 
    Defined.

    Let ciphers_spec Î½ : ciphers Î½ <-> is_cipher_of (Î½ il) (Î½ iq) (fun n => n) (Î½ k) 
                                    /\ exists Ï†, forall i, i < k -> is_cipher_of (Î½ il) (Î½ iq) (Ï† i) (Î½ i).
    Proof. 
      unfold ciphers, Code, CodeNat.
      split; intros (H1 & H2); split; auto; clear H1.
      + apply fmap_reifier_default in H2; auto.
      + destruct H2 as (phi & Hphi).
        intros i Hi; exists (phi i); auto.
    Qed.

    Variables (ll : list dio_constraint) 
              (Hll : forall c x, In c ll -> dc_vars c x -> x < k).

    Let Hll' : forall c, In c ll -> forall x, dc_vars c x -> x < k.
    Proof. intros c ? x ?; apply (@Hll c x); auto. Qed.

    Let pre_quant Î½ := Î½ il+1 < Î½ iq /\ ciphers Î½ /\ dc_list_Code ll Î½.

    Let dio_rel_pre_quant : dio_rel pre_quant.
    Proof. unfold pre_quant; auto. Defined.

    Definition dc_list_bfall Î½ := exists Ï€, pre_quant (fun i => if le_lt_dec il i then Î½ (i-il) else Ï€ i).

    Let dc_list_bfall_spec_1 Î½ :
          dc_list_bfall Î½ <-> exists q Ï†, Î½ 0+1 < q 
                                      /\ (forall i j, i < k -> j < Î½ 0 -> Ï† i j < power q 2) 
                                      /\ forall j, j < Î½ 0 -> Forall (dc_eval (fun i => Ï† i j) (dv_lift Î½ j)) ll.
    Proof.
      split.
      + intros (pi & G0 & G1 & G4).
        rewrite ciphers_spec in G1.
        destruct (le_lt_dec il k) as [ ? | _ ]; try omega.
        destruct (le_lt_dec il il) as [ _  | ? ]; try omega.
        destruct (le_lt_dec il iq) as [ ? | _ ]; try omega.
        replace (il-il) with 0 in * by omega.
        destruct G1 as (G1 & phi & G3).
        assert (forall i, i < k -> is_cipher_of (Î½ 0) (pi iq) (phi i) (pi i)) as G2.
        { intros i Hi; generalize (G3 _ Hi); destruct (le_lt_dec il i); auto; omega. }
        clear G3.
        rewrite dc_list_Code_spec with (Ï€ := pi) (Ï† := phi) (Î½ := Î½) in G4; auto.
        2,3: intros i Hi; destruct (le_lt_dec il i) as [ H | H ]; auto; try omega.
        exists (pi iq), phi; repeat (split; auto). 
        intros i j Hi Hj; destruct (G2 _ Hi) as (_ & G3 & _); auto.
      + intros (q & phi & Hq & Hphi1 & Hphi2).
        assert (q <= power q 2) as Hq' by (apply power_ge_n; auto).
        destruct (the_cipher (fun i => i) Hq) as (u & Hu). { intros; omega. }

        set (pi i := match lt_eq_lt_dec i k with
                     | inleft (left H)  => proj1_sig (the_cipher (phi i) Hq (fun j Hj => Hphi1 _ _ H Hj)) 
                     | inleft (right H) => u
                     | inright H        => q
                   end).
        assert (Hpi_k : pi k = u).
        { unfold pi; destruct (lt_eq_lt_dec k k) as [ [] | ]; auto; try omega. }
        assert (forall i, i < k -> is_cipher_of (Î½ 0) q (phi i) (pi i)) as Hpi.
        { unfold pi; intros i Hi.
          destruct (lt_eq_lt_dec i k) as [ [H | ] | ]; try omega.
          apply (proj2_sig (the_cipher (phi i) Hq (fun j Hj => Hphi1 _ _ H Hj))). }
        assert (Hpi_q : pi iq = q).
        { unfold pi; destruct (lt_eq_lt_dec iq k) as [ [H | ] | ]; try omega. }
        generalize pi Hpi_k Hpi_q Hpi; clear pi Hpi_k Hpi Hpi_q.
        intros pi Hpi_k Hpi_q Hpi; subst u.

        exists pi; red.
        rewrite ciphers_spec.
        destruct (le_lt_dec il k) as [ ? | _ ]; try omega.
        destruct (le_lt_dec il il) as [ _ | ? ]; try omega.
        destruct (le_lt_dec il iq) as [ ? | _ ]; try omega.
        rewrite Nat.sub_diag. 
        subst q; repeat (split; auto).
        * exists phi; intros i Hi.
          destruct (le_lt_dec il i); try omega; auto.
        * rewrite dc_list_Code_spec with (Ï€ := pi) (Ï† := phi); auto;
            intros i Hi; destruct (le_lt_dec il i); auto; omega.
    Qed.

    Let dc_list_bfall_spec Î½ : (forall i, i < Î½ 0 -> exists Ï†, Forall (dc_eval Ï† (dv_lift Î½ i)) ll) <-> dc_list_bfall Î½ .
    Proof.
      rewrite dc_list_bfall_spec_1; split.
      + intros H.
        apply fmmap_reifer_bound  with (p := k) in H.
        - destruct H as (m & phi & Hf).
          set (q := power (Î½ 0+2+m) 2).
          assert (Î½ 0+1 < q) as Hlq.
          { apply lt_le_trans with (Î½ 0+2+m); try omega.
            apply power_ge_n; auto. }
          assert (m <= power q 2) as Hmq.
          { apply le_trans with q.
            apply le_trans with (Î½ 0+2+m); try omega.
            apply power_ge_n; auto.
            apply power_ge_n; auto. }
          exists q, (fun i j => phi j i); split; [ | split ]; auto.
          * intros i j Hi Hj; apply lt_le_trans with m; auto; apply Hf; auto.
          * intros; apply Hf; auto.
        - intros x f g Hfg.
          apply Forall_impl.
          intros c Hc; apply dc_eval_ext; auto.
          intros z Hz; symmetry; apply Hfg, Hll with c; auto.
      + intros (q & phi & Hq & H1 & H2) j Hj.
        exists (fun i => phi i j); auto.
    Qed.

    Theorem dio_rel_dc_list_bfall : dio_rel (fun Î½ => forall i, i < Î½ 0 -> exists Ï†, Forall (dc_eval Ï† (dv_lift Î½ i)) ll).
    Proof.
      apply dio_rel_equiv with (1 := dc_list_bfall_spec).
      unfold dc_list_bfall.
      destruct dio_rel_pre_quant as (f & Hf).
      eexists (df_mexists il f).
      intros; rewrite df_mexists_spec; split;
      intros (phi & H); exists phi; revert H; rewrite <- Hf; auto.
    Defined.

  End dio_bounded_elem.

  Theorem dio_bounded_fall P : dio_rel P -> dio_rel (fun Î½ => forall i, i < Î½ 0 -> P (dv_lift Î½ i)).
  Proof.
    intros (f & Hf).
    destruct (dio_formula_elem f) as (ll & H1 & H2 & H3).
    revert H2; generalize (4*df_size f); intros k H2.
    generalize (dio_rel_dc_list_bfall _ H2).
    apply dio_rel_equiv; intros v.
    split; intros H i Hi; generalize (H _ Hi); rewrite <- Hf, H3; auto.
  Defined.

End dio_bounded_fall.

(* dfbfall f : where f[*,v] has one free variable 
      is equivalent to [n,v] => f[0,v] /\ f[1,v] /\ ... /\ f[n-1,v] 
      also with one free variable 

   Notice that the value of n is not available to f *) 

Definition dv_change (Î½ : nat -> nat) x n := match n with 0 => x | _ => Î½ n end.

Section dfbfall.
 
  Variable (f : dio_formula).

  Let rho i := match i with 0 => 0 | S i => S (S i) end. 

  Let dfbfall_full : dio_rel (fun Î½ => forall i, i < Î½ 0 -> df_pred f (dv_change Î½ i)).
  Proof.
    assert (dio_rel (df_pred (df_ren rho f))) as H.
    { exists (df_ren rho f); tauto. }
    destruct (dio_bounded_fall H) as (g & Hg).
    exists g.
    intros v.
    rewrite Hg. 
    split; intros G i Hi; generalize (G _ Hi);  
      rewrite df_pred_ren; apply df_pred_ext;
      intros [ | [ | x ] ]; simpl; auto.
  Qed.

  Definition dfbfall := proj1_sig dfbfall_full.

  Fact dfbfall_spec : forall Î½, df_pred dfbfall Î½ <-> forall i, i < Î½ 0 -> df_pred f (dv_change Î½ i).
  Proof. apply (proj2_sig dfbfall_full). Qed.

End dfbfall.

Section df_fall_lt.

  Variable (f : dio_formula) (x : dio_expression).

  Definition df_fall_lt := df_subst (fun n => match n with 0 => x | S n => de_var (S n) end) (dfbfall f).

  Fact df_fall_lt_spec Î½ : df_pred df_fall_lt Î½ <-> forall n, n < de_eval Î½ x -> df_pred f (dv_change Î½ n).
  Proof.
    unfold df_fall_lt.
    rewrite df_pred_subst, dfbfall_spec.
    split; intros H n Hn; generalize (H _ Hn);
      apply df_pred_ext;
      intros [ | ]; simpl; auto.
  Qed.

End df_fall_lt.

Corollary dio_rel_fall_lt_0 (K : nat -> (nat -> nat) -> Prop) : 
            ð�”»R (fun Î½ => K (Î½ 0) (fun n => Î½ (S n))) 
   -> ð�”»R (fun Î½ => forall x, x < Î½ 0 -> K x (fun n => Î½ (S n))).
Proof.
  intros (fK & HK).
  exists (df_fall_lt fK (de_var 0)).
  intros; rewrite df_fall_lt_spec.
  simpl. 
  split; intros H n Hn; generalize (H _ Hn); rewrite HK; auto.
Defined.

Theorem dio_rel_fall_lt a (K : nat -> (nat -> nat) -> Prop) : 
            ð�”»P a
   -> ð�”»R (fun Î½ => K (Î½ 0) (fun n => Î½ (S n))) 
   -> ð�”»R (fun Î½ => forall x, x < a Î½ -> K x Î½).
Proof.
  intros (ea & Ha) H.
  apply dio_rel_fall_lt_0 in H.
  destruct H as (f & Hf).
  exists (df_subst (fun n => match n with 0 => ea | S n => de_var n end) f).
  intro; rewrite df_pred_subst, Hf.
  simpl; split; intros H n Hn; apply H; revert Hn; rewrite Ha; auto.
Defined.

Check dio_rel_fall_lt.
Print Assumptions dio_rel_fall_lt.

Hint Resolve dio_rel_fall_lt.

Theorem dio_rel_fall_lt_bound a (K : nat -> nat -> (nat -> nat) -> Prop) : 
            ð�”»P a
   -> ð�”»R (fun Î½ => K (Î½ 0) (a (fun n => Î½ (S n))) (fun n => Î½ (S n))) 
   -> ð�”»R (fun Î½ => forall x, x < a Î½ -> K x (a Î½) Î½).
Proof.
  intros; apply dio_rel_fall_lt; auto.
Qed.

Hint Resolve dio_rel_fall_lt_bound.

Theorem dio_rel_fall_le a (K : nat -> (nat -> nat) -> Prop) : 
            ð�”»P a
   -> ð�”»R (fun Î½ => K (Î½ 0) (fun n => Î½ (S n))) 
   -> ð�”»R (fun Î½ => forall x, x <= a Î½ -> K x Î½).
Proof.
  intros Ha HK.
  apply dio_rel_equiv with (fun v => forall x, x < 1+a v -> K x v); auto.
  intros v; split; intros H x Hx; apply H; omega.
Defined.

Hint Resolve dio_rel_fall_le.
