Require Import List Arith Lia.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_list.

From Undecidability.H10.Dio
  Require Import dio_logic.

Set Implicit Arguments.

Set Default Proof Using "Type".

Section interval.


  Definition interval := ( * )%type.
  Implicit Types (i j : interval).

  Definition in_interval i x := let (a,b) := i in a x < b.
  Definition out_interval i x := let (a,b) := i in x < a b x.
  Definition interval_disjoint i j := x, in_interval i x in_interval j x False.

  Definition interval_union (i j : interval) :=
    match i, j with (,),(,) (min , max ) end.

  Fact in_out_interval i x : in_interval i x out_interval i x False.
  Proof. destruct i; simpl; . Qed.

  Fact in_out_interval_dec i x : { in_interval i x } + { out_interval i x }.
  Proof.
    destruct i as (a,b); simpl.
    destruct (le_lt_dec a x); destruct (le_lt_dec b x); try (left; );right; .
  Qed.


  Fact interval_union_left i j x : in_interval i x in_interval (interval_union i j) x.
  Proof.
    revert i j; intros (a,b) (u,v); simpl.
    generalize (Nat.le_min_l a u) (Nat.le_max_l b v); .
  Qed.


  Fact interval_union_right i j x : in_interval j x in_interval (interval_union i j) x.
  Proof.
    revert i j; intros (a,b) (u,v); simpl.
    generalize (Nat.le_min_r a u) (Nat.le_max_r b v); .
  Qed.


  Definition valuation_union i1 (g1 : ) i2 g2 :
               interval_disjoint
             { g | ( x, in_interval x g x = x)
                   ( x, in_interval x g x = x) }.
  Proof.
    intros .
    exists ( x if in_out_interval_dec x then x else x).
    split; intros x Hx.
    + destruct (in_out_interval_dec x) as [ | ]; auto.
      exfalso; revert Hx ; apply in_out_interval.
    + destruct (in_out_interval_dec x) as [ | ]; auto.
      exfalso; revert Hx; apply .
  Qed.


  Definition valuation_one_union k v i1 (g1 : ) i2 g2 :
                in_interval (interval_union ) k
             interval_disjoint
             { g | g k = v ( x, in_interval x g x = x)
                              ( x, in_interval x g x = x) }.
  Proof.
    intros .
    exists ( x if eq_nat_dec x k then v
                     else if in_out_interval_dec x then x
                     else x).
    split; [ | split ].
    + destruct (eq_nat_dec k k) as [ | [] ]; auto.
    + intros x Hx.
      destruct (eq_nat_dec x k) as [ | ].
      * subst; destruct ; apply interval_union_left; auto.
      * destruct (in_out_interval_dec x) as [ | ]; auto.
        exfalso; revert Hx ; apply in_out_interval.
    + intros x Hx.
      destruct (eq_nat_dec x k) as [ | ].
      * subst; destruct ; apply interval_union_right; auto.
      * destruct (in_out_interval_dec x) as [ | ]; auto.
        exfalso; revert Hx; apply .
  Qed.


End interval.

