From Undecidability.Shared.Libs.DLW
  Require Import utils finite pos vec.

From Undecidability.MuRec
  Require Import recalg ra_bs recursor minimizer ra_ca.

Set Implicit Arguments.

Set Default Proof Using "Type".

Notation "[| f |]" := (@ra_rel _ f) (at level 0).

Section soundness_and_completeness.


  Lemma ra_ca_inc_bs k (f : recalg k) v x : (exists n, [f;v] -[n>> x) -> [f;v] ~~> x.
  Proof.
    intros (n & H); revert H.
    induction 1 as [ n v | v | v
                   | k v p
                   | k i f gj v n w q x H1 IH1 H2 IH2
                   | k f g v n x H1 IH2
                   | k f g v n p x q y H1 IH1 H2 IH2
                   | k f v p n w q H1 IH1 H2 IH2 ]; try (constructor; auto; fail).
    apply in_ra_bs_comp with w; auto.
    apply in_ra_bs_rec_S with x; auto.
    apply in_ra_bs_min with w; auto.
  Qed.


  Lemma ra_bs_inc_rel k (f : recalg k) v x : [f;v] ~~> x -> [|f|] v x.
  Proof.
    induction 1 as [ n v | v | v
                   | k v p
                   | k i f gj v w x H1 IH1 H2
                   | k f g v n x H1
                   | k f g v n x y H1 IH1 H2
                   | k f v n w H1 IH1 H2 ]; try reflexivity.
    exists w; split; auto; intros; rewrite vec_pos_set; auto.
    red; unfold s_rec; simpl; auto.
    rewrite ra_rel_fix_rec in IH1 |- *; unfold s_rec in IH1 |- *.
    simpl in IH1 |- *; exists x; auto.
    rewrite ra_rel_fix_min; unfold s_min; split; auto.
    intros y Hy.
    exists (vec_pos w (nat2pos Hy)).
    generalize (IH1 (nat2pos Hy)).
    rewrite pos2nat_nat2pos.
    eqgoal; do 2 f_equal.
  Qed.


  Lemma ra_rel_inc_ca k (f : recalg k) v x : [|f|] v x -> exists n, [f;v] -[n>> x.
  Proof.
    revert v x; induction f as [ k | | | k p | k i f gj Hf Hgj
                               | k f g Hf Hg
                               | ]; intros v x.
    rewrite ra_rel_fix_cst; unfold s_cst; intros []; exists 1; constructor.
    rewrite ra_rel_fix_zero; unfold s_zero; intro; subst; exists 1; constructor.
    rewrite ra_rel_fix_succ; unfold s_succ; intro; subst; exists 1; constructor.
    rewrite ra_rel_fix_proj; unfold s_proj; intros []; exists 1; constructor.

    rewrite ra_rel_fix_comp; unfold s_comp; intros (w & H1 & H2).
    apply Hf in H1; destruct H1 as (n & H1).
    assert (forall p, exists n, [vec_pos gj p;v] -[n>> vec_pos w p) as H3.
      intros p; specialize (H2 p); rewrite vec_pos_map in H2; auto.
    apply vec_reif in H3.
    destruct H3 as (m & Hm).
    exists (1+n+vec_sum m).
    apply in_ra_ca_comp with (2 := H1); auto.

    rewrite ra_rel_fix_rec; unfold s_rec.
    rewrite (vec_head_tail v); simpl; generalize (vec_head v) (vec_tail v).
    clear v; intros i v.
    revert x; induction i as [ | i IHi ]; intros x; simpl.
    intros H; apply Hf in H; destruct H as (n & Hn); exists (S n); constructor; auto.
    intros (y & H1 & H2).
    apply IHi in H1; destruct H1 as (n & Hn).
    apply Hg in H2; destruct H2 as (m & Hm).
    exists (1+n+m); apply in_ra_ca_rec_S with (1 := Hn); auto.

    rewrite ra_rel_fix_min; unfold s_min; intros (H1 & H2).
    assert (forall (p : pos x), exists r, [|f|] (pos2nat p##v) (S r)) as H3.
      intros p; apply (H2 _ (pos2nat_prop p)).
    apply vec_reif in H3.
    destruct H3 as (w & Hw).
    assert (forall p, exists n, [f;pos2nat p##v] -[n>> S (vec_pos w p)) as H3.
      intros p; apply IHf, Hw.
    apply vec_reif in H3.
    destruct H3 as (m & Hm).
    apply IHf in H1.
    destruct H1 as (n & Hn).
    exists (1+n+vec_sum m).
    apply in_ra_ca_min with (1 := Hm); auto.
  Qed.


  Hint Resolve ra_ca_inc_bs ra_bs_inc_rel ra_rel_inc_ca : core.

  Theorem ra_bs_correct k (f : recalg k) v x : [|f|] v x <-> [f;v] ~~> x.
  Proof. split; auto. Qed.

  Theorem ra_ca_correct k (f : recalg k) v x : [|f|] v x <-> exists n, [f;v] -[n>> x.
  Proof. split; auto. Qed.

End soundness_and_completeness.