Require Import List Arith Nat Omega.
From Undecidability.Shared.Libs.DLW.Utils Require Import utils_list gcd prime.
From Undecidability.H10.Dio Require Import dio_logic.
Set Implicit Arguments.
Section interval.
A small interval & valuation library
Definition interval := (nat * nat)%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 := forall x, in_interval i x -> in_interval j x -> False.
Definition interval_union (i j : interval) :=
match i, j with (a1,b1),(a2,b2) => (min a1 a2, max b1 b2) end.
Fact in_out_interval i x : in_interval i x -> out_interval i x -> False.
Proof. destruct i; simpl; omega. 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; omega);right; omega.
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); omega.
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); omega.
Qed.
Definition valuation_union i1 (g1 : nat -> nat) i2 g2 :
interval_disjoint i1 i2
-> { g | (forall x, in_interval i1 x -> g x = g1 x)
/\ (forall x, in_interval i2 x -> g x = g2 x) }.
Proof.
intros H2.
exists (fun x => if in_out_interval_dec i1 x then g1 x else g2 x).
split; intros x Hx.
+ destruct (in_out_interval_dec i1 x) as [ | H3 ]; auto.
exfalso; revert Hx H3; apply in_out_interval.
+ destruct (in_out_interval_dec i1 x) as [ H3 | ]; auto.
exfalso; revert H3 Hx; apply H2.
Qed.
Definition valuation_one_union k v i1 (g1 : nat -> nat) i2 g2 :
~ in_interval (interval_union i1 i2) k
-> interval_disjoint i1 i2
-> { g | g k = v /\ (forall x, in_interval i1 x -> g x = g1 x)
/\ (forall x, in_interval i2 x -> g x = g2 x) }.
Proof.
intros H1 H2.
exists (fun x => if eq_nat_dec x k then v
else if in_out_interval_dec i1 x then g1 x
else g2 x).
split; [ | split ].
+ destruct (eq_nat_dec k k) as [ | [] ]; auto.
+ intros x Hx.
destruct (eq_nat_dec x k) as [ | ].
* subst; destruct H1; apply interval_union_left; auto.
* destruct (in_out_interval_dec i1 x) as [ | H3 ]; auto.
exfalso; revert Hx H3; apply in_out_interval.
+ intros x Hx.
destruct (eq_nat_dec x k) as [ | ].
* subst; destruct H1; apply interval_union_right; auto.
* destruct (in_out_interval_dec i1 x) as [ H3 | ]; auto.
exfalso; revert H3 Hx; apply H2.
Qed.
End interval.
Section diophantine_system.
Inductive dio_elem_expr : Set :=
| dee_nat : nat -> dio_elem_expr
| dee_var : nat -> dio_elem_expr
| dee_par : nat -> dio_elem_expr
| dee_comp : dio_op -> nat -> nat -> 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 => do_eval 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 :
(forall x, dee_vars e x -> φ1 x = φ2 x)
-> (forall x, ν1 x = ν2 x)
-> dee_eval φ1 ν1 e = dee_eval φ2 ν2 e.
Proof. destruct e as [ | | | [] ]; simpl; auto. Qed.
Definition dee_move k p :=
match p with
| dee_nat n => dee_nat n
| dee_var v => dee_var (k+v)
| dee_par i => dee_par i
| dee_comp o v w => dee_comp o (k+v) (k+w)
end.
Fact dee_eval_move k φ ν e : dee_eval φ ν (dee_move k e) = dee_eval (fun x => φ (k+x)) ν e.
Proof. destruct e as [ | | | [] ]; simpl; auto. Qed.
Fact dee_vars_move k e x : dee_vars (dee_move k e) x <-> exists y, dee_vars e y /\ x = k+y.
Proof. destruct e as [ | | | [] ]; simpl; firstorder. 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 φ (fun 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 := (nat * 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 :
(forall x, dc_vars c x -> φ1 x = φ2 x)
-> (forall x, ν1 x = ν2 x)
-> dc_eval φ1 ν1 c <-> dc_eval φ2 ν2 c.
Proof.
intros H1 H2.
destruct c as (v,e); unfold dc_eval; simpl.
rewrite H1; simpl; auto.
rewrite dee_eval_ext with e φ1 ν1 φ2 ν2; try tauto.
intros; apply H1; simpl; auto.
Qed.
Definition dc_move k c := (k+fst c, dee_move k (snd c)).
Fact dc_eval_move k φ ν c : dc_eval φ ν (dc_move k c) <-> dc_eval (fun x => φ (k+x)) ν c.
Proof.
destruct c as (v,e); simpl.
rewrite dee_eval_move; tauto.
Qed.
Fact dc_vars_move k c x : dc_vars (dc_move k c) x <-> exists y, x = k + y /\ dc_vars c y.
Proof.
destruct c as (v,e); simpl.
rewrite dee_vars_move.
split.
+ intros [ ? | (y & Hy & ?) ]; subst x; firstorder; exists v; auto.
+ intros (y & ? & [ | ]); subst; firstorder.
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 φ (fun 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 : (nat -> nat) -> Prop).
Record dio_repr_at R a n l := {
ds_eqns : list dio_constraint;
ds_ref : nat;
ds_H0 : length ds_eqns = l;
ds_H1 : forall x c, In c ds_eqns -> dc_vars c x -> a <= x < a+n;
ds_H2 : a <= ds_ref < a+n;
ds_H3 : forall ν, exists φ, Forall (dc_eval φ ν) ds_eqns;
ds_H4 : forall ν, R ν <-> exists φ, Forall (dc_eval φ ν) ds_eqns /\ φ ds_ref = 0;
}.
Section diophantine_sys_expr.
Fixpoint de_eqns e x :=
match e with
| de_cst n => (x,dee_nat n)::nil
| de_var p => (x,dee_par p)::nil
| de_comp o p q => (x,dee_comp o (x+1) (x+1+de_size p)) :: de_eqns p (x+1) ++ de_eqns q (x+1+de_size p)
end.
Fact de_eqns_length e x : length (de_eqns e x) = de_size e.
Proof.
revert x; induction e as [ | | o p Hp q Hq ]; intros x; simpl; auto.
rewrite app_length, Hp, Hq; auto.
Qed.
Fact de_size_ge_1 e : 1 <= de_size e.
Proof. destruct e; simpl; omega. Qed.
Fact de_eqns_vars e x : forall c, In c (de_eqns e x) -> forall y, dc_vars c y -> x <= y < x+de_size e.
Proof.
revert x; induction e as [ | | o p Hp q Hq ]; intros x; simpl; auto.
+ intros ? [ [] | [] ]; simpl; intros; omega.
+ intros ? [ [] | [] ]; simpl; intros; omega.
+ intros c [ Hc | Hc ]; [ | apply in_app_or in Hc; destruct Hc as [ Hc | Hc ] ]; subst; simpl.
* intros; generalize (de_size_ge_1 q); intros; omega.
* intros y Hy; apply Hp with (y := y) in Hc; simpl in *; auto; omega.
* intros y Hy; apply Hq with (y := y) in Hc; simpl in *; auto; omega.
Qed.
Fact dc_Forall_eval φ ν e x : Forall (dc_eval φ ν) (de_eqns e x) -> de_eval ν e = φ x.
Proof.
rewrite Forall_forall.
revert x; induction e as [ | v| [] p Hp q Hq ]; simpl; intros x Hx; simpl; auto.
* specialize (Hx (x,dee_nat n)); simpl in Hx; rewrite Hx; auto.
* specialize (Hx (x,dee_par v)); simpl in Hx; rewrite Hx; auto.
* rewrite Hp with (x+1), Hq with (x+1+de_size p).
- symmetry; apply (Hx (_, dee_add _ _)); auto.
- intros; apply Hx; right; apply in_or_app; auto.
- intros; apply Hx; right; apply in_or_app; auto.
* rewrite Hp with (x+1), Hq with (x+1+de_size p).
- symmetry; apply (Hx (_, dee_mul _ _)); auto.
- intros; apply Hx; right; apply in_or_app; auto.
- intros; apply Hx; right; apply in_or_app; auto.
Qed.
Fact dc_eval_exists_Forall ν e x : { φ | Forall (dc_eval φ ν) (de_eqns e x) }.
Proof.
revert x; induction e as [ | v | o p Hp q Hq ]; simpl; intros x.
+ exists (fun _ => n); constructor; simpl; auto.
+ exists (fun _ => ν v); constructor; simpl; auto.
+ destruct (Hp (x+1)) as (g1 & H2).
destruct (Hq (x+1+de_size p)) as (g2 & H4).
generalize (dc_Forall_eval _ _ H2) (dc_Forall_eval _ _ H4); intros H1 H3.
destruct (@valuation_one_union x (do_eval o (de_eval ν p) (de_eval ν q)) (x+1,x+1+de_size p) g1 (x+1+de_size p, x+1+de_size p+de_size q) g2)
as (g & H5 & H6 & H7).
* simpl; rewrite Min.min_l; omega.
* intros y; simpl; omega.
* exists g; constructor.
- red; unfold fst, snd; rewrite H5, H1, H3; simpl; f_equal; symmetry.
++ apply H6; simpl; generalize (de_size_ge_1 p); intros; omega.
++ apply H7; simpl; generalize (de_size_ge_1 q); intros; omega.
- apply Forall_app; split.
++ revert H2; do 2 rewrite Forall_forall.
intros H c Hc.
generalize (H _ Hc); apply dc_eval_ext; auto.
intros y Hy; apply H6.
apply de_eqns_vars with (1 := Hc); auto.
++ revert H4; do 2 rewrite Forall_forall.
intros H c Hc.
generalize (H _ Hc); apply dc_eval_ext; auto.
intros y Hy; apply H7.
apply de_eqns_vars with (1 := Hc); auto.
Qed.
Let compare_lemma x y : { u : nat & { v | u+x = v+y } }.
Proof.
destruct (le_lt_dec x y).
+ exists (y-x), 0; omega.
+ exists 0, (x-y); omega.
Qed.
Let g0 (n x0 x1 x2 x3 m : nat) := if le_lt_dec n m then
match m - n with
| 0 => x0
| 1 => x1
| 2 => x2
| _ => x3
end
else x3.
Let g0_0 (n x0 x1 x2 x3 : nat) : g0 n x0 x1 x2 x3 n = x0.
Proof.
unfold g0; destruct (le_lt_dec n n); try omega.
replace (n-n) with 0 by omega; auto.
Qed.
Let g0_1 (n x0 x1 x2 x3 : nat) : g0 n x0 x1 x2 x3 (n+1) = x1.
Proof.
unfold g0; destruct (le_lt_dec n (n+1)); try omega.
replace (n+1-n) with 1 by omega; auto.
Qed.
Let g0_2 (n x0 x1 x2 x3 : nat) : g0 n x0 x1 x2 x3 (n+2) = x2.
Proof.
unfold g0; destruct (le_lt_dec n (n+2)); try omega.
replace (n+2-n) with 2 by omega; auto.
Qed.
Let g0_3 (n x0 x1 x2 x3 : nat) : g0 n x0 x1 x2 x3 (n+3) = x3.
Proof.
unfold g0; destruct (le_lt_dec n (n+3)); try omega.
replace (n+3-n) with 3 by omega; auto.
Qed.
Lemma dio_repr_at_eq n e1 e2 : dio_repr_at (fun ν => de_eval ν e1 = de_eval ν e2) n (4+de_size e1+de_size e2) (3+de_size e1+de_size e2).
Proof.
exists ((n+3, dee_add (n+1) (n+4)) ::
(n+3, dee_add (n+2) (n+4+de_size e1)) ::
(n, dee_add (n+1) (n+2)) ::
(de_eqns e1 (n+4) ++ de_eqns e2 (n+4+de_size e1))) n.
+ simpl; rewrite app_length; do 2 rewrite de_eqns_length; auto.
+ intros x c [ Hc | [ Hc | [ Hc | Hc ] ] ].
* subst; simpl; generalize (de_size_ge_1 e2); omega.
* subst; simpl; generalize (de_size_ge_1 e2); omega.
* subst; simpl; generalize (de_size_ge_1 e2); omega.
* intros Hx; apply in_app_or in Hc.
destruct Hc as [ Hc | Hc ]; apply de_eqns_vars with (2 := Hx) in Hc;
simpl in *; omega.
+ simpl; omega.
+ intros f.
destruct (@dc_eval_exists_Forall f e1 (n+4)) as (g1 & H2).
destruct (@dc_eval_exists_Forall f e2 (n+4+de_size e1)) as (g2 & H4).
destruct (compare_lemma (g1 (n+4)) (g2 (n+4+de_size e1))) as (u & v & Huv).
set (g3 := g0 n (u+v) u v (u+g1 (n+4))).
destruct (@valuation_union (n+4, n+4+de_size e1) g1 (n+4+de_size e1, n+4+de_size e1+de_size e2) g2)
as (g4 & H5 & H6).
{ intro; simpl; omega. }
destruct (@valuation_union (n,n+4) g3 (n+4,n+4+de_size e1+de_size e2) g4)
as (g & H7 & H8).
{ intro; simpl; omega. }
generalize (de_size_ge_1 e1) (de_size_ge_1 e2); intros E1 E2.
exists g; repeat constructor; simpl.
* rewrite H7, H7; simpl; auto; try omega.
rewrite H8; simpl; try omega.
rewrite H5; simpl; try omega.
unfold g3; rewrite g0_1, g0_3; omega.
* rewrite H7, H7; simpl; auto; try omega.
rewrite H8; simpl; try omega.
rewrite H6; simpl; auto; try omega.
unfold g3; rewrite g0_2, g0_3; omega.
* rewrite H7, H7, H7; simpl; try omega.
unfold g3; rewrite g0_0, g0_1, g0_2; auto.
* apply Forall_app; split.
- revert H2; do 2 rewrite Forall_forall.
intros H c Hc; generalize (H _ Hc).
apply dc_eval_ext; auto.
intros x Hx; rewrite H8.
++ apply H5, de_eqns_vars with (1 := Hc); auto.
++ apply de_eqns_vars with (1 := Hc) in Hx.
simpl in *; omega.
- revert H4; do 2 rewrite Forall_forall.
intros H c Hc; generalize (H _ Hc).
apply dc_eval_ext; auto.
intros x Hx; rewrite H8.
++ apply H6, de_eqns_vars with (1 := Hc); auto.
++ apply de_eqns_vars with (1 := Hc) in Hx.
simpl in *; omega.
+ intros f; split.
* intros Hf.
destruct (@dc_eval_exists_Forall f e1 (n+4)) as (g1 & H2).
destruct (@dc_eval_exists_Forall f e2 (n+4+de_size e1)) as (g2 & H4).
generalize (dc_Forall_eval _ _ H2) (dc_Forall_eval _ _ H4); intros H1 H3.
set (g3 := g0 n 0 0 0 (de_eval f e1)).
destruct (@valuation_union (n+4, n+4+de_size e1) g1 (n+4+de_size e1, n+4+de_size e1+de_size e2) g2)
as (g4 & H5 & H6).
{ intro; simpl; omega. }
destruct (@valuation_union (n, n+4) g3 (n+4, n+4+de_size e1+de_size e2) g4)
as (g & H7 & H8).
{ intro; simpl; omega. }
generalize (de_size_ge_1 e1) (de_size_ge_1 e2); intros E1 E2.
exists g; repeat constructor; simpl.
- rewrite H7, H7; simpl; auto; try omega.
rewrite H8; simpl; try omega.
rewrite H5; simpl; try omega.
unfold g3; rewrite g0_3, g0_1; omega.
- rewrite H7, H7; simpl; auto; try omega.
rewrite H8; simpl; try omega.
unfold g3; rewrite g0_3, g0_2.
rewrite Hf, H6; simpl; auto; omega.
- rewrite H7, H7, H7; simpl; try omega.
unfold g3; rewrite g0_0, g0_1, g0_2; auto.
- apply Forall_app; split.
++ revert H2; do 2 rewrite Forall_forall.
intros H c Hc; generalize (H _ Hc).
apply dc_eval_ext; auto.
intros x Hx; rewrite H8.
** apply H5, de_eqns_vars with (1 := Hc); auto.
** apply de_eqns_vars with (1 := Hc) in Hx.
simpl in *; omega.
++ revert H4; do 2 rewrite Forall_forall.
intros H c Hc; generalize (H _ Hc).
apply dc_eval_ext; auto.
intros x Hx; rewrite H8.
** apply H6, de_eqns_vars with (1 := Hc); auto.
** apply de_eqns_vars with (1 := Hc) in Hx.
simpl in *; omega.
- rewrite H7; simpl; try omega.
unfold g3; rewrite g0_0; auto.
* intros (g & H1 & H0).
do 3 rewrite Forall_cons_inv in H1.
rewrite Forall_app in H1.
destruct H1 as (H1 & H2 & H3 & H4 & H5).
simpl in *.
rewrite dc_Forall_eval with (1 := H4).
rewrite dc_Forall_eval with (1 := H5).
omega.
Defined.
End diophantine_sys_expr.
Let not_interval_union a1 n1 a2 n2 :
a1+n1 <= a2
-> ~ in_interval (interval_union (a1, a1 + n1) (a2, a2 + n2)) (a2 + n2).
Proof.
simpl; intros H1 (_ & H3).
rewrite Nat.max_r in H3; omega.
Qed.
Lemma dio_repr_at_conj R1 a1 n1 p1 R2 a2 n2 p2 n :
dio_repr_at R1 a1 n1 p1
-> dio_repr_at R2 a2 n2 p2
-> a1+n1 <= a2
-> n = 1+a2+n2-a1
-> dio_repr_at (fun ν => R1 ν /\ R2 ν) a1 n (1+p1+p2).
Proof.
intros [ l1 r1 F0 F1 F2 F3 F4 ] [ l2 r2 G0 G1 G2 G3 G4 ] H12 ?; subst n.
exists ((a2+n2,dee_add r1 r2)::l1++l2) (a2+n2).
+ simpl; rewrite app_length, F0, G0; omega.
+ replace (a1+(1+a2+n2-a1)) with (1+a2+n2) by omega.
intros x c [ Hc | Hc ].
* subst; simpl; omega.
* intros H1; apply in_app_or in Hc; destruct Hc as [ Hc | Hc ].
- specialize (F1 _ _ Hc H1); omega.
- specialize (G1 _ _ Hc H1); omega.
+ omega.
+ intros f.
destruct (F3 f) as (g1 & H1).
destruct (G3 f) as (g2 & H2).
destruct (@valuation_one_union (a2+n2) (g1 r1+g2 r2) (a1,a1+n1) g1 (a2,a2+n2) g2)
as (g & Hg1 & Hg2 & Hg3); auto.
{ red; simpl; intros; omega. }
exists g; constructor; [ | apply Forall_app; split ].
* simpl; rewrite (Hg2 r1), (Hg3 r2); auto.
* apply Forall_impl with (2 := H1).
intros c Hc; apply dc_eval_ext; auto.
intros x Hx; apply Hg2, F1 with c; auto.
* apply Forall_impl with (2 := H2).
intros c Hc; apply dc_eval_ext; auto.
intros x Hx; apply Hg3, G1 with c; auto.
+ intros f; rewrite F4, G4; split.
* intros ((g1 & H1 & H2) & (g2 & H3 & H4)).
destruct (@valuation_one_union (a2+n2) 0 (a1,a1+n1) g1 (a2,a2+n2) g2)
as (g & Hg1 & Hg2 & Hg3); auto.
{ red; simpl; intros; omega. }
exists g; split; auto; constructor; simpl.
++ rewrite Hg1, Hg2, Hg3; auto; omega.
++ apply Forall_app; split.
** apply Forall_impl with (2 := H1).
intros c Hc; apply dc_eval_ext; auto.
intros x Hx; apply Hg2, F1 with c; auto.
** apply Forall_impl with (2 := H3).
intros c Hc; apply dc_eval_ext; auto.
intros x Hx; apply Hg3, G1 with c; auto.
* intros (g & Hg1 & Hg2).
inversion Hg1 as [ | ? ? Hg3 Hg4 ].
apply Forall_app in Hg4; destruct Hg4 as (Hg4 & Hg5).
simpl in Hg3; split; exists g; split; auto; omega.
Defined.
Lemma dio_repr_at_disj R1 a1 n1 p1 R2 a2 n2 p2 n :
dio_repr_at R1 a1 n1 p1
-> dio_repr_at R2 a2 n2 p2
-> a1+n1 <= a2
-> n = 1+a2+n2-a1
-> dio_repr_at (fun ν => R1 ν \/ R2 ν) a1 n (1+p1+p2).
Proof.
intros [ l1 r1 F0 F1 F2 F3 F4 ] [ l2 r2 G0 G1 G2 G3 G4 ] H12 ?; subst n.
exists ((a2+n2,dee_mul r1 r2)::l1++l2) (a2+n2).
+ simpl; rewrite app_length, F0, G0; omega.
+ replace (a1+(1+a2+n2-a1)) with (1+a2+n2) by omega.
intros x c [ Hc | Hc ].
* subst; simpl; omega.
* intros H1; apply in_app_or in Hc; destruct Hc as [ Hc | Hc ].
- specialize (F1 _ _ Hc H1); omega.
- specialize (G1 _ _ Hc H1); omega.
+ omega.
+ intros f.
destruct (F3 f) as (g1 & H1).
destruct (G3 f) as (g2 & H2).
destruct (@valuation_one_union (a2+n2) (g1 r1*g2 r2) (a1,a1+n1) g1 (a2,a2+n2) g2)
as (g & Hg1 & Hg2 & Hg3); auto.
{ red; simpl; intros; omega. }
exists g; constructor; [ | apply Forall_app; split ].
* simpl; rewrite (Hg2 r1), (Hg3 r2); auto.
* apply Forall_impl with (2 := H1).
intros c Hc; apply dc_eval_ext; auto.
intros x Hx; apply Hg2, F1 with c; auto.
* apply Forall_impl with (2 := H2).
intros c Hc; apply dc_eval_ext; auto.
intros x Hx; apply Hg3, G1 with c; auto.
+ intros f; rewrite F4, G4; split.
* intros [ (g1 & H1 & H2) | (g2 & H1 & H2) ].
- destruct (G3 f) as (g2 & H3).
destruct (@valuation_one_union (a2+n2) 0 (a1,a1+n1) g1 (a2,a2+n2) g2)
as (g & Hg1 & Hg2 & Hg3); auto.
{ red; simpl; intros; omega. }
exists g; split; auto.
constructor; simpl; [ | apply Forall_app; split ].
++ rewrite Hg1, Hg2, H2; auto.
++ apply Forall_impl with (2 := H1).
intros c Hc; apply dc_eval_ext; auto.
intros x Hx; apply Hg2, F1 with c; auto.
++ apply Forall_impl with (2 := H3).
intros c Hc; apply dc_eval_ext; auto.
intros x Hx; apply Hg3, G1 with c; auto.
- destruct (F3 f) as (g1 & H3).
destruct (@valuation_one_union (a2+n2) 0 (a1,a1+n1) g1 (a2,a2+n2) g2)
as (g & Hg1 & Hg2 & Hg3); auto.
{ red; simpl; intros; omega. }
exists g; split; auto.
constructor; simpl; [ | apply Forall_app; split ].
++ rewrite Hg1, (Hg3 r2), H2, mult_comm; auto.
++ apply Forall_impl with (2 := H3).
intros c Hc; apply dc_eval_ext; auto.
intros x Hx; apply Hg2, F1 with c; auto.
++ apply Forall_impl with (2 := H1).
intros c Hc; apply dc_eval_ext; auto.
intros x Hx; apply Hg3, G1 with c; auto.
* intros (g & Hg1 & Hg2).
inversion Hg1 as [ | ? ? Hg3 Hg4 ].
apply Forall_app in Hg4; destruct Hg4 as (Hg4 & Hg5).
simpl in Hg3; rewrite Hg2 in Hg3.
symmetry in Hg3; apply mult_is_O in Hg3.
destruct Hg3 as [ Hg3 | Hg3 ]; [ left | right ]; exists g; 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 (fun ν => exists n, R (dv_lift ν n)) a m p.
Proof.
intros [ l r F0 F1 F2 F3 F4 ] ?; 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 omega.
apply F1 in H; simpl in *; auto; omega.
+ omega.
+ intros f.
destruct (F3 (fun x => match x with 0 => 0 | S x => f x end)) as (g & Hg).
exists (fun 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 F1 in Hx; auto; omega.
* intros [ | x ]; auto.
destruct (eq_nat_dec (a+n) (a+n)); tauto.
+ intros f; split.
* intros (u & Hu).
apply F4 in Hu.
destruct Hu as (g & H1 & H2).
exists (fun x => if eq_nat_dec x (a+n) then u else g x); simpl; split.
- rewrite Forall_map.
apply Forall_impl with (2 := H1).
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 F1 in Hx; auto; omega.
++ intros [ | x ]; auto.
destruct (eq_nat_dec (a+n) (a+n)); tauto.
- destruct (eq_nat_dec r (a+n)); auto.
subst; omega.
* intros (g & H1 & H2).
exists (g (a+n)); rewrite F4.
exists g; split; auto.
revert H1; 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.
Defined.
Fixpoint df_weight_1 f :=
match f with
| df_atm a b => 4 + de_size a + de_size b
| df_conj f g => 1 + df_weight_1 f + df_weight_1 g
| df_disj 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 <= 4*df_size f.
Proof. induction f; simpl; omega. Qed.
Fixpoint df_weight_2 f :=
match f with
| df_atm a b => 3 + de_size a + de_size b
| df_conj f g => 1 + df_weight_2 f + df_weight_2 g
| df_disj 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 <= 3*df_size f.
Proof. induction f; simpl in *; omega. 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 [ a b | f IHf g IHg | f IHf g IHg | f IHf ]; intros n; simpl df_pred; simpl df_weight_1; simpl df_weight_2.
+ apply dio_repr_at_eq.
+ apply dio_repr_at_conj with (n1 := df_weight_1 f) (a2 := n+df_weight_1 f) (n2 := df_weight_1 g); auto; omega.
+ apply dio_repr_at_disj with (n1 := df_weight_1 f) (a2 := n+df_weight_1 f) (n2 := df_weight_1 g); auto; omega.
+ apply dio_repr_at_exst with (n := df_weight_1 f); auto; omega.
Defined.
For any diophantine logic formula f of size s, one can compute a list l
of at most 1+3*s elementary diophantine constraints, containing at
most 4*s variables and such that df_pred f ν is equivalent to
the simultaneous satisfiability at ν of all the elementary constraints in l
Theorem dio_formula_elem f : { l | length l <= 1+3*df_size f
/\ (forall c x, In c l -> dc_vars c x -> x < 4*df_size f)
/\ forall ν, df_pred f ν <-> exists φ, Forall (dc_eval φ ν) l }.
Proof.
destruct (dio_repr_at_form 0 f) as [l r H0 H1 H2 H3 H4].
exists ((r,dee_nat 0) :: l); split; [ | split ]; simpl length; try omega.
+ rewrite H0; apply le_n_S, df_weigth_2_size.
+ intros c x [ [] | H ].
* simpl dc_vars; intros [ | [] ]; subst.
generalize (df_weigth_1_size f); intros; omega.
* intros G; apply H1 in G; auto.
generalize (df_weigth_1_size f); intros; omega.
+ intros ν; rewrite H4.
split; intros (φ & H); exists φ; revert H; rewrite Forall_cons_inv; simpl; tauto.
Defined.
Definition dio_fs f := proj1_sig (dio_formula_elem f).
End diophantine_system.