Require Import Arith Nat ZArith Lia.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_tac gcd sums bounded_quantification.

Set Implicit Arguments.

Set Default Proof Using "Type".



Definition de_bruijn_ext {X} (ν : nat -> X) x :=
  fix dbe n :=
  match n with
    | 0 => x
    | S n => ν n
  end.

Notation "x · ν" := (de_bruijn_ext ν x) (at level 1, format "x · ν", left associativity).
Notation "ν ⭳" := (fun n => ν (S n)) (at level 1, format "ν ⭳", no associativity).

Fact de_bruijn_ext_proj X (ν : nat -> X) x n : (x·ν)⭳ n = ν n.
Proof. reflexivity. Qed.

Fact de_bruijn_proj_ext X (ν : nat -> X) n : (ν 0)·(ν⭳) n = ν n.
Proof. destruct n; reflexivity. Qed.


Inductive dio_op := do_add | do_mul.


Definition de_op_sem (o : dio_op) :=
  match o with
    | do_add => plus
    | do_mul => mult
  end.

Definition df_op_sem (o : dio_op) :=
  match o with
    | do_add => or
    | do_mul => and
  end.


Inductive dio_formula : Set :=
  | df_cst : forall (x : nat) (n : nat), dio_formula
  | df_eq : forall (x y : nat), dio_formula
  | df_op : forall (o : dio_op) (x y z : nat), dio_formula
  | df_bin : forall (o : dio_op) (f g : dio_formula), dio_formula
  | df_exst : dio_formula -> dio_formula.

Notation df_add := (df_op do_add).
Notation df_mul := (df_op do_mul).
Notation df_conj := (df_bin do_mul).
Notation df_disj := (df_bin do_add).

Notation "∃ x" := (df_exst x) (at level 54, right associativity).
Notation "x ∧ y" := (df_conj x y) (at level 51, right associativity, format "x ∧ y").
Notation "x ∨ y" := (df_disj x y) (at level 52, right associativity, format "x ∨ y").

Local Notation "x ≐ ⌞ n ⌟" := (df_cst x n)
      (at level 49, no associativity, format "x ≐ ⌞ n ⌟").
Local Notation "x ≐ y" := (df_eq x y)
      (at level 49, no associativity, format "x ≐ y").
Local Notation "x ≐ y ⨢ z" := (df_add x y z)
      (at level 49, no associativity, y at next level, format "x ≐ y ⨢ z").
Local Notation "x ≐ y ⨰ z" := (df_mul x y z)
      (at level 49, no associativity, y at next level, format "x ≐ y ⨰ z").

Local Reserved Notation "'⟦' t '⟧'" (at level 1, format "⟦ t ⟧").
Local Reserved Notation "f '⦃' σ '⦄'" (at level 1, format "f ⦃ σ ⦄").

