Require Import L Encodings DecidableRecognisable Markov Enumerable.

Implicit Types P Q : term -> Prop.

(** * Reducability *)

Definition computable_gen X Y (xenc : X -> term) (yenc : Y -> term) f :=
  exists u, proc u /\ forall s, u (xenc s) ▷ (yenc (f s)).

Definition computable_fun f := computable_gen tenc tenc f.

Record mreducible P Q : Prop :=
  { f : term -> term ;
    f_red : forall s, P s <-> Q (f s) ;
    f_comp : computable_fun f ;
  }.
Notation "P ⪯ Q" := (mreducible P Q) (at level 40, no associativity).

Lemma mreducible_sane P Q :
  mreducible P Q <-> exists u, proc u /\ forall s, exists t, u (tenc s) ▷ tenc t /\ (P s <-> Q t).
Proof.
(* Goal: iff (mreducible P (fun _ : term => False)) (forall s : term, not (P s)) *)
  split.
  - intros [f ? (u & ? & ?)].
(* Goal: @ex term (fun u : term => and (proc u) (forall s : term, @ex term (fun t : term => and (evaluates (app u (tenc s)) (tenc t)) (iff (P s) (Q t))))) *)
    exists u. split; value.
(* Goal: forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end) *)
    intros. exists (f s). split; eauto.
  - intros (u & ? & ?). assert (forall s, exists t, u (tenc s) ▷ tenc t) as [f ?] %  L_computable_computable by firstorder.
(* Goal: mreducible P Q *)
    exists f.
(* Goal: forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end) *)
    + intros. destruct (H0 s) as (t & ? & ?).
      enough (f s = t) as ->. eassumption.
      specialize (e s). eapply tenc_inj. now rewrite <- e, <- H1. 
    + firstorder.
Qed.  

Instance mreducible_preorder : PreOrder mreducible.
Proof.
(* Goal: @PreOrder (forall _ : term, Prop) mreducible *)
  econstructor.
  - exists (fun s => s).
    + firstorder.
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
    + exists I. split; value. intros. solveeq.
  - intros P Q R [f1 H1 [u1 []]] [f2 H3 [u2 []]].
(* Goal: mreducible P R *)
    exists (fun s => f2 (f1 s)).
    + firstorder.
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
    + exists (lambda (u2 (u1 0))). split; value.
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
      intros. eapply evaluates_equiv. split; value.
(* Goal: equiv (app (lambda (app u2 (app u1 (var Datatypes.O)))) (tenc s)) (tenc (f2 (f1 s))) *)
      specialize (H0 s). specialize (H4 (f1 s)).
(* Goal: equiv (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc (lambda t))) (tenc (g (lambda t))) *)
      solveeq.
Qed.

Lemma mreducible_ext P Q P' Q' :
  (forall s, P s <-> P' s) -> (forall s, Q s <-> Q' s) -> P ⪯ Q -> P' ⪯ Q'.
Proof.
(* Goal: forall s : term, iff (Q s) (Q s) *)
  intros ? ? [f ? ?]. exists f; firstorder.
Qed.

Lemma mreducible_comp P Q :
  P ⪯ Q -> (fun s => ~ P s) ⪯ (fun s => ~ Q s).
Proof.
(* Goal: forall s : term, iff (Q s) (Q s) *)
  intros [f ? ?]. exists f; firstorder.
Qed.

Lemma mreducible_comp_conv :
  (forall P Q, (fun s => ~ P s) ⪯ (fun s => ~ Q s) -> P ⪯ Q) ->
  Markov_Eva.
Proof.
(* Goal: forall _ : forall (P Q : forall _ : term, Prop) (_ : mreducible (fun s : term => not (P s)) (fun s : term => not (Q s))), mreducible P Q, Markov_Eva *)
  intros ? ? ? ?. specialize (H eva (fun s => ~~ eva s)).
(* Goal: eva s *)
  destruct H.
  - eapply mreducible_ext with (P :=  (fun s0 : term => ~ eva s0)) (Q :=  (fun s0 : term => ~ eva s0)); try reflexivity.
(* Goal: forall s : term, iff (Q s) (Q s) *)
    firstorder.      
  - eapply f_red. intros ?. eapply H1. intros ?. now eapply f_red in H2.
Qed.

Lemma mreducible_dec P Q :
  decidable Q -> P ⪯ Q -> decidable P.
