From Undecidability.L Require Export L.
Require Import Coq.Logic.ConstructiveEpsilon.

Lemma eval_converges s t : eval s t -> converges s.
Proof.
  intros [v [R lv]]. exists t. rewrite v. subst. split. reflexivity. auto.
Qed.

Hint Resolve eval_converges.

Inductive seval : nat -> term -> term -> Prop :=
| sevalR n s : seval n (lam s) (lam s)
| sevalS n s t u v w :
    seval n s (lam u) -> seval n t (lam v) -> seval n (subst u 0 (lam v)) w -> seval (S n) (s t) w.

Local Notation "s '⇓' n t" := (seval n s t) (at level 51).

Lemma seval_eval n s t : seval n s t -> eval s t.
Proof with eauto using star_trans, star_trans_l, star_trans_r.
  intros. induction H as [ | n s t u v w _ [IHe1 _] _ [IHe2 _] _ [IHe3 lam_w]].
  - repeat econstructor.
  - split...
    transitivity ((lam u) t)...
    transitivity ((lam u) (lam v))... now rewrite stepApp.
Qed.

Hint Resolve seval_eval.

Lemma seval_S n s t : seval n s t -> seval (S n) s t.
Proof.
  induction 1; eauto using seval.
Qed.

Lemma eval_step s s' t n : s ≻ s' -> seval n s' t -> seval (S n) s t.
Proof with eauto using seval_S, seval.
  intros H; revert n t; induction H; intros n u A...
  - inv A...
  - inv A...
Qed.

Lemma eval_seval s t : eval s t -> exists n, seval n s t.
Proof.
  intros [A B]. induction A.
  - destruct B. subst. eauto using seval.
  - destruct (IHA B) as [k C]. eauto using seval, eval_step.
    Grab Existential Variables. exact 0.
Qed.

Fixpoint eva (n : nat) (u : term) :=
  match u with
  | var n => None
  | lam s => Some (lam s)
  | app s t => match n with
           | 0 => None
           | S n => match eva n s, eva n t with
                    | Some (lam s), Some t => eva n (subst s 0 t)
                    | _ , _ => None
                    end
            end
  end.

Lemma eva_lam n s t : eva n s = Some t -> lambda t.
Proof.
  revert s t; induction n; intros s t H;
  destruct s; try inv H; eauto.
  destruct (eva n s1) eqn:Hs1; try now inv H1.
  destruct t0; try inv H1.
  destruct (eva n s2); try inv H0.
  eapply IHn in H1. eassumption.
Qed.

Lemma eva_seval n s t : eva n s = Some t -> seval n s t.
Proof.
  revert s t. induction n; intros s t H;
  destruct s; try now inv H; eauto using seval.
  destruct (eva n s1) eqn:Hs1; try now (simpl in H; rewrite Hs1 in H; inv H).
  destruct t0; try now (simpl in H; rewrite Hs1 in H; inv H).
  destruct (eva n s2) eqn:Hs2; try now (simpl in H; rewrite Hs1, Hs2 in H; inv H).
  destruct (eva_lam Hs2); subst t1.
  econstructor; eauto. eapply IHn. simpl in H. rewrite Hs1, Hs2 in H. eassumption.
Qed.

Lemma seval_eva n s t : seval n s t -> eva n s = Some t.
Proof.
  induction 1.
  - destruct n; reflexivity.
  - simpl. rewrite IHseval1, IHseval2. eassumption.
Qed.

Lemma equiv_eva s t : lambda t -> s == t -> exists n, eva n s = Some t.
Proof.
  intros lt A. cut (eval s t). intros H.
  eapply eval_seval in H. destruct H as [n H]. eapply seval_eva in H.
  eauto. eauto using equiv_lambda.
Qed.

Lemma eva_equiv s s' n : eva n s = Some s' -> s == s'.
Proof.
  intros H. eapply eva_seval in H. eapply seval_eval in H. destruct H. eapply star_equiv.
  eassumption.
Qed.

Lemma eva_n_Sn n s t : eva n s = Some t -> eva (S n) s = Some t.
Proof.
  intros H. eapply eva_seval in H. eapply seval_eva.
  eapply seval_S. eassumption.
Qed.

