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.