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

(** ** Single Diophantine equations *)

Require Import List Arith Omega Nat.

Require Import utils_tac utils_list sums pos vec. 
Require Import dio_logic dio_elem.

Set Implicit Arguments.

Local Notation "∑" := (msum plus 0).

Section convexity.

  Let convex_1 x p : 2*(x*(x+p)) <= x*x+(x+p)*(x+p).
  Proof.
(* Goal: forall _ : @eq nat (mul (S (S O)) (mul x (add x p))) (add (mul x x) (mul (add x p) (add x p))), @eq nat p O *)
    rewrite mult_assoc.
(* Goal: forall _ : @eq nat (add (mul a x) (mul (add a t) y)) (add (mul a y) (mul (add a t) x)), @eq nat x y *)
    repeat rewrite Nat.mul_add_distr_r.
(* Goal: forall _ : @eq nat (Nat.mul (Nat.mul (S (S O)) x) (add x p)) (add (mul x x) (Nat.add (Nat.mul x (add x p)) (Nat.mul p (add x p)))), @eq nat (mul p p) O *)
    repeat rewrite Nat.mul_add_distr_l.
(* Goal: forall _ : @eq nat (Nat.add (Nat.mul (Nat.mul (S (S O)) x) x) (Nat.mul (Nat.mul (S (S O)) x) p)) (add (mul x x) (Nat.add (Nat.add (Nat.mul x x) (Nat.mul x p)) (Nat.add (Nat.mul p x) (Nat.mul p p)))), @eq nat (mul p p) O *)
    rewrite (mult_comm p x).
(* Goal: forall _ : @eq nat (Nat.add (Nat.mul (Nat.mul (S (S O)) x) x) (Nat.mul (Nat.mul (S (S O)) x) p)) (add (mul x x) (Nat.add (Nat.add (Nat.mul x x) (Nat.mul x p)) (Nat.add (Nat.mul x p) (Nat.mul p p)))), @eq nat (mul p p) O *)
    repeat rewrite <- mult_assoc.
(* Goal: forall _ : @eq nat (Nat.add (Nat.mul (S (S O)) (Nat.mul x x)) (Nat.mul (S (S O)) (Nat.mul x p))) (add (mul x x) (Nat.add (Nat.add (Nat.mul x x) (Nat.mul x p)) (Nat.add (Nat.mul x p) (Nat.mul p p)))), @eq nat (mul p p) O *)
    generalize (x*x) (x*p) (p*p); intros; omega.
  Qed.

  Let convex_2 x p : 2*(x*(x+p)) = x*x+(x+p)*(x+p) -> p = 0.
  Proof.
(* Goal: forall _ : @eq nat (mul (S (S O)) (mul x (add x p))) (add (mul x x) (mul (add x p) (add x p))), @eq nat p O *)
    rewrite mult_assoc.
(* Goal: forall (_ : lt a b) (_ : @eq nat (add (mul a x) (mul b y)) (add (mul a y) (mul b x))), @eq nat x y *)
    intros H.
(* Goal: @eq nat p O *)
    cut (p*p = 0).
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
    { destruct p; simpl; auto; discriminate. }
(* Goal: @eq nat (mul p p) O *)
    revert H.
(* Goal: forall _ : @eq nat (add (mul a x) (mul (add a t) y)) (add (mul a y) (mul (add a t) x)), @eq nat x y *)
    repeat rewrite Nat.mul_add_distr_r.
(* Goal: forall _ : @eq nat (Nat.mul (Nat.mul (S (S O)) x) (add x p)) (add (mul x x) (Nat.add (Nat.mul x (add x p)) (Nat.mul p (add x p)))), @eq nat (mul p p) O *)
    repeat rewrite Nat.mul_add_distr_l.
(* Goal: forall _ : @eq nat (Nat.add (Nat.mul (Nat.mul (S (S O)) x) x) (Nat.mul (Nat.mul (S (S O)) x) p)) (add (mul x x) (Nat.add (Nat.add (Nat.mul x x) (Nat.mul x p)) (Nat.add (Nat.mul p x) (Nat.mul p p)))), @eq nat (mul p p) O *)
    rewrite (mult_comm p x).
(* Goal: forall _ : @eq nat (Nat.add (Nat.mul (Nat.mul (S (S O)) x) x) (Nat.mul (Nat.mul (S (S O)) x) p)) (add (mul x x) (Nat.add (Nat.add (Nat.mul x x) (Nat.mul x p)) (Nat.add (Nat.mul x p) (Nat.mul p p)))), @eq nat (mul p p) O *)
    repeat rewrite <- mult_assoc.
(* Goal: forall _ : @eq nat (Nat.add (Nat.mul (S (S O)) (Nat.mul x x)) (Nat.mul (S (S O)) (Nat.mul x p))) (add (mul x x) (Nat.add (Nat.add (Nat.mul x x) (Nat.mul x p)) (Nat.add (Nat.mul x p) (Nat.mul p p)))), @eq nat (mul p p) O *)
    generalize (x*x) (x*p) (p*p); intros; omega.
  Qed.

  Fact convex_le x y : 2*(x*y) <= x*x+y*y.
  Proof.
(* Goal: forall _ : @eq nat (mul (S (S O)) (mul x y)) (add (mul x x) (mul y y)), @eq nat x y *)
    destruct (le_lt_dec x y).
    + replace y with (x+(y-x)) by omega.
