Require Import Arith Lia List Bool.
From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_tac utils_list sums bounded_quantification.
From Undecidability.H10.Matija
Require Import cipher.
From Undecidability.H10.Dio
Require Import dio_logic dio_cipher dio_elem.
Set Implicit Arguments.
Set Default Proof Using "Type".
Local Notation power := (mscal mult 1).
Local Notation "∑" := (msum plus 0).
Section dio_rel_bounded_fall.
Section dio_bounded_elem.
Variable (k : nat).
Notation iq := (k+1). Notation il := (k+2).
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.
Local Fact dio_rel_dc_Code c : 𝔻R (dc_Code c).
Proof.
destruct c as (u & [ n | v | [] | [] v w ]); unfold dc_Code; dio auto.
Defined.
Hint Resolve dio_rel_dc_Code : dio_rel_db.
Local Fact 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) (j·ν) c.
Proof.
intros G1 G2 G3 G4 G5.
assert (ω il = ν 0) as G0.
{ rewrite G5; try lia; f_equal; lia. }
destruct c as (u & [ n | v | [ | p ] | [] v w ]); simpl.
+ assert (u < k) as Hu. { apply G3; left; auto. }
rewrite G0, G4, G4; try lia.
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; lia.
* 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 lia).
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 lia).
unfold dc_eval; simpl.
apply G1 in Hu.
apply (is_cipher_of_equiv Hu G2).
+ rewrite G0, G4; try lia.
rewrite G5; try lia.
replace (il+p-il) with p by lia.
assert (u < k) as Hu. { apply G3; cbv; auto. }
rewrite G4; try lia.
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 lia).
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 lia).
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.
Local Definition dc_list_Code ll ν := fold_right (fun c P => dc_Code c ν /\ P) True ll.
Local Fact dio_rel_dc_list_Code ll : 𝔻R (dc_list_Code ll).
Proof. induction ll; unfold dc_list_Code; simpl; dio auto. Qed.
Hint Resolve dio_rel_dc_list_Code : dio_rel_db.
Local Fact 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) (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.
Local Definition ciphers ν :=
CodeNat (ν il) (ν iq) (ν k)
/\ forall i, i < k -> Code (ν il) (ν iq) (ν i).
Local Fact dio_rel_ciphers : 𝔻R ciphers.
Proof.
unfold ciphers; dio auto.
apply dio_rel_finite_conj; intros; dio auto.
Defined.
Hint Resolve dio_rel_ciphers : dio_rel_db.
Local Fact 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 : 𝔻R pre_quant.
Proof. unfold pre_quant; dio auto. Defined.
Let 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) (j·ν)) ll.
Proof.
split.
+ intros (pi & G0 & G1 & G4).
rewrite ciphers_spec in G1.
destruct (le_lt_dec il k) as [ ? | _ ]; try lia.
destruct (le_lt_dec il il) as [ _ | ? ]; try lia.
destruct (le_lt_dec il iq) as [ ? | _ ]; try lia.
replace (il-il) with 0 in * by lia.
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; lia. }
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 lia.
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; lia. }
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 lia. }
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 lia.
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 lia. }
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 lia.
destruct (le_lt_dec il il) as [ _ | ? ]; try lia.
destruct (le_lt_dec il iq) as [ ? | _ ]; try lia.
rewrite Nat.sub_diag.
subst q; repeat (split; auto).
* exists phi; intros i Hi.
destruct (le_lt_dec il i); try lia; auto.
* rewrite dc_list_Code_spec with (π := pi) (φ := phi); auto;
intros i Hi; destruct (le_lt_dec il i); auto; lia.
Qed.
Let dc_list_bfall_spec ν :
(forall i, i < ν 0 -> exists φ, Forall (dc_eval φ 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 lia.
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 lia.
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.
Local Theorem dio_rel_dc_list_bfall : 𝔻R (fun ν => forall i, i < ν 0 -> exists φ, Forall (dc_eval φ i·ν) ll).
Proof using Hll.
dio by lemma dc_list_bfall_spec; unfold dc_list_bfall.
destruct dio_rel_pre_quant as (f & Hf).
exists (df_mexists il f).
abstract (intros; rewrite df_mexists_spec; split;
intros (phi & H); exists phi; revert H; rewrite <- Hf; auto).
Defined.
End dio_bounded_elem.
Local Theorem dio_rel_bounded_fall R : 𝔻R R -> 𝔻R (fun ν => forall i, i < ν 0 -> R 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.
abstract (intros v; split; intros H i Hi; generalize (H _ Hi); rewrite <- Hf, H3; auto).
Defined.
End dio_rel_bounded_fall.
Theorem dio_rel_fall_lt a (R : nat -> (nat -> nat) -> Prop) :
𝔻F a
-> 𝔻R (fun ν => R (ν 0) ν⭳)
-> 𝔻R (fun ν => forall x, x < a ν -> R x ν).
Proof.
intros Ha H.
by dio equiv (fun ν => exists y, y = a ν /\ forall x, x < y -> R x ν).
+ abstract(intros v; split;
[ exists (a v); auto
| intros (? & -> & ?); auto ]).
+ set (T v := R (v 0) v⭳⭳).
by dio equiv (fun v => forall x, x < v 0 -> T (x·v)).
* abstract (intros v; unfold T; simpl; tauto).
* apply dio_rel_bounded_fall; unfold T; simpl.
revert H; apply dio_rel_ren
with (ρ := fun n => match n with 0 => 0 | S n => S (S n) end).
Defined.
Hint Resolve dio_rel_fall_lt : dio_rel_db.
Corollary dio_rel_fall_lt_bound a (R : nat -> nat -> (nat -> nat) -> Prop) :
𝔻F a
-> 𝔻R (fun ν => R (ν 0) (a ν⭳) ν⭳)
-> 𝔻R (fun ν => forall x, x < a ν -> R x (a ν) ν).
Proof. intros; dio auto. Defined.
Corollary dio_rel_fall_le a (R : nat -> (nat -> nat) -> Prop) :
𝔻F a
-> 𝔻R (fun ν => R (ν 0) ν⭳)
-> 𝔻R (fun ν => forall x, x <= a ν -> R x ν).
Proof.
intros Ha HK.
by dio equiv (fun v => forall x, x < 1+a v -> R x v).
abstract (intros v; split; intros H x Hx; apply H; lia).
Defined.
Hint Resolve dio_rel_fall_lt_bound
dio_rel_fall_le : dio_rel_db.