Section diophantine_logic_basics.

  Fixpoint df_size f :=
    match f with
      | df_cst _ _ => 3
      | df_eq _ _ => 3
      | df_op _ _ _ _ => 5
      | df_bin _ f g => 1 + df_size f + df_size g
      | df_exst f => 1 + df_size f
    end.


  Fixpoint df_size_Z f :=
    (match f with
      | df_cst _ _ => 3
      | df_eq _ _ => 3
      | df_op _ _ _ _ => 5
      | df_bin _ f g => 1 + df_size_Z f + df_size_Z g
      | df_exst f => 1 + df_size_Z f
    end)%Z.

  Fact df_size_Z_spec f : df_size_Z f = Z.of_nat (df_size f).
  Proof.
    induction f as [ | | | ? f Hf g Hg | f Hf ]; simpl df_size;
      rewrite Nat2Z.inj_succ; try rewrite Nat2Z.inj_add; unfold df_size_Z; fold df_size_Z; auto; try lia.
  Qed.


  Fixpoint df_pred f ν :=
    match f with
      | df_cst x n => ν x = n
      | df_eq x y => ν x = ν y
      | df_op o x y z => ν x = de_op_sem o (ν y) (ν z)
      | df_bin o f g => df_op_sem o (⟦f⟧ ν) (⟦g⟧ ν)
      | df_exst f => exists n, ⟦f⟧ n·ν
    end
  where "⟦ f ⟧" := (df_pred f).


  Fact df_pred_cst x n ν : ⟦x ≐ ⌞n⌟⟧ ν = (ν x = n).
  Proof. reflexivity. Qed.

  Fact df_pred_eq x y ν : ⟦x ≐ y⟧ ν = (ν x = ν y).
  Proof. reflexivity. Qed.

  Fact df_pred_add x y z ν : ⟦x ≐ y ⨢ z⟧ ν = (ν x = ν y + ν z).
  Proof. reflexivity. Qed.

  Fact df_pred_mul x y z ν : ⟦x ≐ y ⨰ z⟧ ν = (ν x = ν y * ν z).
  Proof. reflexivity. Qed.

  Fact df_pred_conj f g ν : ⟦f ∧ g⟧ ν = (⟦f⟧ ν /\ ⟦g⟧ ν).
  Proof. reflexivity. Qed.

  Fact df_pred_disj f g ν : ⟦f ∨ g⟧ ν = (⟦f⟧ ν \/ ⟦g⟧ ν).
  Proof. reflexivity. Qed.

  Fact df_pred_exst f ν : ⟦∃f⟧ ν = exists n, ⟦f⟧ n·ν.
  Proof. reflexivity. Qed.


  Fact df_pred_ext f ν ω : (forall x, ν x = ω x) -> ⟦f⟧ ν <-> ⟦f⟧ ω.
  Proof.
    induction f as [ | | [] | [] f Hf g Hg | f Hf ] in ν, ω |- *; intros H; simpl.
    1-4: rewrite !H; tauto.
    1-2: rewrite Hf, Hg; auto; tauto.
    split; intros (n & Hn); exists n; revert Hn; apply Hf;
        intros []; simpl; auto.
  Qed.


  Definition der_lift ρ x := match x with 0 => 0 | S x => S (ρ x) end.

  Fixpoint df_ren ρ f :=
    match f with
      | df_cst x n => df_cst (ρ x) n
      | df_eq x y => df_eq (ρ x) (ρ y)
      | df_op o x y z => df_op o (ρ x) (ρ y) (ρ z)
      | df_bin o f g => df_bin o f⦃ρ⦄ g⦃ρ⦄
      | df_exst f => df_exst f⦃der_lift ρ⦄
    end
  where "f ⦃ ρ ⦄" := (df_ren ρ f).

  Fact df_ren_size ρ f : df_size f⦃ρ⦄ = df_size f.
  Proof. revert ρ; induction f; intros; simpl; auto; do 2 f_equal; auto. Qed.

  Fact df_ren_size_Z ρ f : df_size_Z f⦃ρ⦄ = df_size_Z f.
  Proof. do 2 rewrite df_size_Z_spec; f_equal; apply df_ren_size. Qed.


  Fact df_pred_ren f ν ρ : ⟦f⦃ρ⦄⟧ ν <-> ⟦f⟧ (fun x => ν (ρ x)).
  Proof.
    revert ν ρ; induction f as [ | | [] | [] f Hf g Hg | f Hf ]; intros ν ρ; simpl; try tauto.
    1-2: rewrite Hf, Hg; tauto.
    split; intros (n & Hn); exists n; revert Hn; rewrite Hf;
        apply df_pred_ext; intros []; simpl; auto.
  Qed.

  Fact df_pred_lift f ν : ⟦f⦃S⦄⟧ ν <-> ⟦f⟧ ν⭳.
  Proof. apply df_pred_ren. Qed.

End diophantine_logic_basics.

Local Notation "⟦ f ⟧" := (df_pred f).
Local Notation "f ⦃ ρ ⦄" := (df_ren ρ f).


Definition dio_rel R := { f | forall ν, ⟦f⟧ ν <-> R ν }.
Notation 𝔻R := dio_rel.