Proof.
(* Goal: forall (_ : decidable Q) (_ : mreducible P Q), decidable P *)
  intros (u & Hp & H) [f ? (v & ? & ?)].
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
  exists (lambda (u (v 0))). split; value.
  intros s. assert (lambda (u (v 0)) (tenc s) ≡ u (v (tenc s))) as -> by solveeq.
(* Goal: forall s : term, iff (Q s) (Q s) *)
  rewrite H1. firstorder.
Qed.

Lemma mreducible_red P Q s t :
  Q s -> ~ Q t -> decidable P -> P ⪯ Q.
Proof.
(* Goal: forall (_ : Q s) (_ : not (Q t)) (_ : decidable P), mreducible P Q *)
  intros ? ? ?. pose proof (decidable_dec H1) as [f ?].
(* Goal: mreducible P Q *)
  destruct H1 as (u & ? & ?).
(* Goal: mreducible P Q *)
  exists (fun x => if f x then s else t).
  - intros x. specialize (H2 x). destruct (f x); firstorder congruence.
  - exists (lambda (u 0 (tenc s) (tenc t))). split; value.
    intros x. assert ((lambda (((u 0) (tenc s)) (tenc t))) (tenc x) ≡ u (tenc x) (tenc s) (tenc t)) as -> by solveeq.
    destruct (H3 x) as [ [-> % H2 ->] | [? ->] ].
    + solveeq.
    + rewrite <- H2 in H4. destruct (f x); try congruence. solveeq.
Qed.

Lemma mreducible_recognisable P Q :
  recognisable Q -> P ⪯ Q -> recognisable P.
Proof.
(* Goal: forall (_ : recognisable Q) (_ : mreducible P Q), recognisable P *)
  intros (u & ? & ?) [f ? (v & ? & ?)].
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
  exists (lambda (u (v 0))). split; value.
  intros s. assert (lambda (u (v 0)) (tenc s) ≡ u (v (tenc s))) as -> by solveeq.
(* Goal: iff (P s) (eva (app u (app v (tenc s)))) *)
  now rewrite H2, f_red, H0.
Qed.

Lemma mreducible_full P :
  P ⪯ (fun s => True) <-> (forall s, P s).
Proof.
(* Goal: iff (mreducible P (fun _ : term => False)) (forall s : term, not (P s)) *)
  split. 
  - firstorder.
  - intros. eapply mreducible_ext with (P := fun _ => True) (Q := fun _ => True); firstorder.
Qed.

Lemma mreducible_empty P :
  P ⪯ (fun s => False) <-> (forall s, ~ P s).
Proof.
(* Goal: iff (mreducible P (fun _ : term => False)) (forall s : term, not (P s)) *)
  split. 
  - firstorder.
  - intros. eapply mreducible_ext with (P := fun _ => False) (Q := fun _ => False); firstorder. exact 0.
Qed.

Lemma eva_red :
  (fun s => eva (s (tenc s))) ⪯ eva.
Proof.
(* Goal: mreducible (fun s : term => eva (app s (tenc s))) eva *)
  exists (fun s => app s (tenc s)).
  - firstorder.
  - exists (lambda (App 0 (Q 0))). split; value.
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
    intros. eapply evaluates_equiv. split; value.
(* Goal: equiv (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc (lambda t))) (tenc (g (lambda t))) *)
    transitivity (App (tenc s) (Q (tenc s))). solveeq.
(* Goal: equiv (app (app App (tenc s)) (app Q (tenc s))) (tenc (app s (tenc s))) *)
    now rewrite Q_correct, App_correct.
Qed.

Lemma recognisable_iff P :
  recognisable P <-> P ⪯ eva.
Proof.
(* Goal: iff (mreducible P (fun _ : term => False)) (forall s : term, not (P s)) *)
  split.
  - intros (u & ? & ?).
    exists (fun x => u (tenc x)).
    + eassumption. 
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
    + exists (lambda (App (tenc u) (Q 0))). split; value.
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
      intros. eapply evaluates_equiv; split; value.
(* Goal: equiv (app (app App (tenc s)) (app Q (tenc s))) (tenc (app s (tenc s))) *)
      redL. now rewrite Q_correct, App_correct.
  - intros ?. eapply mreducible_recognisable.
(* Goal: iff (P s) (Q t) *)
(* Goal: @eq term (f s) t *)
    eapply recognisable_eva. eassumption.
Qed.

Lemma preceq_lub P Q : exists R,
    P ⪯ R /\ Q ⪯ R /\ forall R', P ⪯ R' -> Q ⪯ R' -> R ⪯ R'.