(* Goal: le (mul (S (S O)) (Nat.mul y (add y (sub x y)))) (Nat.add (mul y y) (mul (add y (sub x y)) (add y (sub x y)))) *)
      apply convex_1.
    + rewrite (mult_comm x y), plus_comm.
      replace x with (y+(x-y)) by omega.
(* Goal: le (mul (S (S O)) (Nat.mul y (add y (sub x y)))) (Nat.add (mul y y) (mul (add y (sub x y)) (add y (sub x y)))) *)
      apply convex_1.
  Qed.

  Fact convex_eq x y : 2*(x*y) = x*x+y*y -> x = y.
  Proof.
(* Goal: forall _ : @eq nat (mul (S (S O)) (mul x y)) (add (mul x x) (mul y y)), @eq nat x y *)
    destruct (le_lt_dec x y).
    + replace y with (x+(y-x)) by omega.
(* Goal: forall _ : @eq nat (mul (S (S O)) (Nat.mul y (add y (sub x y)))) (Nat.add (mul y y) (mul (add y (sub x y)) (add y (sub x y)))), @eq nat (add y (sub x y)) y *)
      intros H; apply convex_2 in H; omega.
    + rewrite (mult_comm x y), plus_comm.
      replace x with (y+(x-y)) by omega.
(* Goal: forall _ : @eq nat (mul (S (S O)) (Nat.mul y (add y (sub x y)))) (Nat.add (mul y y) (mul (add y (sub x y)) (add y (sub x y)))), @eq nat (add y (sub x y)) y *)
      intros H; apply convex_2 in H; omega.
  Qed.

  Let convex_3 a t x y : 0 < t -> a*x+(a+t)*y = a*y+(a+t)*x -> x = y.
  Proof.
(* Goal: forall (_ : lt a b) (_ : @eq nat (add (mul a x) (mul b y)) (add (mul a y) (mul b x))), @eq nat x y *)
    intros H.
(* Goal: forall _ : @eq nat (add (mul a x) (mul (add a t) y)) (add (mul a y) (mul (add a t) x)), @eq nat x y *)
    repeat rewrite Nat.mul_add_distr_r.
(* Goal: forall _ : @eq nat (add (mul a x) (Nat.add (Nat.mul a y) (Nat.mul t y))) (add (mul a y) (Nat.add (Nat.mul a x) (Nat.mul t x))), @eq nat x y *)
    intros H1.
(* Goal: @eq nat x y *)
    apply Nat.mul_cancel_l with t; omega.
  Qed.
   
  Fact convex_neq a b x y : a < b -> a*x+b*y = a*y+b*x -> x = y.
  Proof.
(* Goal: forall (_ : lt a b) (_ : @eq nat (add (mul a x) (mul b y)) (add (mul a y) (mul b x))), @eq nat x y *)
    intros H.
    replace b with (a+(b-a)) by omega.
(* Goal: forall _ : @eq nat (add (mul a x) (mul (add a (sub b a)) y)) (add (mul a y) (mul (add a (sub b a)) x)), @eq nat x y *)
    apply convex_3; omega.
  Qed.

  Hint Resolve convex_le.

  Fact convex_n_le n (f g : nat -> nat) :  ∑ n (fun i => 2*(f i*g i)) 
                                        <= ∑ n (fun i => f i*f i + g i*g i).
  Proof.
(* Goal: forall (_ : @eq nat (@msum nat add O n (fun i : nat => mul (S (S O)) (mul (f i) (g i)))) (@msum nat add O n (fun i : nat => add (mul (f i) (f i)) (mul (g i) (g i))))) (i : nat) (_ : lt i n), @eq nat (f i) (g i) *)
    revert f g; induction n as [ | n IHn ]; intros f g.
    + rewrite msum_0; auto.
    + do 2 rewrite msum_S.
(* Goal: le (add (mul (S (S O)) (mul (f O) (g O))) (@msum nat add O n (fun n : nat => mul (S (S O)) (mul (f (S n)) (g (S n)))))) (add (add (mul (f O) (f O)) (mul (g O) (g O))) (@msum nat add O n (fun n : nat => add (mul (f (S n)) (f (S n))) (mul (g (S n)) (g (S n)))))) *)
      apply plus_le_compat; auto.
  Qed.

  Hint Resolve convex_n_le.

  Let nat_le_sum a b c d : a <= b -> c <= d -> a+c = b+d -> a = b /\ c = d.
  Proof. intros; omega. Qed.


  (* This one can be used to encode a list of equations
     x1 = y1 ... xn = yn into a single equation of size
     linear in n if all the xi, yi have a bounded size 

     Hence one can transform a system elementary diophantine
     equations into a single polynomial equation of linear
     size !! *)

  Fact convex_n_eq n (f g : nat -> nat) : ∑ n (fun i => 2*(f i*g i)) 
                                        = ∑ n (fun i => f i*f i + g i*g i)
                                    <-> forall i, i < n -> f i = g i.
  Proof.
(* Goal: iff (@dio_single_pred (pos n) P (@pair (dio_polynomial (pos n) P) (dio_polynomial (pos n) P) p q) ν) (@ex (vec nat n) (fun w : vec nat n => @eq nat (@dp_eval (pos n) P (@vec_pos nat n w) ν p) (@dp_eval (pos n) P (@vec_pos nat n w) ν q))) *)
    split.
    + revert f g; induction n as [ | n IHn ]; intros f g.