Section dio_rel_closure_properties.

  Implicit Types R S : (nat -> nat) -> Prop.

  Fact dio_rel_cst x n : 𝔻R (fun ν => ν x = n).
  Proof. exists (x ≐ ⌞n⌟); abstract (intro; simpl; tauto). Defined.

  Fact dio_rel_eq x y : 𝔻R (fun ν => ν x = ν y).
  Proof. exists (x ≐ y); simpl; tauto. Defined.

  Fact dio_rel_add x y z : 𝔻R (fun ν => ν x = ν y + ν z).
  Proof. exists (x ≐ y ⨢ z); abstract (intro; simpl; tauto). Defined.

  Fact dio_rel_mul x y z : 𝔻R (fun ν => ν x = ν y * ν z).
  Proof. exists (x ≐ y ⨰ z); abstract (intro; simpl; tauto). Defined.

  Fact dio_rel_conj R S : 𝔻R R -> 𝔻R S -> 𝔻R (fun ν => R ν /\ S ν).
  Proof.
    intros (fR & H1) (fS & H2); exists (fR ∧ fS).
    abstract (intro; rewrite df_pred_conj, H1, H2; tauto).
  Defined.

  Fact dio_rel_disj R S : 𝔻R R -> 𝔻R S -> 𝔻R (fun ν => R ν \/ S ν).
  Proof.
    intros (fR & H1) (fS & H2); exists (fR ∨ fS).
    abstract (intro; rewrite df_pred_disj, H1, H2; tauto).
  Defined.

  Fact dio_rel_exst (K : nat -> (nat -> nat) -> Prop) :
                 𝔻R (fun ν => K (ν 0) ν⭳) -> 𝔻R (fun ν => exists x, K x ν).
  Proof.
    intros (f & Hf); exists (∃f).
    abstract (intros ν; rewrite df_pred_exst;
      split; intros (n & Hn); exists n; revert Hn; rewrite Hf; simpl; auto).
  Defined.

  Fact dio_rel_equiv R S : (forall ν, S ν <-> R ν) -> 𝔻R R -> 𝔻R S.
  Proof.
    intros H (f & Hf); exists f.
    abstract (intro; rewrite Hf, H; tauto).
  Defined.

  Fact dio_rel_ren R ρ : 𝔻R R -> 𝔻R (fun ν => R (fun n => ν (ρ n))).
  Proof.
    intros (f & Hf); exists (f⦃ρ⦄).
    abstract (intros; rewrite df_pred_ren, Hf; tauto).
  Defined.

End dio_rel_closure_properties.



Definition dio_fun t := 𝔻R (fun ν => ν 0 = t ν⭳).
Notation 𝔻F := dio_fun.

Fact dio_fun_var x : 𝔻F (fun ν => ν x).
Proof. apply dio_rel_eq. Defined.

Fact dio_fun_cst c : 𝔻F (fun _ => c).
Proof. red; apply dio_rel_cst. Defined.

Fact dio_fun_add_im x y : 𝔻F (fun ν => ν x + ν y).
Proof. apply dio_rel_add. Defined.

Fact dio_fun_mul_im x y : 𝔻F (fun ν => ν x * ν y).
Proof. apply dio_rel_mul. Defined.

Fact dio_fun_equiv r s : (forall ν, s ν = r ν) -> 𝔻F r -> 𝔻F s.
Proof.
  intros H1; apply dio_rel_equiv.
  abstract (intro; rewrite H1; tauto).
Defined.

Fact dio_fun_ren t f : 𝔻F t -> 𝔻F (fun ν => t (fun n => ν (f n))).
Proof. apply dio_rel_ren with (ρ := der_lift f). Defined.

Section utilities_for_better_efficiency.

  Ltac dio_sym H := now (apply dio_rel_equiv with (2 := H)).

  Fact dio_rel_cst_sym x n : 𝔻R (fun ν => n = ν x).
  Proof. dio_sym (dio_rel_cst x n). Defined.

  Fact dio_rel_add_sym x y z : 𝔻R (fun ν => ν y + ν z = ν x).
  Proof. dio_sym (dio_rel_add x y z). Defined.

  Fact dio_rel_mul_sym x y z : 𝔻R (fun ν => ν y * ν z = ν x).
  Proof. dio_sym (dio_rel_mul x y z). Defined.

  Fact dio_rel_fun x t : 𝔻F t -> 𝔻R (fun ν => ν x = t ν).
  Proof.
    apply dio_rel_ren
      with (ρ := fun n =>
        match n with
          | 0 => x
          | S n => n
        end).
  Defined.

  Fact dio_rel_fun_sym x t : 𝔻F t -> 𝔻R (fun ν => t ν = ν x).
  Proof. intros H; dio_sym (dio_rel_fun x H). Defined.