Proof.
  exists (fun s => match s with
             app 0 s => P s
           | app _ s => Q s
           | s => Q s
           end).
(* Goal: iff (mreducible P (fun _ : term => False)) (forall s : term, not (P s)) *)
  repeat split.
  - {
(* Goal: mreducible P (fun s : term => match s with | var n => Q s | app (var (Datatypes.O as n) as s0) s1 => P s1 | app (var (S n0 as n) as s0) s1 => Q s1 | app (app s2 t as s0) s1 => Q s1 | app (lambda s2 as s0) s1 => Q s1 | lambda s0 => Q s end) *)
      exists (fun s => app 0 s).
      - cbn. firstorder.
      - exists (lambda (App (tenc 0) 0)). split; value. intros.
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
        eapply evaluates_equiv; split; value.
(* Goal: equiv (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc (lambda t))) (tenc (g (lambda t))) *)
        transitivity (App (tenc 0) (tenc s)). solveeq.
(* Goal: equiv (app (app App (tenc (var (S Datatypes.O)))) (tenc s)) (tenc (app (var (S Datatypes.O)) s)) *)
        now rewrite App_correct.
    }
  - {
(* Goal: mreducible Q (fun s : term => match s with | var n => Q s | app (var (Datatypes.O as n) as s0) s1 => P s1 | app (var (S n0 as n) as s0) s1 => Q s1 | app (app s2 t as s0) s1 => Q s1 | app (lambda s2 as s0) s1 => Q s1 | lambda s0 => Q s end) *)
      exists (fun s => app 1 s).
      - cbn. firstorder.
      - exists (lambda (App (tenc 1) 0)). split; value. intros.
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
        eapply evaluates_equiv; split; value.
(* Goal: equiv (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc (lambda t))) (tenc (g (lambda t))) *)
        transitivity (App (tenc 1) (tenc s)). solveeq.
(* Goal: equiv (app (app App (tenc (var (S Datatypes.O)))) (tenc s)) (tenc (app (var (S Datatypes.O)) s)) *)
        now rewrite App_correct.
    }
  - intros D [f] [g].
    exists (fun s => match s with
             | app 0 s => f s
             | app _ s => g s
             | _ => g s
             end).
(* Goal: forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end) *)
    cbn. intros. destruct s as [ | [[] | | ] |]; cbn; firstorder.
(* Goal: computable_fun (fun s : term => match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end) *)
    destruct f_comp as (u & ? & ?), f_comp0 as (v & ? & ?).
(* Goal: computable_fun (fun s : term => match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end) *)
    exists (lambda (0 (lambda (v 1)) (lambda (lambda (1 (lambda (0 (u 1) (lambda (v 2)))) (lambda (lambda (v 2))) (lambda (v 1))))) (lambda (v 1)))).
(* Goal: and (proc (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O))))))) (forall s : term, evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s1 => f s1 | app (var (S n0 as n) as s0) s1 => g s1 | app (app s2 t as s0) s1 => g s1 | app (lambda s2 as s0) s1 => g s1 | lambda s0 => g s end)) *)
    split; value. intros. eapply evaluates_equiv; split; value.
(* Goal: equiv (app (lambda (app (app (app (var Datatypes.O) (lambda (app v (var (S Datatypes.O))))) (lambda (lambda (app (app (app (var (S Datatypes.O)) (lambda (app (app (var Datatypes.O) (app u (var (S Datatypes.O)))) (lambda (app v (var (S (S Datatypes.O)))))))) (lambda (lambda (app v (var (S (S Datatypes.O))))))) (lambda (app v (var (S Datatypes.O)))))))) (lambda (app v (var (S Datatypes.O)))))) (tenc s)) (tenc match s with | var n => g s | app (var (Datatypes.O as n) as s0) s => f s | app (var (S n0 as n) as s0) s => g s | app (app s1 t as s0) s => g s | app (lambda s1 as s0) s => g s | lambda s0 => g s end) *)
    destruct s as [ | [ [] | | ] | ] eqn:E.
    + specialize (H2 s). subst. solveeq.
    + specialize (H0 t1). subst. solveeq.
    + specialize (H2 t1). specialize (H0 t1). subst. solveeq.
    + specialize (H2 t2). specialize (H0 t2). solveeq.
    + specialize (H2 t1). solveeq.
    + specialize (H2 s). subst. solveeq.
Qed.