(* Goal: forall (_ : @eq nat (@msum nat add O O (fun i : nat => mul (S (S O)) (mul (f i) (g i)))) (@msum nat add O O (fun i : nat => add (mul (f i) (f i)) (mul (g i) (g i))))) (i : nat) (_ : lt i O), @eq nat (f i) (g i) *)
      * intros; omega.
(* Goal: forall (_ : lt a b) (_ : @eq nat (add (mul a x) (mul b y)) (add (mul a y) (mul b x))), @eq nat x y *)
      * do 2 rewrite msum_S; intros H.
(* Goal: forall (i : nat) (_ : lt i (S n)), @eq nat (f i) (g i) *)
        apply nat_le_sum in H; auto.
(* Goal: forall (i : nat) (_ : lt i (S n)), @eq nat (f i) (g i) *)
        destruct H as (H1 & H2).
(* Goal: forall (i : nat) (_ : lt i (S n)), @eq nat (f i) (g i) *)
        apply convex_eq in H1.
(* Goal: forall (i : nat) (_ : lt i (S n)), @eq nat (f i) (g i) *)
        specialize (IHn _ _ H2).
(* Goal: forall (i : nat) (_ : lt i (S n)), @eq nat (f i) (g i) *)
        intros [ | ] ?; auto; apply IHn; omega.
    + intros Hfg.
(* Goal: @eq nat (@msum nat add O n (fun i : nat => mul (S (S O)) (mul (f i) (g i)))) (@msum nat add O n (fun i : nat => add (mul (f i) (f i)) (mul (g i) (g i)))) *)
      apply msum_ext.
(* Goal: forall (i : nat) (_ : lt i n), @eq nat (mul (S (S O)) (mul (f i) (g i))) (add (mul (f i) (f i)) (mul (g i) (g i))) *)
      intros i Hi; rewrite Hfg; auto; ring.
  Qed.

End convexity.

Section diophantine_polynomial.

  Variable (V P : Set).

  Inductive dio_polynomial : Set :=
    | dp_nat : nat -> dio_polynomial                  (* natural number constant *)
    | dp_var : V   -> dio_polynomial                  (* existentially quantified variable *)
    | dp_par : P   -> dio_polynomial                  (* parameter *)
    | dp_comp : dio_op -> dio_polynomial -> dio_polynomial -> dio_polynomial.

  Notation dp_add := (dp_comp do_add).
  Notation dp_mul := (dp_comp do_mul).

  Fixpoint dp_var_list p :=
    match p with
      | dp_nat _      => nil
      | dp_var v      => v::nil
      | dp_par _      => nil
      | dp_comp _ p q => dp_var_list p ++ dp_var_list q
    end.

  Fixpoint dp_par_list p :=
    match p with
      | dp_nat _      => nil
      | dp_var _      => nil
      | dp_par x      => x::nil
      | dp_comp _ p q => dp_par_list p ++ dp_par_list q
    end.

  (* ρ σ ν φ *)

  Fixpoint dp_eval φ ν p := 
    match p with
      | dp_nat n => n
      | dp_var v => φ v
      | dp_par i => ν i
      | dp_comp do_add p q => dp_eval φ ν p + dp_eval φ ν q 
      | dp_comp do_mul p q => dp_eval φ ν p * dp_eval φ ν q 
    end.

  Fact dp_eval_ext φ ν φ' ν' p :
        (forall v, In v (dp_var_list p) -> φ v = φ' v) 
     -> (forall i, In i (dp_par_list p) -> ν i = ν' i) 
     -> dp_eval φ ν p = dp_eval φ' ν' p.
  Proof.
    induction p as [ | | | [] p Hp q Hq ]; simpl; intros H1 H2; f_equal; auto;
      ((apply Hp || apply Hq); intros; [ apply H1 | apply H2 ]; apply in_or_app; auto).
  Qed.

  Fact dp_eval_fix_add φ ν p q : dp_eval φ ν (dp_add p q) = dp_eval φ ν p + dp_eval φ ν q.
  Proof. trivial. Qed.

  Fact dp_eval_fix_mul φ ν p q : dp_eval φ ν (dp_mul p q) = dp_eval φ ν p * dp_eval φ ν q.
  Proof. trivial. Qed.

  Fixpoint dp_size p :=
    match p with
      | dp_nat n => 1
      | dp_var v => 1
      | dp_par i => 1
      | dp_comp _ p q => 1 + dp_size p + dp_size q 
    end.

  Fact dp_size_fix_comp o p q : dp_size (dp_comp o p q) = 1 + dp_size p + dp_size q.
  Proof. auto. Qed.

  Definition dio_single := (dio_polynomial * dio_polynomial)%type.
  Definition dio_single_size (e : dio_single) := dp_size (fst e) + dp_size (snd e).

  Definition dio_single_pred e ν := exists φ, dp_eval φ ν (fst e) = dp_eval φ ν (snd e).

End diophantine_polynomial.

(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
Arguments dp_nat {V P}.
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
Arguments dp_var {V P}.
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
Arguments dp_par {V P}.
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
Arguments dp_comp {V P}.

Notation dp_add := (dp_comp do_add).
Notation dp_mul := (dp_comp do_mul).

Section dio_elem_dio_poly.

  Let dp_2xy u v : dio_polynomial nat nat := dp_mul (dp_nat 2) (dp_mul u v).
  Let dp_x2y2 u v : dio_polynomial nat nat := dp_add (dp_mul u u) (dp_mul v v).

  Let dp_2xy_size u v : dp_size (dp_2xy u v) = 3+dp_size u+dp_size v.
  Proof. auto. Qed.

  Let dp_x2y2_size u v : dp_size (dp_x2y2 u v) = 3+2*dp_size u+2*dp_size v.
  Proof. simpl; omega. Qed.

  Let dp_common e : dio_polynomial nat nat :=
    match e with
      | dee_nat c      => dp_nat c
      | dee_var v      => dp_var v
      | dee_par p      => dp_par p
      | dee_comp o v w => dp_comp o (dp_var v) (dp_var w)
    end.

  Let dp_common_size e : dp_size (dp_common e) <= 3.
  Proof. destruct e as [ | | | [] ]; simpl; auto. Qed.

  Let dp_eval_common φ ν e : dp_eval φ ν (dp_common e) = dee_eval φ ν e.
  Proof. destruct e as [ | | | [] ]; auto. Qed.  

  Let dp_left (c : dio_constraint) := dp_2xy (dp_var (fst c)) (dp_common (snd c)).
  Let dp_right (c : dio_constraint) := dp_x2y2 (dp_var (fst c)) (dp_common (snd c)).
 
  Let dee2dp_1 l := fold_right dp_add (dp_nat 0) (map dp_left l).
  Let dee2dp_2 l := fold_right dp_add (dp_nat 0) (map dp_right l).

  Let dee2dp_1_size l : dp_size (dee2dp_1 l) <= 1+8*length l.
  Proof.
(* Goal: le (@dp_size nat nat (dee2dp_2 l)) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint l))) *)
    induction l as [ | (x,e) l IHl ].
    + simpl; auto.
    + unfold dee2dp_1; simpl fold_right; fold (dee2dp_1 l).