Lemma eva_Sn_n n s : eva (S n) s = None -> eva n s = None.
Proof.
  intros H; destruct s, n; try reflexivity; try now inv H.
  simpl. destruct (eva n s1) eqn:Hs1, (eva n s2) eqn:Hs2.
  - destruct t; try reflexivity.
    assert (Hs' : eva (S n) s1 = Some (lam t)) by eauto using eva_n_Sn.
    assert (Ht' : eva (S n) s2 = Some (t0)) by eauto using eva_n_Sn.
    destruct (eva n (subst t 0 t0)) eqn:Ht; try reflexivity.
    assert (H' : eva (S n) (subst t 0 t0) = Some t1) by eauto using eva_n_Sn.
    rewrite <- H. change (Some t1 = match eva (S n) s1, eva (S n) s2 with
                    | Some (lam s), Some t => eva (S n) (subst s 0 t)
                    | _ , _ => None
                    end). rewrite Hs', Ht'. rewrite H'. reflexivity.

  - destruct t; reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

Lemma eproc_equiv s t: eval s (lam t) <-> s == (lam t).
Proof.
  split; intros H; eauto using equiv_lambda.
  destruct (eval_seval H) as [n A]. destruct H; eauto.
Qed.

Lemma Omega_diverges s : ~ (Omega == lam s).
Proof.
  intros H. eapply eproc_equiv in H.
  eapply eval_seval in H. destruct H. inv H.
  inv H2. inv H4. induction n.
  - inv H6.
  - inv H6. decide (0 = 0); try now tauto. inv H2. inv H3. simpl in *. decide (0 = 0); try now tauto.
Qed.

Lemma app_converges (s t : term) : (converges (s t)) -> converges s /\ converges t.
Proof.
  intros H. split;
  destruct H as [u [H lu]];inv lu;
  eapply eproc_equiv in H; eapply eval_seval in H; destruct H as [n H]; inv H;
  [exists (lam u) | exists (lam v)];(split;[|auto]); eapply eproc_equiv; eapply seval_eval; eassumption.
Qed.


Require Import Coq.Logic.ConstructiveEpsilon.
Definition cChoice := constructive_indefinite_ground_description_nat_Acc.

Fixpoint stepf (s : term) : list term :=
  match s with
  | (lam _) => []
  | var x => []
  | app (lam s) (lam t) => [subst s 0 (lam t)]
  | app s t => map (fun x => app x t) (stepf s) ++ map (fun x => app s x) (stepf t)
  end.

Ltac stepf_tac :=
  match goal with
  | [ H : app _ _ ≻ ?t |- ?P ] => inv H
  | [ H : var _ ≻ ?t |- ?P ] => inv H
  | [ H : lam _ ≻ ?t |- ?P ] => inv H

  | [ H : exists x, _ |- _ ] => destruct H
  | [ H : _ /\ _ |- _ ] => destruct H
  end + subst.

Lemma stepf_spec s t : t el stepf s <-> s ≻ t.
Proof.
  revert t; induction s; intros; try now (firstorder; inv H). cbn.
  destruct s1, s2.
  all:cbn - [stepf].
  all:try rewrite !in_app_iff;try rewrite !in_map_iff.
  1-8:setoid_rewrite IHs1.
  1-8:try setoid_rewrite IHs2.
  all:intuition idtac.
  all:repeat stepf_tac.
  all:eauto using step.
Qed.

Fixpoint stepn (n : nat) s : list term :=
  match n with
  | 0 => [s]
  | S n => flat_map (stepn n) (stepf s)
  end.

Lemma stepn_spec n s t : t el stepn n s <-> s >(n) t.
Proof.
  revert s t; induction n; intros.
  - cbn. firstorder.
  - cbn. rewrite in_flat_map. firstorder; exists x; firstorder using stepf_spec.
Qed.

Lemma informative_eval s t: eval s t -> {l | s >(l) t}.
Proof.
  intros H. destruct H. eapply star_pow in H. apply cChoice; eauto.
  intros. eapply dec_transfer.
  eapply stepn_spec. exact _.
Qed.

Lemma informative_eval2 s : (exists t, eval s t) -> {t | eval s t}.
Proof.
  intros H.
  edestruct cChoice with (P:=fun n => exists t, t el stepn n s /\ lambda t).
  -intros.
   decide (exists t, t el stepn n s /\ lambda t). all:eauto.
  -destruct H as (?&H&?). eapply star_pow in H as [? H].
   eapply stepn_spec in H. eauto.
  -apply list_cc in e. 2:eauto.
   destruct e as (?&H'&?). unfold eval. apply stepn_spec,pow_star in H'. eauto.
Qed.