End utilities_for_better_efficiency.

Fact dio_rel_fun_eq r t : 𝔻F r -> 𝔻F t -> 𝔻R (fun ν => r ν = t ν).
Proof.
  intros H1 H2; red in H1, H2.
  apply dio_rel_equiv with (R := fun ν => exists x, x = r ν /\ x = t ν).
  + abstract (intros v; split;
     [ intros ->; exists (t v); auto
     | intros (? & -> & ?); auto ]).
  + apply dio_rel_exst, dio_rel_conj; auto.
Defined.


Create HintDb dio_fun_db. Create HintDb dio_rel_db. Create HintDb dio_rel_im_db.


Ltac dio_fun_auto :=
      apply dio_fun_var
   || apply dio_fun_cst
   || apply dio_fun_add_im
   || apply dio_fun_mul_im
   || auto 7 with dio_fun_db
   .


Ltac dio_rel_immediate := auto with dio_rel_im_db.

Ltac dio_rel_eq :=
      apply dio_rel_fun
   || apply dio_rel_fun_sym
   || apply dio_rel_fun_eq
   .

Ltac dio_rel_decompose :=
      apply dio_rel_exst
   || apply dio_rel_conj
   || apply dio_rel_disj
   .


Ltac dio_rel_auto :=
   dio_rel_immediate;
   auto 7 with dio_rel_db dio_fun_db;
   ( (dio_rel_eq; dio_fun_auto)
   || (dio_rel_decompose; dio_rel_auto)
   || idtac ).


Tactic Notation "dio" "auto" :=
  match goal with
    | |- 𝔻R _ => dio_rel_auto
    | |- 𝔻F _ => dio_fun_auto
  end.


Tactic Notation "by" "dio" "equiv" uconstr(f) :=
  match goal with
    | |- 𝔻R _ => apply dio_rel_equiv with (R := f); [ | dio auto ]
    | |- 𝔻F _ => apply dio_fun_equiv with (r := f); [ | dio auto ]
  end.

Tactic Notation "dio" "by" "lemma" uconstr(f) :=
  intros; apply dio_rel_equiv with (1 := f); dio auto.


#[export] Hint Resolve dio_fun_var
             dio_fun_cst
             dio_fun_ren : dio_fun_db.

#[export] Hint Resolve dio_rel_eq
             dio_rel_cst dio_rel_cst_sym
             dio_rel_add dio_rel_add_sym
             dio_rel_mul dio_rel_mul_sym : dio_rel_im_db.


Fact dio_fun_plus r t : 𝔻F r -> 𝔻F t -> 𝔻F (fun ν => r ν + t ν).
Proof.
  intros H1 H2; red.
  by dio equiv (fun ν => exists b c, ν 0 = b + c /\ b = r ν⭳ /\ c = t ν⭳).
  abstract (intros v; split;
    [ exists (r v⭳), (t v⭳); auto
    | intros (? & ? & -> & -> & ->); auto ]).
Defined.

Fact dio_fun_mult r t : 𝔻F r -> 𝔻F t -> 𝔻F (fun ν => r ν * t ν).
Proof.
  intros H1 H2; red.
  by dio equiv (fun ν => exists b c, ν 0 = b * c /\ b = r ν⭳ /\ c = t ν⭳).
  abstract (intros v; split;
   [ exists (r v⭳), (t v⭳); auto
   | intros (? & ? & -> & -> & ->); auto ]).
Defined.

#[export] Hint Resolve dio_fun_plus dio_fun_mult : dio_fun_db.

Local Fact example_eq : 𝔻R (fun ν => ν 0 = ν 0).
Proof. dio auto. Defined.