(* Goal: le (@dp_size nat nat (@dp_comp nat nat do_add (dp_right (@pair nat dio_elem_expr x e)) (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint (@cons dio_constraint (@pair nat dio_elem_expr x e) l)))) *)
      rewrite dp_size_fix_comp.
(* Goal: le (add (add (S O) (@dp_size nat nat (dp_left (@pair nat dio_elem_expr x e)))) (@dp_size nat nat (dee2dp_1 l))) (add (S O) (mul (S (S (S (S (S (S (S (S O)))))))) (@length dio_constraint (@cons dio_constraint (@pair nat dio_elem_expr x e) l)))) *)
      unfold dp_left; rewrite dp_2xy_size.
(* Goal: le (add (add (S O) (add (add (S (S (S O))) (mul (S (S O)) (@dp_size nat nat (@dp_var nat nat (@fst nat dio_elem_expr (@pair nat dio_elem_expr x e)))))) (mul (S (S O)) (@dp_size nat nat (dp_common (@snd nat dio_elem_expr (@pair nat dio_elem_expr x e))))))) (@dp_size nat nat (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint (@cons dio_constraint (@pair nat dio_elem_expr x e) l)))) *)
      unfold fst, snd.
(* Goal: le (add (add (S O) (add (add (S (S (S O))) (mul (S (S O)) (@dp_size nat nat (@dp_var nat nat x)))) (mul (S (S O)) (@dp_size nat nat (dp_common e))))) (@dp_size nat nat (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint (@cons dio_constraint (@pair nat dio_elem_expr x e) l)))) *)
      generalize (dp_common_size e); intros.
(* Goal: le (add (add (S O) (add (add (S (S (S O))) (mul (S (S O)) (@dp_size nat nat (@dp_var nat nat x)))) (mul (S (S O)) (@dp_size nat nat (dp_common e))))) (@dp_size nat nat (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint (@cons dio_constraint (@pair nat dio_elem_expr x e) l)))) *)
      simpl dp_size at 1; simpl length.
(* Goal: le (add (add (S O) (add (add (S (S (S O))) (mul (S (S O)) (S O))) (mul (S (S O)) (@dp_size nat nat (dp_common e))))) (@dp_size nat nat (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (S (@length dio_constraint l)))) *)
      rewrite Nat.mul_succ_r; omega.
  Qed.

  Let dee2dp_2_size l : dp_size (dee2dp_2 l) <= 1+12*length l.
  Proof.
(* Goal: le (@dp_size nat nat (dee2dp_2 l)) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint l))) *)
    induction l as [ | (x,e) l IHl ].
    + simpl; auto.
    + unfold dee2dp_2; simpl fold_right; fold (dee2dp_2 l).
(* Goal: le (@dp_size nat nat (@dp_comp nat nat do_add (dp_right (@pair nat dio_elem_expr x e)) (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint (@cons dio_constraint (@pair nat dio_elem_expr x e) l)))) *)
      rewrite dp_size_fix_comp.
(* Goal: le (add (add (S O) (@dp_size nat nat (dp_right (@pair nat dio_elem_expr x e)))) (@dp_size nat nat (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint (@cons dio_constraint (@pair nat dio_elem_expr x e) l)))) *)
      unfold dp_right; rewrite dp_x2y2_size.
(* Goal: le (add (add (S O) (add (add (S (S (S O))) (mul (S (S O)) (@dp_size nat nat (@dp_var nat nat (@fst nat dio_elem_expr (@pair nat dio_elem_expr x e)))))) (mul (S (S O)) (@dp_size nat nat (dp_common (@snd nat dio_elem_expr (@pair nat dio_elem_expr x e))))))) (@dp_size nat nat (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint (@cons dio_constraint (@pair nat dio_elem_expr x e) l)))) *)
      unfold fst, snd.
