From Undecidability.L Require Export Datatypes.LNat Datatypes.LBool Tactics.LTactics Computability.Computability Tactics.Lbeta.

Set Default Proof Using "Type".
Section MuRecursor.

Variable P : term.
Hypothesis P_proc : proc P.
Local Hint Resolve P_proc : LProc.

Hypothesis : (n:), ( (b:bool), app P (ext n) == ext b ).

Lemma dec_P : n:, {b:bool | app P (ext n) == ext b}.
Proof using .
  intros. eapply lcomp_comp.
  -apply bool_enc_inv_correct.
  -apply .
Qed.


Section hoas.
  Import HOAS_Notations.
  Definition := Eval cbn -[enc] in (convert (λ mu P n, (P n) (!!K n) (λ Sn, P Sn) (!!(ext S) n))).
End hoas.

Import L_Notations.

Lemma mu'_proc : proc .
Proof.
  unfold ; Lproc.
Qed.


Local Hint Resolve : LProc.

Lemma mu'_n_false n: P (ext n) == ext false P (ext n) >* P (ext (S n)).
Proof using P_proc.
  intros R. apply equiv_lambda in R;[|Lproc]. recStep . unfold K. now Lsimpl.
Qed.


Lemma mu'_0_false n: ( n', n' < n P (ext n') == ext false) P (ext 0) >* P (ext n).
Proof using P_proc.
  intros H. induction n.
  -reflexivity.
  -rewrite IHn.
   +apply mu'_n_false. apply H. .
   +intros. apply H. .
Qed.


Lemma mu'_n_true (n:): P (ext n) == ext true P (ext n) == ext n.
Proof using P_proc.
  intros R. recStep . Lsimpl. rewrite R. unfold K. now Lsimpl.
Qed.


(* TODO: mu' sound*)
Lemma mu'_sound v n: proc v P (ext (n:)) == v
                     ( n', n' < n P (ext n') == ext false)
                      n0, n P (ext ) == ext true v == ext
                                 n', n' < P (ext (n':)) == ext false.
Proof using P_proc .
  intros pv. intros R. apply equiv_lambda in R;try Lproc. apply star_pow in R. destruct R as [k R]. revert n R. apply complete_induction with (x:=k);clear k;intros k. intros IH n R H.
  specialize (dec_P n).
  destruct (dec_P n) as [[] eq].
  -exists n;intuition. apply pow_star in R. apply star_equiv in R. rewrite R. now rewrite mu'_n_true.
  -assert (R':=mu'_n_false eq). apply star_pow in R'. destruct R' as [k' R'].
   destruct (parametrized_confluence uniform_confluence R R') as [x [l [u [ [ [ [ eq']]]]]]]. destruct x.
   +inv . apply IH in as [ [ [ [ ]]]].
    *exists . repeat split;try assumption;.
    *decide (l=k);[|]. subst l. assert (k'=0) by . subst k'. inv R'. apply inj_enc in . .
    *intros. decide (n'=n). subst. tauto. apply H. .
   +destruct as [? [C _]]. destruct pv as [_ [v']]. subst v. inv C.
Qed.


Lemma mu'_complete n0 : P (ext ) == ext true
                         ( n', n' < P (ext n') == ext false)
                         P (ext 0) == ext .
Proof using P_proc.
  intros. rewrite mu'_0_false with (n:=);try tauto.
  -recStep . Lsimpl. rewrite H. unfold K. now Lsimpl.
Qed.


(* the mu combinator:*)

Definition :term := lam ( #0 (ext 0)).

Lemma mu_proc : proc .
Proof.
  unfold . Lproc.
Qed.


Local Hint Resolve mu_proc : LProc.

Lemma mu_sound v : v P == v n, v = ext n P (ext n) == ext true ( n', n' < n P (ext n') == ext false).
Proof using P_proc .
  unfold . intros lv R. standardizeHypo 100. apply mu'_sound in R.
  -destruct R as [n ?]. exists n. intuition. apply unique_normal_forms;try Lproc. assumption.
  -split;[|Lproc]. apply equiv_lambda in R;auto. apply closed_star in R;Lproc.
  -intros. .
Qed.


Lemma mu_complete (n:) : P (ext n) == ext true n0:, P == ext .
Proof using P_proc .
  remember 0 as .
  assert ( n':, n'< n-(n-) P (ext n') == ext false) by (intros;).
  assert ((n-)+=n) by . remember (n-) as k. clear Heqk . induction k.
  -simpl in *. subst. intros. eexists. unfold . Lsimpl. apply mu'_complete;eauto. intros. apply H. .
  -intros. destruct (dec_P (n-S k)) as [y P'].
   destruct y.
   +eexists. unfold . Lsimpl. apply mu'_complete. exact P'. exact H.
   +apply IHk. intros. decide (n' = n - (S k)).
     *subst. exact P'.
     *apply H. .
     *assumption.
Qed.


Lemma mu_spec : converges ( P) n : , P (ext n) == ext true.
Proof using P_proc .
  split.
  - intros (? & ? & ?). eapply mu_sound in H as (? & ? & ? & ?); eauto.
  - intros []. eapply mu_complete in H as []. exists (ext ). split. eauto. eapply proc_ext.
Qed.


End MuRecursor.

#[export] Hint Resolve : LProc.
#[export] Hint Resolve mu_proc : LProc.