Section True_False.


  Hint Resolve dio_rel_cst dio_rel_add : dio_rel_db.

  Fact dio_rel_True : 𝔻R (fun _ => True).
  Proof.
    by dio equiv (fun _ => exists x, x = 0).
    abstract (split; try tauto; exists 0; auto).
  Defined.

  Fact dio_rel_False : 𝔻R (fun _ => False).
  Proof.
    by dio equiv (fun _ => exists x, x = 1 /\ x = 0).
    abstract (split; try tauto; intros (? & ? & ?); lia).
  Defined.

End True_False.

#[export] Hint Resolve dio_rel_True dio_rel_False : dio_rel_db.

Fact dio_rel_le_im x y : 𝔻R (fun ν => ν x <= ν y).
Proof.
  by dio equiv (fun ν => exists a, ν y = a + ν x).
  abstract (intros v; split;
    [ intros H; exists (v y - v x); lia
    | intros (? & ->); lia ]).
Defined.

Fact dio_rel_lt_im x y : 𝔻R (fun ν => ν x < ν y).
Proof.
  by dio equiv (fun ν => exists a b c, ν y = c + ν x /\ b = 1 /\ c = a + b).
  abstract (intros v; split;
    [ intros H; exists (v y - v x -1), 1, (v y - v x); lia
    | intros (? & ? & ? & -> & -> & ->); lia ]).
Defined.

Fact dio_rel_div_im x y : 𝔻R (fun ν => divides (ν x) (ν y)).
Proof.
  by dio equiv (fun ν => exists a, ν y = a * ν x).
  unfold divides; tauto.
Defined.

#[export] Hint Resolve dio_rel_le_im
             dio_rel_lt_im
             dio_rel_div_im : dio_rel_im_db.

Fact dio_rel_le r t : 𝔻F r -> 𝔻F t -> 𝔻R (fun ν => r ν <= t ν).
Proof.
  intros H1 H2.
  by dio equiv (fun ν => exists a b, a <= b /\ a = r ν /\ b = t ν).
  abstract (intros v; split;
    [ exists (r v), (t v)
    | intros (? & ? & ? & -> & ->) ]; auto).
Defined.

Fact dio_rel_lt r t : 𝔻F r -> 𝔻F t -> 𝔻R (fun ν => r ν < t ν).
Proof.
  intros H1 H2.
  by dio equiv (fun ν => exists a b, a < b /\ a = r ν /\ b = t ν).
  abstract (intros v; split;
    [ exists (r v), (t v)
    | intros (? & ? & ? & -> & ->) ]; auto).
Defined.

#[export] Hint Resolve dio_rel_lt
             dio_rel_le : dio_rel_db.

Fact dio_rel_neq r t : 𝔻F r -> 𝔻F t -> 𝔻R (fun ν => r ν <> t ν).
Proof.
  intros H1 H2.
  by dio equiv (fun v => exists a b, (a < b \/ b < a) /\ a = r v /\ b = t v).
  abstract (intros v; split;
    [ exists (r v), (t v)
    | intros (? & ? & ?) ]; lia).
Defined.

Fact dio_rel_div r t : 𝔻F r -> 𝔻F t -> 𝔻R (fun ν => divides (r ν) (t ν)).
Proof.
  intros H1 H2.
  by dio equiv (fun v => exists a b, divides a b /\ a = r v /\ b = t v).
  abstract (intros v; split;
    [ exists (r v), (t v)
    | intros (? & ? & ? & -> & ->) ]; auto).
Defined.

#[export] Hint Resolve dio_rel_neq
             dio_rel_div : dio_rel_db.


Local Fact example_le : 𝔻R (fun ν => ν 0 <= ν 1).
Proof. dio auto. Defined.


Local Fact example_lt : 𝔻R (fun ν => ν 0 < ν 1).
Proof. dio auto. Defined.


Local Fact example_div : 𝔻R (fun ν => divides (ν 0) (ν 1)).
Proof. dio auto. Defined.