(* Goal: le (add (add (S O) (add (add (S (S (S O))) (mul (S (S O)) (@dp_size nat nat (@dp_var nat nat x)))) (mul (S (S O)) (@dp_size nat nat (dp_common e))))) (@dp_size nat nat (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint (@cons dio_constraint (@pair nat dio_elem_expr x e) l)))) *)
      generalize (dp_common_size e); intros.
(* Goal: le (add (add (S O) (add (add (S (S (S O))) (mul (S (S O)) (@dp_size nat nat (@dp_var nat nat x)))) (mul (S (S O)) (@dp_size nat nat (dp_common e))))) (@dp_size nat nat (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (@length dio_constraint (@cons dio_constraint (@pair nat dio_elem_expr x e) l)))) *)
      simpl dp_size at 1; simpl length.
(* Goal: le (add (add (S O) (add (add (S (S (S O))) (mul (S (S O)) (S O))) (mul (S (S O)) (@dp_size nat nat (dp_common e))))) (@dp_size nat nat (dee2dp_2 l))) (add (S O) (mul (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) (S (@length dio_constraint l)))) *)
      rewrite Nat.mul_succ_r; omega.
  Qed.

  Let dc_value_1 φ ν (c : dio_constraint) := 2*(φ (fst c)*dee_eval φ ν (snd c)).
  Let dc_value_2 φ ν (c : dio_constraint) := (φ (fst c)*φ (fst c)) + (dee_eval φ ν (snd c)*dee_eval φ ν (snd c)).

  Let dee2dp_1_eval φ ν l : dp_eval φ ν (dee2dp_1 l) = fold_right plus 0 (map (dc_value_1 φ ν) l).
  Proof.
(* Goal: @eq nat (@dp_eval nat nat φ ν (dee2dp_2 l)) (@fold_right nat nat add O (@map dio_constraint nat (dc_value_2 φ ν) l)) *)
    induction l as [ | (u,e) l IHl ].
    + simpl; auto.
    + simpl fold_right; rewrite <- IHl.
(* Goal: @eq nat (@dp_eval nat nat φ ν (dee2dp_1 (@cons dio_constraint (@pair nat dio_elem_expr u e) l))) (add (dc_value_1 φ ν (@pair nat dio_elem_expr u e)) (@dp_eval nat nat φ ν (dee2dp_1 l))) *)
      unfold dee2dp_1; simpl fold_right.
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
      rewrite dp_eval_fix_add; f_equal; auto.
(* Goal: @eq nat (@dp_eval nat nat φ ν (dp_left (@pair nat dio_elem_expr u e))) (dc_value_1 φ ν (@pair nat dio_elem_expr u e)) *)
      unfold dc_value_1, dp_left, dp_2xy.
(* Goal: @eq nat (add (@dp_eval nat nat φ ν (@dp_comp nat nat do_mul (@dp_var nat nat (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e))) (@dp_var nat nat (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e))))) (@dp_eval nat nat φ ν (@dp_comp nat nat do_mul (dp_common (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e))) (dp_common (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e)))))) (add (mul (φ (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e))) (φ (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e)))) (mul (dee_eval φ ν (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e))) (dee_eval φ ν (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e))))) *)
      repeat rewrite dp_eval_fix_mul.
(* Goal: @eq nat (mul (@dp_eval nat nat φ ν (@dp_nat nat nat (S (S O)))) (mul (@dp_eval nat nat φ ν (@dp_var nat nat (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e)))) (@dp_eval nat nat φ ν (dp_common (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e)))))) (mul (S (S O)) (mul (φ (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e))) (dee_eval φ ν (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e))))) *)
      unfold fst, snd; do 2 f_equal.
(* Goal: @eq nat (@dp_eval nat nat φ ν (dp_common e)) (dee_eval φ ν e) *)
      apply dp_eval_common.
  Qed.

  Let dee2dp_2_eval φ ν l : dp_eval φ ν (dee2dp_2 l) = fold_right plus 0 (map (dc_value_2 φ ν) l).
  Proof.
(* Goal: @eq nat (@dp_eval nat nat φ ν (dee2dp_2 l)) (@fold_right nat nat add O (@map dio_constraint nat (dc_value_2 φ ν) l)) *)
    induction l as [ | (u,e) l IHl ].
    + simpl; auto.
    + simpl fold_right; rewrite <- IHl.
(* Goal: @eq nat (@dp_eval nat nat φ ν (dee2dp_2 (@cons dio_constraint (@pair nat dio_elem_expr u e) l))) (add (dc_value_2 φ ν (@pair nat dio_elem_expr u e)) (@dp_eval nat nat φ ν (dee2dp_2 l))) *)
      unfold dee2dp_2; simpl fold_right.
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
      rewrite dp_eval_fix_add; f_equal; auto.
(* Goal: @eq nat (@dp_eval nat nat φ ν (dp_right (@pair nat dio_elem_expr u e))) (dc_value_2 φ ν (@pair nat dio_elem_expr u e)) *)
      unfold dc_value_2, dp_right, dp_x2y2.
(* Goal: @eq nat (@dp_eval nat nat φ ν (@dp_comp nat nat do_add (@dp_comp nat nat do_mul (@dp_var nat nat (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e))) (@dp_var nat nat (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e)))) (@dp_comp nat nat do_mul (dp_common (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e))) (dp_common (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e)))))) (add (mul (φ (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e))) (φ (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e)))) (mul (dee_eval φ ν (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e))) (dee_eval φ ν (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e))))) *)
      rewrite dp_eval_fix_add.