Section diophantine_system.


  Inductive dio_elem_expr : Set :=
    | dee_nat : dio_elem_expr
    | dee_var : dio_elem_expr
    | dee_par : dio_elem_expr
    | dee_comp : dio_op dio_elem_expr.
  Notation dee_add := (dee_comp do_add).
  Notation dee_mul := (dee_comp do_mul).

  Definition dee_eval φ ν e :=
    match e with
      | dee_nat n n
      | dee_var v φ v
      | dee_par i ν i
      | dee_comp o v w de_op_sem o (φ v) (φ w)
    end.

  Definition dee_vars e x :=
    match e with
      | dee_nat _ False
      | dee_var v x = v
      | dee_par _ False
      | dee_comp _ v w x = v x = w
    end.

  Fact dee_eval_ext e φ1 ν1 φ2 ν2 :
        ( x, dee_vars e x φ1 x = φ2 x)
      ( x, ν1 x = ν2 x)
      dee_eval φ1 ν1 e = dee_eval φ2 ν2 e.
  Proof. destruct e as [ | | | [] ]; simpl; auto. Qed.

  Definition dee_dec k e :=
    match e with
      | dee_nat n dee_nat n
      | dee_var v dee_var v
      | dee_par 0 dee_var k
      | dee_par (S i) dee_par i
      | dee_comp o v w dee_comp o v w
    end.

  Fact dee_eval_dec φ ν k e : dee_eval φ ν (dee_dec k e) = dee_eval φ ( x match x with 0 φ k | S x ν x end) e.
  Proof. destruct e as [ | | [] | [] ]; simpl; auto. Qed.

  Fact dee_vars_dec k e x : dee_vars (dee_dec k e) x x = k dee_vars e x.
  Proof. destruct e as [ | | [] | [] ]; simpl; firstorder. Qed.

  Definition dio_constraint := ( * dio_elem_expr)%type.

  Implicit Type (c : dio_constraint).

  Definition dc_eval φ ν c := φ (fst c) = dee_eval φ ν (snd c).

  Arguments dc_eval φ ν c /.

  Definition dc_vars c x := x = fst c dee_vars (snd c) x.

  Arguments dc_vars c x /.

  Fact dc_eval_ext c φ1 ν1 φ2 ν2 :
        ( x, dc_vars c x φ1 x = φ2 x)
      ( x, ν1 x = ν2 x)
      dc_eval φ1 ν1 c dc_eval φ2 ν2 c.
  Proof.
    intros .
    destruct c as (v,e); unfold dc_eval; simpl.
    rewrite ; simpl; auto.
    rewrite dee_eval_ext with e φ1 ν1 φ2 ν2; try tauto.
    intros; apply ; simpl; auto.
  Qed.


  Definition dc_dec k c := (fst c, dee_dec k (snd c)).

  Fact dc_eval_dec φ ν k c : dc_eval φ ν (dc_dec k c) dc_eval φ ( x match x with 0 φ k | S x ν x end) c.
  Proof. destruct c; simpl; rewrite dee_eval_dec; tauto. Qed.

  Fact dc_vars_dec k c x : dc_vars (dc_dec k c) x x = k dc_vars c x.
  Proof. destruct c; simpl; intros [ | H ]; auto; apply dee_vars_dec in H; tauto. Qed.

  Implicit Type (R : ( ) Prop).


  Record dio_repr_at R a n l := {
    ds_eqns : list dio_constraint;
    ds_ref : ;
    ds_H0 : length ds_eqns = l;
    ds_H1 : x c, In c ds_eqns dc_vars c x a x < a+n;
    ds_H2 : a ds_ref < a+n;
    ds_H3 : ν, φ, Forall (dc_eval φ ν) ds_eqns;
    ds_H4 : ν, R ν φ, Forall (dc_eval φ ν) ds_eqns φ ds_ref = 0;
  }.

  Local Definition (n x0 x1 x2 x3 x4 x5 x6 x7 m : ) := if le_lt_dec n m then
                                 match m - n with
                                   | 0
                                   | 1
                                   | 2
                                   | 3
                                   | 4
                                   | 5
                                   | 6
                                   | _
                                end
                              else .

  Tactic Notation "g0" "auto" constr(n) constr(t) :=
    unfold ; destruct (le_lt_dec n (n+t)); try ;
    replace (n+t-n) with t by ; auto.

  Local Lemma g0_0 (n x0 x1 x2 x3 x4 x5 x6 x7 : ) : n (n+0) = .
  Proof. auto n 0. Qed.

  Local Lemma g0_1 (n x0 x1 x2 x3 x4 x5 x6 x7 : ) : n (n+1) = .
  Proof. auto n 1. Qed.

  Local Lemma g0_2 (n x0 x1 x2 x3 x4 x5 x6 x7 : ) : n (n+2) = .
  Proof. auto n 2. Qed.

  Local Lemma g0_3 (n x0 x1 x2 x3 x4 x5 x6 x7 : ) : n (n+3) = .
  Proof. auto n 3. Qed.

  Local Lemma g0_4 (n x0 x1 x2 x3 x4 x5 x6 x7 : ) : n (n+4) = .
  Proof. auto n 4. Qed.

  Local Lemma g0_5 (n x0 x1 x2 x3 x4 x5 x6 x7 : ) : n (n+5) = .
  Proof. auto n 5. Qed.

  Local Lemma g0_6 (n x0 x1 x2 x3 x4 x5 x6 x7 : ) : n (n+6) = .
  Proof. auto n 6. Qed.

  Local Lemma g0_7 (n x0 x1 x2 x3 x4 x5 x6 x7 : ) : n (n+7) = .
  Proof. auto n 7. Qed.

  Tactic Notation "rew" "g0" :=
    try rewrite !g0_0;
    try rewrite !g0_1;
    try rewrite !g0_2;
    try rewrite !g0_3;
    try rewrite !g0_4;
    try rewrite !g0_5;
    try rewrite !g0_6;
    try rewrite !g0_7.

  Local Lemma complete_lemma x y : { u : & { v | u+x = v+y } }.
  Proof.
    destruct (le_lt_dec x y).
    + exists (y-x), 0; .
    + exists 0, (x-y); .
  Qed.



  Lemma dio_repr_at_cst x i a : dio_repr_at ( ν ν x = i) a 6 5.
  Proof.
    exists ( (a+5,dee_add (a+0) (a+1))
           ::(a+2,dee_add (a+0) (a+3))
           ::(a+2,dee_add (a+1) (a+4))
           ::(a+3,dee_par x)
           ::(a+4,dee_nat i)
           ::nil)
           (a+5); simpl; auto; try .
    + intros j c.
      repeat (intros [ | H ]; [ simpl; try | revert H ]); try tauto.
    + intros v.
      destruct (complete_lemma (v x) i) as (p & q & H).
      exists ( a p q (p+v x) (v x) i (p+q) 0 0);
        repeat constructor; simpl; rew ; auto.
    + intros v; split.
      * intros H.
        exists ( a 0 0 (v x) (v x) i 0 0 0);
          repeat constructor; simpl; rew ; auto.
      * intros ( & H); revert H.
        repeat rewrite Forall_cons_inv; simpl; .
  Defined.



  Lemma dio_repr_at_eq x y a : dio_repr_at ( ν ν x = ν y) a 6 5.
  Proof.
    exists ( (a+5,dee_add (a+0) (a+1))
           ::(a+2,dee_add (a+0) (a+3))
           ::(a+2,dee_add (a+1) (a+4))
           ::(a+3,dee_par x)
           ::(a+4,dee_par y)
           ::nil)
           (a+5); simpl; auto; try .
    + intros j c.
      repeat (intros [ | H ]; [ simpl; try | revert H ]); try tauto.
    + intros v.
      destruct (complete_lemma (v x) (v y)) as (p & q & H).
      exists ( a p q (p+v x) (v x) (v y) (p+q) 0 0);
        repeat constructor; simpl; rew ; auto.
    + intros v; split.
      * intros H.
        exists ( a 0 0 (v x) (v x) (v y) 0 0 0);
          repeat constructor; simpl; rew ; auto.
      * intros ( & H); revert H.
        repeat rewrite Forall_cons_inv; simpl; .
  Defined.



  Lemma dio_repr_at_op o x y z a : dio_repr_at ( ν ν x = de_op_sem o (ν y) (ν z)) a 8 7.
  Proof.
    exists ( (a+7,dee_add (a+0) (a+1))
           ::(a+6,dee_add (a+0) (a+2))
           ::(a+6,dee_add (a+1) (a+5))
           ::(a+5,dee_comp o (a+3) (a+4))
           ::(a+2,dee_par x)
           ::(a+3,dee_par y)
           ::(a+4,dee_par z)
           ::nil)
           (a+7); simpl; auto; try .
    + intros j c.
      repeat (intros [ | H ]; [ simpl; try | revert H ]); try tauto.
    + intros v.
      destruct (complete_lemma (v x) (de_op_sem o (v y) (v z))) as (p & q & H).
      exists ( a p q (v x) (v y) (v z) (de_op_sem o (v y) (v z)) (p+v x) (p+q));
        repeat constructor; simpl; rew ; auto.
    + intros v; split.
      * intros H.
        exists ( a 0 0 (v x) (v y) (v z) (v x) (v x) 0);
          repeat constructor; simpl; rew ; auto.
      * intros ( & H); revert H.
        repeat rewrite Forall_cons_inv; simpl.
        intros (( & & & & & & & _) & ).
        rewrite , , ; .
  Defined.


  Local Lemma not_interval_union a1 n1 a2 n2 :
           +
         in_interval (interval_union (, + ) (, + )) ( + ).
  Proof.
    simpl; intros (_ & ).
    rewrite Nat.max_r in ; .
  Qed.


  Local Definition dio_op_swap o := match o with do_add do_mul | do_mul do_add end.

  Fact dio_repr_at_bin o R1 a1 n1 p1 R2 a2 n2 p2 n :
          dio_repr_at
        dio_repr_at
        +
        n = 1++-
        dio_repr_at ( ν df_op_sem o ( ν) ( ν)) n (1++).
  Proof.
    intros [ ] [ ] ?; subst n.
    exists ((+,dee_comp (dio_op_swap o) )::) (+).
    + simpl; rewrite app_length, , ; .
    + replace (+(1++-)) with (1++) by .
      intros x c [ Hc | Hc ].
      * subst; simpl; .
      * intros ; apply in_app_or in Hc; destruct Hc as [ Hc | Hc ].
        - specialize ( _ _ Hc ); .
        - specialize ( _ _ Hc ); .
    + .
    + intros f.
      destruct ( f) as ( & ).
      destruct ( f) as ( & ).
      destruct (@valuation_one_union (+) (de_op_sem (dio_op_swap o) ( ) ( )) (,+) (,+) )
        as (g & & & ); auto using not_interval_union.
      { red; simpl; intros; . }
      exists g; constructor; [ | apply Forall_app; split ].
      * simpl; rewrite , ( ), ( ); auto.
      * apply Forall_impl with (2 := ).
        intros c Hc; apply dc_eval_ext; auto.
        intros x Hx; apply , with c; auto.
      * apply Forall_impl with (2 := ).
        intros c Hc; apply dc_eval_ext; auto.
        intros x Hx; apply , with c; auto.
    + intros f.
      destruct o; simpl; rewrite , ; split.
      * intros [ ( & & ) | ( & & ) ].
        - destruct ( f) as ( & ).
          destruct (@valuation_one_union (+) 0 (,+) (,+) )
            as (g & & & ); auto using not_interval_union.
          { red; simpl; intros; . }
          exists g; split; auto.
          constructor; simpl; [ | apply Forall_app; split ].
          ++ rewrite , , ; auto.
          ++ apply Forall_impl with (2 := ).
             intros c Hc; apply dc_eval_ext; auto.
             intros x Hx; apply , with c; auto.
          ++ apply Forall_impl with (2 := ).
             intros c Hc; apply dc_eval_ext; auto.
             intros x Hx; apply , with c; auto.
        - destruct ( f) as ( & ).
          destruct (@valuation_one_union (+) 0 (,+) (,+) )
            as (g & & & ); auto using not_interval_union.
          { red; simpl; intros; . }
          exists g; split; auto.
          constructor; simpl; [ | apply Forall_app; split ].
          ++ rewrite , ( ), , mult_comm; auto.
          ++ apply Forall_impl with (2 := ).
             intros c Hc; apply dc_eval_ext; auto.
             intros x Hx; apply , with c; auto.
          ++ apply Forall_impl with (2 := ).
             intros c Hc; apply dc_eval_ext; auto.
             intros x Hx; apply , with c; auto.
      * intros (g & & ).
        inversion as [ | ? ? ].
        apply Forall_app in ; destruct as ( & ).
        simpl in ; rewrite in .
        symmetry in ; apply mult_is_O in .
        destruct as [ | ]; [ left | right ]; exists g; auto.
      * intros (( & & ) & ( & & )).
        destruct (@valuation_one_union (+) 0 (,+) (,+) )
          as (g & & & ); auto using not_interval_union.
        { red; simpl; intros; . }
        exists g; split; auto; constructor; simpl.
        ++ rewrite , , ; auto; .
        ++ apply Forall_app; split.
           ** apply Forall_impl with (2 := ).
              intros c Hc; apply dc_eval_ext; auto.
              intros x Hx; apply , with c; auto.
           ** apply Forall_impl with (2 := ).
              intros c Hc; apply dc_eval_ext; auto.
              intros x Hx; apply , with c; auto.
      * intros (g & & ).
        inversion as [ | ? ? ].
        apply Forall_app in ; destruct as ( & ).
        simpl in ; split; exists g; split; auto; .
  Defined.


  Lemma dio_repr_at_exst R a n m p :
          dio_repr_at R a n p
        m = n+1
        dio_repr_at ( ν n, R n·ν) a m p.
  Proof.
    intros [ l r ] ?; subst m.
    exists (map (dc_dec (a+n)) l) r.
    + rewrite map_length; auto.
    + intros x c'; rewrite in_map_iff.
      intros (c & E & Hc) H; subst.
      apply dc_vars_dec in H.
      destruct H as [ | H ]; subst; simpl; try .
      apply in H; simpl in *; auto; .
    + .
    + intros f.
      destruct ( ( x match x with 0 0 | S x f x end)) as (g & Hg).
      exists ( x if eq_nat_dec x (a+n) then 0 else g x).
      rewrite Forall_map.
      apply Forall_impl with (2 := Hg).
      intros c Hc; rewrite dc_eval_dec; apply dc_eval_ext; auto.
      * intros x Hx.
        destruct (eq_nat_dec x (a+n)); subst; auto.
        apply in Hx; auto; .
      * intros [ | x ]; auto.
        destruct (eq_nat_dec (a+n) (a+n)); tauto.
    + intros f; split.
      * intros (u & Hu).
        apply in Hu.
        destruct Hu as (g & & ).
        exists ( x if eq_nat_dec x (a+n) then u else g x); simpl; split.
        - rewrite Forall_map.
          apply Forall_impl with (2 := ).
          intros c Hc; rewrite dc_eval_dec; apply dc_eval_ext; auto.
          ++ intros x Hx.
             destruct (eq_nat_dec x (a+n)); auto.
             subst x; apply in Hx; auto; .
          ++ intros [ | x ]; auto.
             destruct (eq_nat_dec (a+n) (a+n)); tauto.
        - destruct (eq_nat_dec r (a+n)); auto.
          subst; .
      * intros (g & & ).
        exists (g (a+n)); rewrite .
        exists g; split; auto.
        revert ; do 2 rewrite Forall_forall.
        intros H c Hc.
        apply in_map with (f := dc_dec _), H in Hc.
        revert Hc; rewrite dc_eval_dec; apply dc_eval_ext; auto.
        intros []; simpl; auto.
  Defined.


  Fixpoint df_weight_1 f :=
    match f with
      | df_cst _ _ 6
      | df_eq _ _ 6
      | df_op _ _ _ _ 8
      | df_bin _ f g 1 + df_weight_1 f + df_weight_1 g
      | df_exst f 1 + df_weight_1 f
    end.

  Fact df_weigth_1_size f : df_weight_1 f 8*df_size f.
  Proof. induction f; simpl; . Qed.

  Fixpoint df_weight_2 f :=
    match f with
      | df_cst _ _ 5
      | df_eq _ _ 5
      | df_op _ _ _ _ 7
      | df_bin _ f g 1 + df_weight_2 f + df_weight_2 g
      | df_exst f df_weight_2 f
    end.

  Fact df_weigth_2_size f : df_weight_2 f 7*df_size f.
  Proof. induction f; simpl in *; . Qed.

  Lemma dio_repr_at_form n f : dio_repr_at (df_pred f) n (df_weight_1 f) (df_weight_2 f).
  Proof.
    revert n;
    induction f as [ x i | x y | o x y z | o f IHf g IHg | f IHf ]; intros n; simpl df_pred; simpl df_weight_1; simpl df_weight_2.
    + apply dio_repr_at_cst; auto.
    + apply dio_repr_at_eq; auto.
    + apply dio_repr_at_op; auto.
    + apply dio_repr_at_bin with ( := df_weight_1 f) ( := n+df_weight_1 f) ( := df_weight_1 g); auto; .
    + apply dio_repr_at_exst with (n := df_weight_1 f); auto; .
  Defined.


End diophantine_system.


Theorem dio_formula_elem f : { l | length l 1+7*df_size f
                                ( c x, In c l dc_vars c x x < 8*df_size f)
                                ν, df_pred f ν φ, Forall (dc_eval φ ν) l }.
Proof.
  destruct (dio_repr_at_form 0 f) as [l r ].
  exists ((r,dee_nat 0) :: l); split; [ | split ]; simpl length; try .
  + rewrite ; apply le_n_S, df_weigth_2_size.
  + intros c x [ [] | H ].
    * simpl dc_vars; intros [ | [] ]; subst.
      generalize (df_weigth_1_size f); intros; simpl; .
    * intros G; apply in G; auto.
      generalize (df_weigth_1_size f); intros; simpl; .
  + intros ν; rewrite .
    split; intros (φ & H); exists φ; revert H; rewrite Forall_cons_inv; simpl; tauto.
Defined.


Definition dio_fs f := proj1_sig (dio_formula_elem f).