Section dio_fun_rem.


  Let rem_equiv p x r : r = rem x p
                    <-> exists x' p', x' = x /\ p' = p /\
                                 ( (p' = 0 /\ x' = r)
                                  \/ (p' <> 0 /\ r < p' /\ exists n, x' = n*p' + r) ).
  Proof.
    split.
    + intro; exists x, p; subst; msplit 2; auto.
      destruct (eq_nat_dec p 0) as [ Hp | Hp ].
      * left; split; auto; subst; rewrite rem_0; auto.
      * right; split; auto; split.
        - apply div_rem_spec2; auto.
        - exists (div x p);apply div_rem_spec1.
    + intros (? & ? & -> & -> & [ (H1 & H2) | (H1 & H2 & n & H3) ]).
      * subst; rewrite rem_0; auto.
      * symmetry; apply rem_prop with n; auto.
  Qed.

  Fact dio_fun_rem p x : 𝔻F p -> 𝔻F x -> 𝔻F (fun ν => rem (x ν) (p ν)).
  Proof.
    dio by lemma (fun v => rem_equiv (p v⭳) (x v⭳) (v 0)).
  Defined.

End dio_fun_rem.

#[export] Hint Resolve dio_fun_rem : dio_fun_db.

Local Fact dio_fun_rem_example : 𝔻F (fun ν => rem (ν 0) (ν 1)).
Proof. dio auto. Defined.


Section dio_rel_ndivides.


  Let ndivides_eq x y : ~ (divides x y) <-> x = 0 /\ y <> 0 \/ exists a b, y = a*x+b /\ 0 < b < x.
  Proof.
    split.
    + intros H.
      destruct x as [ | x ].
      * left; split; auto; contradict H; subst; apply divides_0.
      * right; exists (div y (S x)), (rem y (S x)); split.
        - apply div_rem_spec1.
        - rewrite divides_rem_eq in H.
          generalize (@div_rem_spec2 y (S x)); intros; lia.
    + intros [ (H1 & H2) | (a & b & H1 & H2) ].
      * subst; contradict H2; revert H2; apply divides_0_inv.
      * rewrite divides_rem_eq.
        rewrite (div_rem_spec1 y x) in H1.
        apply div_rem_uniq in H1; try lia.
        apply div_rem_spec2; lia.
  Qed.

  Fact dio_rel_ndivides x y : 𝔻F x -> 𝔻F y -> 𝔻R (fun ν => ~ divides (x ν) (y ν)).
  Proof.
    dio by lemma (fun v => ndivides_eq (x v) (y v)).
  Defined.

End dio_rel_ndivides.

Local Fact dio_rel_ndiv_example : 𝔻R (fun ν => ~ divides (ν 0) (ν 1)).
Proof. apply dio_rel_ndivides; dio auto. Defined.


Section dio_rel_not_divides.


  Let not_divides_eq p x : ~ divides p x <-> rem x p <> 0.
  Proof. rewrite divides_rem_eq; tauto. Qed.

  Lemma dio_rel_not_divides x p : 𝔻F x -> 𝔻F p -> 𝔻R (fun ν => ~ divides (x ν) (p ν)).
  Proof.
    dio by lemma (fun v => not_divides_eq (x v) (p v)).
  Defined.

End dio_rel_not_divides.

#[export] Hint Resolve dio_rel_not_divides : dio_rel_db.

Local Fact example_rem_strange : 𝔻R (fun ν => rem (ν 0) (ν 1) = ν 2 * ν 3).
Proof. dio auto. Defined.




Section dio_rel_compose.

  Variable (f : (nat -> nat) -> nat) (R : nat -> (nat -> nat) -> Prop).
  Hypothesis (Hf : 𝔻F f)
             (HR : 𝔻R (fun ν => R (ν 0) ν⭳)).

  Lemma dio_rel_compose : 𝔻R (fun ν => R (f ν) ν).
  Proof using HR Hf.
    by dio equiv (fun v => exists y, y = f v /\ R y v).
    abstract(intros v; split;
     [ exists (f v); auto
     | intros (? & -> & ?); auto ]).
  Defined.

End dio_rel_compose.

Section dio_fun_compose.

  Variable (f : (nat -> nat) -> nat) (Hf : 𝔻F f)
           (g : nat -> nat) (Hg : 𝔻F (fun ν => g (ν 0))).

  Lemma dio_fun_compose : 𝔻F (fun ν => g (f ν)).
  Proof using Hf Hg.
    red; by dio equiv (fun v => exists y, y = f v⭳ /\ v 0 = g y).
    abstract(intros; split;
     [ exists (f ν⭳); auto
     | intros (? & -> & ?); auto ]).
  Defined.

