Require Import Arith.
From Undecidability.Shared.Libs.DLW
Require Import utils_tac utils_nat utils_decidable pos vec.
From Undecidability.MuRec
Require Import recalg ra_utils.
Set Implicit Arguments.
Set Default Proof Using "Type".
Local Notation "'⟦' f '⟧'" := (@ra_rel _ f) (at level 0).
Section ra_min_extra.
Variable (n : nat) (f : recalg (S n)) (v : vec nat n).
Hypothesis Hf : forall x, ex (⟦f⟧ (x##v)).
Theorem ra_min_extra : ex (⟦ra_min f⟧ v) <-> exists x, ⟦f⟧ (x##v) 0.
Proof using Hf.
split.
+ intros (x & H1 & H2); exists x; auto.
+ intros (x & Hx).
destruct bounded_min_d with (P := fun x => ⟦f⟧ (x##v) 0)
(Q := fun x => exists k, ⟦f⟧ (x##v) (S k))
(n := S x)
as [ (m & H1 & H2 & H3) | H1 ]; auto.
* intros y _; destruct (Hf y) as ([ | k ] & Hk); auto.
right; exists k; auto.
* exists m; split; auto.
* destruct (H1 _ (le_refl _)) as (k & Hk).
generalize (ra_rel_fun _ _ _ _ Hx Hk); discriminate.
Qed.
End ra_min_extra.
Section ra_min_extra'.
Variable (n : nat) (f : recalg (S n)) (v : vec nat n).
Hypothesis Hf : forall x, ⟦f⟧ (x##v) 0 \/ ⟦f⟧ (x##v) 1.
Theorem ra_min_ex : ex (⟦ra_min f⟧ v) <-> exists x, ⟦f⟧ (x##v) 0.
Proof using Hf.
apply ra_min_extra.
intros x; destruct (Hf x); firstorder.
Qed.
End ra_min_extra'.
Section ra_enum.
Variables (k : nat) (f : recalg (S k)).
Let a : recalg (S (S k)).
Proof.
ra root f.
+ ra arg pos0.
+ apply vec_set_pos; intros p.
ra arg (pos_nxt (pos_nxt p)).
Defined.
Let Ha v x : ⟦a⟧ v x <-> ⟦f⟧ (vec_pos v pos0##vec_tail (vec_tail v)) x.
Proof.
unfold a.
rewrite ra_rel_fix_comp; simpl.
split.
+ intros (w & H1 & H2); revert H1 H2.
vec split w with y; intros H1 H2.
generalize (H2 pos0); simpl; intros H3; subst.
eq goal H1; do 2 f_equal.
apply vec_pos_ext; intros p.
specialize (H2 (pos_nxt p)); simpl in H2.
rewrite vec_pos_map, vec_pos_set in H2; simpl in H2.
rewrite <- H2; repeat rewrite vec_pos_tail; auto.
+ vec split v with p; vec split v with q; simpl; intros H.
exists (p##v); split; auto.
intros y; analyse pos y; simpl; auto.
rewrite vec_pos_map, vec_pos_set; simpl; auto.
Qed.
Let b : recalg (S (S k)).
Proof.
ra root ra_succ.
ra arg pos1.
Defined.
Let Hb v x : ⟦b⟧ v x <-> x = S (vec_pos v pos1).
Proof.
unfold b; simpl; split.
+ intros (w & H1 & H2); revert H1 H2.
vec split w with y; vec nil w; intros H1 H2.
specialize (H2 pos0); simpl in H2; subst; auto.
+ intros H; exists (vec_pos v pos1##vec_nil); subst; split; simpl; auto.
pos split; simpl; auto.
Qed.
Opaque a b.
Let g : recalg (S (S k)).
Proof.
ra root ra_eq.
+ exact a.
+ exact b.
Defined.
Hypothesis Hf : forall v, exists x, ⟦f⟧ v x.
Let Hg v : exists e, ⟦g⟧ v e /\ (e = 0 <-> ⟦f⟧ (vec_pos v pos0##vec_tail (vec_tail v)) (S (vec_pos v pos1))).
Proof.
unfold g.
destruct (Hf (vec_pos v pos0##vec_tail (vec_tail v))) as (x & Hx).
destruct (ra_eq_rel (x##S (vec_pos v pos1)##vec_nil)) as (e & H1 & H2).
exists e; split.
+ exists (x##S (vec_pos v pos1)##vec_nil); split; auto.
intros p; analyse pos p; simpl.
* apply Ha; auto.
* apply Hb; auto.
+ simpl in H2; rewrite H2; split.
* intros; subst; auto.
* revert Hx; apply ra_rel_fun.
Qed.
Opaque g.
Definition ra_enum : recalg (S k).
Proof using a. apply ra_min, g. Defined.
Fact ra_enum_spec x v : ex (⟦ra_enum⟧ (x##v)) <-> exists n, ⟦f⟧ (n##v) (S x).
Proof using Hf.
unfold ra_enum; simpl; unfold s_min.
rewrite μ_min_of_total.
+ split.
* intros (r & Hr).
destruct (Hg (r##x##v)) as (e & H1 & H2).
simpl in H2.
exists r; apply H2.
revert H1 Hr; apply ra_rel_fun.
* intros (n & Hn); exists n.
destruct (Hg (n##x##v)) as (e & H1 & H2).
apply H2 in Hn; subst; auto.
+ intros ? ? ?; apply ra_rel_fun.
+ intros y; destruct (Hg (y##x##v)) as (e & ? & _).
exists e; auto.
Qed.
End ra_enum.