(* Goal: @eq nat (add (@dp_eval nat nat φ ν (@dp_comp nat nat do_mul (@dp_var nat nat (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e))) (@dp_var nat nat (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e))))) (@dp_eval nat nat φ ν (@dp_comp nat nat do_mul (dp_common (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e))) (dp_common (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e)))))) (add (mul (φ (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e))) (φ (@fst nat dio_elem_expr (@pair nat dio_elem_expr u e)))) (mul (dee_eval φ ν (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e))) (dee_eval φ ν (@snd nat dio_elem_expr (@pair nat dio_elem_expr u e))))) *)
      repeat rewrite dp_eval_fix_mul.
      unfold fst, snd; do 2 f_equal;
(* Goal: @eq nat (@dp_eval nat nat φ ν (dp_common e)) (dee_eval φ ν e) *)
      apply dp_eval_common.
  Qed.

  Let dee2dp_spec φ ν l : dp_eval φ ν (dee2dp_1 l) = dp_eval φ ν (dee2dp_2 l)
                      <-> Forall (dc_eval φ ν) l.
  Proof.
(* Goal: iff (@eq nat (@dp_eval nat nat φ ν (dee2dp_1 l)) (@dp_eval nat nat φ ν (dee2dp_2 l))) (@Forall dio_constraint (dc_eval φ ν) l) *)
    rewrite dee2dp_1_eval, dee2dp_2_eval.
(* Goal: iff (@eq nat (@fold_right nat nat add O (@map dio_constraint nat (dc_value_1 φ ν) l)) (@fold_right nat nat add O (@map dio_constraint nat (dc_value_2 φ ν) l))) (@Forall dio_constraint (dc_eval φ ν) l) *)
    destruct (list_fun_inv l (0,dee_nat 0)) as (f & Hf).
(* Goal: iff (@eq nat (@fold_right nat nat add O (@map dio_constraint nat (dc_value_1 φ ν) l)) (@fold_right nat nat add O (@map dio_constraint nat (dc_value_2 φ ν) l))) (@Forall dio_constraint (dc_eval φ ν) l) *)
    rewrite Hf at 1 2.
(* Goal: iff (@eq nat (@fold_right nat nat add O (@map dio_constraint nat (dc_value_1 φ ν) (@map nat dio_constraint f (list_an O (@length dio_constraint l))))) (@fold_right nat nat add O (@map dio_constraint nat (dc_value_2 φ ν) (@map nat dio_constraint f (list_an O (@length dio_constraint l)))))) (@Forall dio_constraint (dc_eval φ ν) l) *)
    do 2 rewrite map_map.
(* Goal: iff (@eq nat (@fold_right nat nat add O (@map nat nat (fun x : nat => dc_value_1 φ ν (f x)) (list_an O (@length dio_constraint l)))) (@fold_right nat nat add O (@map nat nat (fun x : nat => dc_value_2 φ ν (f x)) (list_an O (@length dio_constraint l))))) (@Forall dio_constraint (dc_eval φ ν) l) *)
    do 2 rewrite <- sum_fold_map.
(* Goal: iff (@eq nat (@msum nat add O (@length dio_constraint l) (fun x : nat => dc_value_1 φ ν (f x))) (@msum nat add O (@length dio_constraint l) (fun x : nat => dc_value_2 φ ν (f x)))) (@Forall dio_constraint (dc_eval φ ν) l) *)
    unfold dc_value_1, dc_value_2.
(* Goal: iff (@eq nat (@msum nat add O (@length dio_constraint l) (fun x : nat => mul (S (S O)) (mul (φ (@fst nat dio_elem_expr (f x))) (dee_eval φ ν (@snd nat dio_elem_expr (f x)))))) (@msum nat add O (@length dio_constraint l) (fun x : nat => add (mul (φ (@fst nat dio_elem_expr (f x))) (φ (@fst nat dio_elem_expr (f x)))) (mul (dee_eval φ ν (@snd nat dio_elem_expr (f x))) (dee_eval φ ν (@snd nat dio_elem_expr (f x))))))) (@Forall dio_constraint (dc_eval φ ν) l) *)
    rewrite convex_n_eq.
(* Goal: iff (forall (i : nat) (_ : lt i (@length dio_constraint l)), @eq nat (φ (@fst nat dio_elem_expr (f i))) (dee_eval φ ν (@snd nat dio_elem_expr (f i)))) (@Forall dio_constraint (dc_eval φ ν) l) *)
    unfold dc_eval.
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
    apply Forall_forall_map with (P := fun i =>  φ (fst i) = dee_eval φ ν (snd i)); auto.
  Qed.

