Library Partial

Require Export Nat Subst Options Seval.

Section PartialFunctions.

Variable F : term.
Hypothesis proc_F : proc F.

Hypothesis total_F : forall t n, (exists v, F (enc n) (tenc t) == some v /\ proc v) \/ F (enc n) (tenc t) == none.

Definition S' := R (.\"S'", "n", "F", "t"; ("F" "n" "t") !K (.\"x"; "S'" (!Succ "n") "F" "t") !I).

Hint Unfold S' : cbv.

Lemma S'_rec n t : S' (enc n) F (tenc t) == (F (enc n) (tenc t)) K (lam ( (lam (S' #0)) (Succ (enc n)) F (tenc t))) I.
Proof.
  crush.
Qed.

Hypothesis mono_F : forall n t v, F (enc n) (tenc t) == some v -> F (enc (S n)) (tenc t) == some v.

Lemma S'_n_Sn n t : S' (enc n) F (tenc t) == S' (enc (S n)) F (tenc t).
Proof with eauto.
  rewrite S'_rec... destruct (@total_F t n) as [[v [Hv proc_v]] | H].
  - rewrite Hv. rewrite S'_rec... rewrite (mono_F Hv). transitivity v. crush. symmetry. crush.
  - crush.
Qed.

Definition Se := S' (enc 0).

Lemma S'_0_n n t : Se F (tenc t) == S' (enc n) F (tenc t).
Proof.
  induction n.
  - reflexivity.
  - rewrite IHn. now eapply S'_n_Sn.
Qed.

Lemma Se_converges t v : Se F (tenc t) == lam v -> closed (lam v).
Proof with value; eauto using nat.
  unfold Se; generalize 0; intros n H.
  eapply equiv_lambda' in H... rewrite star_pow in H. destruct H as [n1 H].
  revert n H.
  eapply complete_induction with (x := n1). clear n1.
  intros n1 IHn n H.
  destruct (total_F t n) as [[v' H'] | HH]...
  + assert (v' = lam v). {
        destruct H'. cut (S' (enc n) F (tenc t) == lam v). intros A.
        rewrite S'_rec in A. rewrite H0 in A.
        eapply eqTrans with (s := v') in A. destruct H1 as [_ [? ?]]. subst. eapply eq_lam in A. congruence. symmetry. clear A. crush.
        eapply star_equiv. eapply star_pow. firstorder.
      }
      subst. firstorder.
  + assert (A : exists k, pow step (S k) (((S' (enc n)) F) (tenc t)) (((S' (enc (S n))) F) (tenc t))). {
        eapply powSk. unfold S'. reduce.
        transitivity ((F (enc n) (tenc t)) K (lam ( (lam (S' #0)) (Succ (enc n)) F (tenc t))) I). simpl. repeat reduction'.
        assert (F (enc n) (tenc t) >* none) by eauto using equiv_lambda.
        eapply star_trans. do 3 eapply star_trans_l...
        crush.
      }
      destruct A as [k A].
      destruct (pow_trans_lam H A) as [m [m_lt_n1 B]].
      eapply IHn...
Qed.

Lemma Se_correct' (t v : term) : proc v ->
                                    ( Se F (tenc t) == v <-> exists n, F (enc n) (tenc t) == some v ).
Proof with eauto using nat.
  intros proc_v; split...
  - unfold Se; generalize 0; intros n H.
    eapply equiv_lambda' in H... rewrite star_pow in H. destruct H as [k H].
    revert n H.
    eapply complete_induction with (x := k). clear k.
    intros k IHn n H.
    destruct (total_F t n) as [[v' H'] | HH]...
    + assert (v' = v). {
        destruct H'. cut (S' (enc n) F (tenc t) == v). intros A.
        rewrite S'_rec in A. rewrite H0 in A.
        eapply eqTrans with (s := v') in A. destruct proc_v as [_ [? ?]], H1 as [_ [? ?]]. subst. eapply eq_lam in A. congruence. symmetry. clear A. crush.
        eapply star_equiv. eapply star_pow. firstorder.
      }
      subst.
      exists n. firstorder.
    + assert (A : exists k, pow step (S k) (((S' (enc n)) F) (tenc t)) (((S' (enc (S n))) F) (tenc t))). {
        eapply powSk. unfold S'. reduce.
        transitivity ((F (enc n) (tenc t)) K (lam ( (lam (S' #0)) (Succ (enc n)) F (tenc t))) I). simpl. repeat reduction'.
        assert (F (enc n) (tenc t) >* none) by eauto using equiv_lambda.
        eapply star_trans. do 3 eapply star_trans_l...
        crush.
      }
      destruct A as [k' A].
      destruct proc_v as [_ [? ?]]. subst.
      destruct (pow_trans_lam H A) as [m [m_lt_k B]].
      eapply IHn...
    + value.
  - intros [m Hm]. rewrite S'_0_n with (n := m), S'_rec, Hm... crush.
Qed.

Corollary Se_correct (t v : term) : lambda v -> (Se F (tenc t) == v <-> exists n, F (enc n) (tenc t) == some v).
Proof.
  intros lam_v; split.
  - intros. destruct lam_v; subst.
    eapply Se_correct' in H. firstorder.
    eapply Se_converges in H. value.
  - intros [n H].
    assert (closed v). { destruct (total_F t n) as [[v' [Hv' proc_v']] | Hv'].
                         + rewrite H in Hv'. eapply some_inj in Hv'. subst; value. eassumption. value.
                         + rewrite H in Hv'. symmetry in Hv'. exfalso. eapply none_equiv_some. eassumption.
                       }
    cut (Se F (tenc t) == v). intros A; destruct lam_v; subst. eassumption.
    eapply Se_correct'. value. firstorder.
Qed.

End PartialFunctions.