End dio_fun_compose.



Section multiple_exists.

  Fixpoint df_mexists n f :=
    match n with
      | 0 => f
      | S n => df_mexists n (∃f)
    end.

  Fact df_mexists_size n f : df_size (df_mexists n f) = n + df_size f.
  Proof.
    induction n as [ | n IHn ] in f |- *; auto; simpl.
    rewrite IHn; simpl; lia.
  Qed.

  Fact df_mexists_size_Z n f : df_size_Z (df_mexists n f) = (Z.of_nat n + df_size_Z f)%Z.
  Proof.
    rewrite df_size_Z_spec, df_mexists_size, Nat2Z.inj_add, df_size_Z_spec; lia.
  Qed.


  Lemma df_mexists_spec n f ν :
           ⟦df_mexists n f⟧ ν
       <-> exists π, ⟦f⟧ (fun i => if le_lt_dec n i then ν (i-n) else π i).
  Proof.
    revert f ν; induction n as [ | n IHn ]; intros f v.
    + simpl; split; [ intros H; exists (fun _ => 0) | intros (? & H) ]; revert H;
        apply df_pred_ext; intros; f_equal; lia.
    + simpl df_mexists; rewrite IHn; split; intros (pi & Hpi).
      * revert Hpi; rewrite df_pred_exst.
        intros (u & Hu).
        exists (fun i => match i with 0 => u | S i => pi i end).
        revert Hu; apply df_pred_ext.
        Opaque le_lt_dec.
        simpl; intros [ | i ].
        - replace (0-S n) with 0 by lia; auto.
        - replace (S i - S n) with (i-n) by lia.
          simpl; destruct (le_lt_dec (S n) (S i));
            destruct (le_lt_dec n i); auto; lia.
      * exists (fun i => pi (S i)).
        rewrite df_pred_exst; exists (pi 0).
        revert Hpi; apply df_pred_ext.
        intros [ | i ].
        - replace (0-S n) with 0 by lia; simpl; auto.
        - replace (S i - S n) with (i-n) by lia.
          Opaque le_lt_dec.
          simpl; destruct (le_lt_dec (S n) (S i));
            destruct (le_lt_dec n i); auto; lia.
  Qed.

End multiple_exists.


Section dio_rel_finite_conj.

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

  Definition df_true := proj1_sig dio_rel_True.

  Fact df_true_size : df_size df_true = 4.
  Proof. reflexivity. Qed.

  Fact df_true_spec ν : df_pred df_true ν <-> True.
  Proof. apply (proj2_sig dio_rel_True). Qed.

  Fixpoint df_mconj n f :=
    match n with
      | 0 => df_true
      | S n => f 0 ∧ df_mconj n f⭳
    end.

  Fact df_mconj_size n f : df_size (df_mconj n f) = 4+n+∑ n (fun i => df_size (f i)).
  Proof.
    revert f; induction n as [ | n IHn ]; intros f; simpl; auto.
    rewrite IHn; ring.
  Qed.

  Fact df_mconj_spec n f ν : df_pred (df_mconj n f) ν <-> forall i, i < n -> df_pred (f i) ν.
  Proof.
    revert f ν; induction n as [ | n IHn ]; intros f v; simpl df_mconj.
    + rewrite df_true_spec; split; auto; intros; lia.
    + rewrite df_pred_conj, IHn; split.
      * intros (? & H2) [ | i ] ?; auto; apply H2; lia.
      * intros H; split; intros; apply H; lia.
  Qed.

  Lemma dio_rel_finite_conj n (R : nat -> (nat -> nat) -> Prop) :
         (forall i, i < n -> 𝔻R (R i))
      -> 𝔻R (fun ν => forall i, i < n -> R i ν).
  Proof.
    intros H.
    apply fmap_reifier_t_default with (1 := df_true) in H.
    destruct H as (f & Hf).
    exists (df_mconj n f).
    abstract(intros v; rewrite df_mconj_spec; split;
      intros E i Hi; generalize (E _ Hi); apply Hf; trivial).
  Defined.

End dio_rel_finite_conj.