(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
  Theorem dio_elem_single l : { E : dio_single nat nat | dio_single_size E <= 2+20*length l
              /\ forall ν φ, dp_eval φ ν (fst E) = dp_eval φ ν (snd E) <-> Forall (dc_eval φ ν) l }.
  Proof.
(* Goal: iff (@dio_single_pred (pos n) P (@pair (dio_polynomial (pos n) P) (dio_polynomial (pos n) P) p q) ν) (@ex (vec nat n) (fun w : vec nat n => @eq nat (@dp_eval (pos n) P (@vec_pos nat n w) ν p) (@dp_eval (pos n) P (@vec_pos nat n w) ν q))) *)
    exists (dee2dp_1 l,dee2dp_2 l); split.
    + unfold dio_single_size, fst, snd.
(* Goal: forall (_ : @eq nat (@msum nat add O O (fun i : nat => mul (S (S O)) (mul (f i) (g i)))) (@msum nat add O O (fun i : nat => add (mul (f i) (f i)) (mul (g i) (g i))))) (i : nat) (_ : lt i O), @eq nat (f i) (g i) *)
      generalize (dee2dp_1_size l) (dee2dp_2_size l); intros; omega.
    + unfold dio_single_pred, fst, snd; split; apply dee2dp_spec.
  Defined.

(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
  Theorem dio_elem_equation l : { E : dio_single nat nat | dio_single_size E <= 2+20*length l
                                            /\ forall ν, dio_single_pred E ν <-> exists φ, Forall (dc_eval φ ν) l }.
  Proof.
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
    destruct (dio_elem_single l) as (p & H1 & H2); exists p; split; auto.
(* Goal: forall ν : forall _ : nat, nat, iff (@dio_single_pred nat nat p ν) (@ex (forall _ : nat, nat) (fun φ : forall _ : nat, nat => @Forall dio_constraint (dc_eval φ ν) l)) *)
    split; intros (phi & H); exists phi; revert H; apply H2.
  Defined.

End dio_elem_dio_poly.

Corollary dio_rel_single R : 
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
      𝔻R R -> { E : dio_single nat nat | forall ν, R ν <-> dio_single_pred E ν}.
Proof.
(* Goal: forall _ : dio_rel R, @sig (dio_single nat nat) (fun E : dio_single nat nat => forall ν : forall _ : nat, nat, iff (R ν) (@dio_single_pred nat nat E ν)) *)
  intros (A & HA).
(* Goal: @sig (dio_single nat nat) (fun E : dio_single nat nat => forall ν : forall _ : nat, nat, iff (R ν) (@dio_single_pred nat nat E ν)) *)
  destruct dio_formula_elem with (f := A) as (l & _ & _ & Hl).
(* Goal: @sig (dio_single nat nat) (fun E : dio_single nat nat => forall ν : forall _ : nat, nat, iff (R ν) (@dio_single_pred nat nat E ν)) *)
  destruct dio_elem_equation with (l := l) as (E & _ & HE).
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
  exists E; intro; rewrite HE, <- Hl, HA; tauto.
Qed.

Section dio_poly_pos.

  Variable P : Set.

  Implicit Type (p : dio_polynomial nat P).

(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
  Definition dio_poly_pos m p : (forall x, In x (dp_var_list p) -> x < m) -> { q | forall φ ν, dp_eval φ ν p = dp_eval (vec_pos (fun2vec 0 m φ)) ν q }.
  Proof.
(* Goal: forall (_ : lt a b) (_ : @eq nat (add (mul a x) (mul b y)) (add (mul a y) (mul b x))), @eq nat x y *)
    induction p as [ n | v | i | o p Hp q Hq ]; intros H.
    + exists (dp_nat n); auto.
    + specialize (H v); spec in H; simpl; auto.
(* Goal: @sig (dio_polynomial (pos m) P) (fun q : dio_polynomial (pos m) P => forall (φ : forall _ : nat, nat) (ν : forall _ : P, nat), @eq nat (φ v) (@dp_eval (pos m) P (@vec_pos nat m (@fun2vec nat O m φ)) ν q)) *)
      exists (dp_var (nat2pos H)); intros phi psi; simpl.
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
      rewrite vec_pos_fun2vec, pos2nat_nat2pos; auto.
    + exists (dp_par i); auto.
    + simpl in H.
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
      destruct Hp as (p1 & H1). { intros; apply H, in_or_app; auto. }
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
      destruct Hq as (q1 & H2). { intros; apply H, in_or_app; auto. }
(* Goal: @sig (dio_polynomial (pos m) P) (fun q0 : dio_polynomial (pos m) P => forall (φ : forall _ : nat, nat) (ν : forall _ : P, nat), @eq nat (@dp_eval nat P φ ν (@dp_comp nat P o p q)) (@dp_eval (pos m) P (@vec_pos nat m (@fun2vec nat O m φ)) ν q0)) *)
      exists (dp_comp o p1 q1); intros phi psi; simpl.
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
      destruct o; f_equal; auto.
  Qed.

(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
  Theorem dio_poly_eq_pos (e : dio_single nat P) : { m : nat 
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
                                                 & { p' : dio_polynomial (pos m) P 
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
                                                 & { q' | forall ν, dio_single_pred e ν <-> dio_single_pred (p',q') ν } } }.
  Proof.
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P e ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
    destruct e as (p,q).
    destruct (list_upper_bound (dp_var_list p++dp_var_list q)) as (m & Hm).
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
    destruct (@dio_poly_pos m p) as (p1 & H1). { intros; apply Hm, in_or_app; auto. }
(* Goal: forall (x : nat) (_ : @In nat x (@dp_var_list nat P q)), lt x m *)
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
    destruct (@dio_poly_pos m q) as (q1 & H2). { intros; apply Hm, in_or_app; auto. }
(* Goal: @sigT nat (fun m : nat => @sigT (dio_polynomial (pos m) P) (fun p' : dio_polynomial (pos m) P => @sig (dio_polynomial (pos m) P) (fun q' : dio_polynomial (pos m) P => forall ν : forall _ : P, nat, iff (@dio_single_pred nat P (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q) ν) (@dio_single_pred (pos m) P (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p' q') ν)))) *)
    exists m, p1, q1; intros psi; unfold dio_single_pred.
(* Goal: iff (@ex (forall _ : nat, nat) (fun φ : forall _ : nat, nat => @eq nat (@dp_eval nat P φ psi (@fst (dio_polynomial nat P) (dio_polynomial nat P) (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q))) (@dp_eval nat P φ psi (@snd (dio_polynomial nat P) (dio_polynomial nat P) (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q))))) (@ex (forall _ : pos m, nat) (fun φ : forall _ : pos m, nat => @eq nat (@dp_eval (pos m) P φ psi (@fst (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p1 q1))) (@dp_eval (pos m) P φ psi (@snd (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) (@pair (dio_polynomial (pos m) P) (dio_polynomial (pos m) P) p1 q1))))) *)
    split; intros (phi & Hphi).
    + exists (vec_pos (fun2vec 0 m phi)); simpl.
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
      rewrite <- H1, <- H2; auto.
    + exists (vec2fun (vec_set_pos phi) 0).
(* Goal: @eq nat (@dp_eval nat P (@vec2fun nat m (@vec_set_pos nat m phi) O) psi (@fst (dio_polynomial nat P) (dio_polynomial nat P) (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q))) (@dp_eval nat P (@vec2fun nat m (@vec_set_pos nat m phi) O) psi (@snd (dio_polynomial nat P) (dio_polynomial nat P) (@pair (dio_polynomial nat P) (dio_polynomial nat P) p q))) *)
      rewrite H1, H2.
(* Goal: @eq nat (@dp_eval (pos m) P (@vec_pos nat m (@fun2vec nat O m (@vec2fun nat m (@vec_set_pos nat m phi) O))) psi p1) (@dp_eval (pos m) P (@vec_pos nat m (@fun2vec nat O m (@vec2fun nat m (@vec_set_pos nat m phi) O))) psi q1) *)
      rewrite fun2vec_vec2fun.
      eq goal Hphi; f_equal; 
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
      apply dp_eval_ext; auto; intros j _; rewrite vec_pos_set; auto. 
  Qed.

  Fact dio_poly_eq_pos_equiv n (p q : dio_polynomial (pos n) P) ν : dio_single_pred (p,q) ν <-> exists w, dp_eval (vec_pos w) ν p = dp_eval (vec_pos w) ν q.
  Proof.
(* Goal: iff (@dio_single_pred (pos n) P (@pair (dio_polynomial (pos n) P) (dio_polynomial (pos n) P) p q) ν) (@ex (vec nat n) (fun w : vec nat n => @eq nat (@dp_eval (pos n) P (@vec_pos nat n w) ν p) (@dp_eval (pos n) P (@vec_pos nat n w) ν q))) *)
    split. 
    + intros (w & Hw); exists (vec_set_pos w); eq goal Hw; f_equal; simpl; apply dp_eval_ext; auto;
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
        intros; rewrite vec_pos_set; auto.
    + intros (w & Hw); exists (vec_pos w); auto.
  Qed.

End dio_poly_pos.

Check dio_poly_eq_pos.

Section dio_poly_inst_par.

  Variable (V P : Set) (σ : P -> nat).

  Fixpoint dp_inst_par (p : dio_polynomial V P) : dio_polynomial V Empty_set :=
    match p with
      | dp_nat c       => dp_nat c
      | dp_var v       => dp_var v
      | dp_par p       => dp_nat (σ p)
      | dp_comp o p q  => dp_comp o (dp_inst_par p) (dp_inst_par q)
    end.

  Fact dp_inst_par_eval φ ν p : 
    dp_eval φ ν (dp_inst_par p) = dp_eval φ σ p.
  Proof. induction p as [ | | | [] ]; simpl; f_equal; auto. Qed.

End dio_poly_inst_par.

Section dio_poly_ren_par.

  Variable (V P Q : Set) (f : P -> Q).

  Fixpoint dp_ren_par p : dio_polynomial V Q :=
    match p with
      | dp_nat c       => dp_nat c
      | dp_var v       => dp_var v
      | dp_par p       => dp_par (f p)
      | dp_comp o p q  => dp_comp o (dp_ren_par p) (dp_ren_par q)
    end.

  Fact dp_ren_par_eval φ ν p : 
    dp_eval φ ν (dp_ren_par p) = dp_eval φ (fun i => ν (f i)) p.
  Proof. induction p as [ | | | [] ]; simpl; f_equal; auto. Qed.

End dio_poly_ren_par.

Section dio_poly_proj_par.

  Variable (V : Set) (n : nat).

  Fixpoint dp_proj_par p : dio_polynomial V (pos n) :=
    match p with
      | dp_nat c       => dp_nat c
      | dp_var v       => dp_var v
      | dp_par p       => match le_lt_dec n p with left _ => dp_nat 0 | right H => dp_par (nat2pos H) end
      | dp_comp o p q  => dp_comp o (dp_proj_par p) (dp_proj_par q)
    end.

  Fact dp_proj_par_eval φ ν p : 
    dp_eval φ ν (dp_proj_par p) = dp_eval φ (fun i => match le_lt_dec n i with left _ => 0 | right H => ν (nat2pos H) end) p.
  Proof. 
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
    induction p as [ | | p | [] ]; simpl; f_equal; auto.
(* Goal: @eq nat (@dp_size nat nat (dp_2xy u v)) (add (add (S (S (S O))) (@dp_size nat nat u)) (@dp_size nat nat v)) *)
    destruct (le_lt_dec n p); auto.
  Qed.
      
End dio_poly_proj_par.


