From Undecidability.L Require Import DecidableRecognisable InterpreterResults.
Open Scope list_scope.
Implicit Types s t : term.

(** * Enumerable classes *)

(** ** Definition of enumerable classes *)
Definition enumerable p := exists u, proc u /\ (forall n, u(enc n) ≡ none \/ exists s, u (enc n) ≡ oenc (Some s) /\ p s) /\ forall s, p s -> exists n, u (enc n) ≡ oenc (Some s).

(** ** Enumerable classes are recognisable *)

(** *** Equality of encoded terms *)

Definition Eq := rho (.\ "Eq", "s", "t"; "s" (.\"n";        "t" (.\"m"; !EqN "n" "m") !(lambda (lambda F)) !(lambda F))
                                           (.\"s1", "s2"; "t" !(lambda F) (.\"t1","t2"; ("Eq" "s1" "t1") ("Eq" "s2" "t2") !F) !(lambda F))
                                           (.\"s1";       "t" !(lambda F) !(lambda (lambda F)) (.\"t1"; "Eq" "s1" "t1")) ).
Hint Unfold Eq : cbv.

Definition term_eq_bool s t := if decision (s = t) then true else false.

Lemma Eq_correct' s t :
  Eq (tenc s) (tenc t) ≡ benc (term_eq_bool s t).
Proof with try solveeq.
  revert t; induction s; intros.
  + destruct t; [ | solveeq..].
    transitivity (EqN (enc n) (enc n0)). solveeq. rewrite EqN_correct.
    unfold term_eq_bool. destruct _. inv e.
    now rewrite <- beq_nat_refl. assert (n <> n0) by firstorder congruence.
    rewrite <- Nat.eqb_neq in H. now rewrite H.
  + destruct t; [ solveeq | | solveeq].
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    transitivity ((Eq (tenc s1) (tenc t1)) (Eq (tenc s2) (tenc t2)) F). solveeq.
    rewrite IHs1, IHs2. 
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    unfold term_eq_bool. destruct *; try congruence; solveeq.
  + destruct t; [ solveeq.. | ].
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    transitivity (Eq (tenc s) (tenc t)). solveeq.
    rewrite IHs.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    unfold term_eq_bool. destruct *; try congruence; solveeq.
Qed.

Lemma Eq_correct s t :
      (s  = t -> Eq (tenc s) (tenc t) ≡ T )
  /\ ( s <> t -> Eq (tenc s) (tenc t) ≡ F ).
Proof.
  intuition; rewrite Eq_correct';
  unfold term_eq_bool; destruct _; now try congruence.
Qed.

(** *** Search using Choose *)

Section Fix_f.

  Variable u : term.
  Hypothesis proc_u : proc u.
  Hypothesis total_u : forall n, u (enc n) ≡ none \/ exists s, u (enc n) ≡ oenc (Some s).

  Definition Re : term := Eval cbv in
        .\ "s"; !C (.\ "n"; !u "n" (.\ "t"; !Eq "s" "t") !F).

  Lemma Re_proc :
    proc Re.
  Proof.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
    value.
  Qed.

  Lemma H_rec n s : ((lambda (((u 0) (lambda ((Eq (tenc s)) 0))) F)) (enc n) ≡ u (enc n) (lambda (Eq (tenc s) 0)) F).
  Proof.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    solveeq.
  Qed.

  Lemma H_proc s : proc (.\ "n"; !u "n" (.\ "t"; !Eq !(tenc s) "t") !F).
  Proof.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
    value.
  Qed.

  Lemma H_test s : test (.\ "n"; !u "n" (.\ "t"; !Eq !(tenc s) "t") !F).
  Proof.
(* Goal: forall n : nat, or (equiv (app (lambda (app some (app u (var O)))) (enc n)) none) (@ex term (fun s : term => and (equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) (@ex nat (fun n0 : nat => @eq term (f n0) s)))) *)
    intros n. cbn. rewrite H_rec.
(* Goal: or (evaluates (app (app (app u (enc n)) (lambda (app (app Eq (tenc s)) (var O)))) F) T) (evaluates (app (app (app u (enc n)) (lambda (app (app Eq (tenc s)) (var O)))) F) F) *)
    destruct (total_u n) as [ | [] ].
    + rewrite H. right. solveeq.
    + rewrite H, some_correct_r; value.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
      assert (lambda (Eq (tenc s) 0) (tenc x) ≡ Eq (tenc s) (tenc x)) by solveeq.
(* Goal: @eq (option term) (@nth term n (L (S n))) (@Some term s) *)
      rewrite H0. decide (s = x).
      * eapply Eq_correct in e. rewrite e. left. econstructor.
(* Goal: or (equiv (app (lambda (app some (app u (var O)))) (enc n)) none) (@ex term (fun s : term => and (equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) (@ex nat (fun n : nat => @eq term (f n) s)))) *)
      * eapply Eq_correct in n0. rewrite n0. right. econstructor.
  Qed.

  Lemma Re_sound s : eva (Re (tenc s)) -> exists n, u (enc n) ≡ oenc (Some s).
  Proof.
(* Goal: forall (_ : proc u) (_ : forall n : nat, evaluates (app u (enc n)) (tenc (f n))), recognisable (fun t : term => @ex nat (fun n : nat => @eq term (f n) t)) *)
    intros.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    assert (Re (tenc s) ≡ C (lambda (u 0 (lambda (Eq (tenc s) 0)) F))) by solveeq.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
    rewrite H0 in H. eapply C_sound in H as [n H]; value.
    - exists n. unfold satis in H. destruct (total_u n) as [ | []].
      + cbn. rewrite H_rec, H1, none_correct in H; value. inv H.
      + rewrite H_rec, H1, some_correct_r in H; value.
(* Goal: equiv (app u (enc n)) (oenc (@Some term s)) *)
        assert (lambda (Eq (tenc s) 0) (tenc x) ≡ Eq (tenc s) (tenc x)) by (clear; solveeq).        
(* Goal: equiv (app u (enc n)) (oenc (@Some term s)) *)
        rewrite H2 in H.
(* Goal: or (evaluates (app (app Eq (tenc s)) (tenc x)) T) (evaluates (app (app Eq (tenc s)) (tenc x)) F) *)
        decide (s = x).
        * now subst.
        * eapply Eq_correct in n0. rewrite n0 in H. inv H.
(* Goal: forall n : nat, or (equiv (app (lambda (app some (app u (var O)))) (enc n)) none) (@ex term (fun s : term => and (equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) (@ex nat (fun n0 : nat => @eq term (f n0) s)))) *)
    - intros n. rewrite H_rec. destruct (total_u n) as [ | [] ].
      + rewrite H1. right. solveeq.
      + rewrite H1, some_correct_r; value.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
        assert (lambda (Eq (tenc s) 0) (tenc x) ≡ Eq (tenc s) (tenc x)) by solveeq.
(* Goal: or (evaluates (app (app Eq (tenc s)) (tenc x)) T) (evaluates (app (app Eq (tenc s)) (tenc x)) F) *)
        rewrite H2. decide (s = x).
        * eapply Eq_correct in e. rewrite e. left. econstructor.
(* Goal: or (equiv (app (lambda (app some (app u (var O)))) (enc n)) none) (@ex term (fun s : term => and (equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) (@ex nat (fun n : nat => @eq term (f n) s)))) *)
        * eapply Eq_correct in n0. rewrite n0. right. econstructor.
  Qed.

  Lemma Re_complete n s : u (enc n) ≡ oenc (Some s) -> eva (Re (tenc s)).
  Proof.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    intros. assert (Re (tenc s) ≡ C (lambda (u 0 (lambda (Eq (tenc s) 0)) F))) by solveeq.
(* Goal: @eq (option term) (@nth term n (L (S n))) (@Some term s) *)
    rewrite H0. edestruct (C_complete (n := n) (H_proc s) (H_test s)).
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
    - unfold satis. cbn. rewrite H_rec, H. eapply evaluates_equiv; split; value.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
      transitivity (Eq (tenc s) (tenc s)). solveeq.
(* Goal: or (evaluates (app (app (app u (enc n)) (lambda (app (app Eq (tenc s)) (var O)))) F) T) (evaluates (app (app (app u (enc n)) (lambda (app (app Eq (tenc s)) (var O)))) F) F) *)
      edestruct (Eq_correct). now rewrite H1.
    - destruct H1; eauto.
  Qed.

End Fix_f.

Lemma enumerable_recognisable p : enumerable p -> recognisable p.
Proof.
  intros [v [f_cls [f_total f_enum]]].  
  pose (u := (lambda (Re v 0))).
  assert (Hu : forall s, u (tenc s) ≡ Re v (tenc s)) by (intros; solveeq).
(* Goal: enumerable (fun _ : term => True) *)
  exists u.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
  split. value. intuition.
  - rewrite Hu. eapply f_enum in H as []. eapply Re_complete.
    + value.
    + firstorder.
    + eauto.
  - rewrite Hu in H. eapply Re_sound in H as [n H].
    destruct (f_total n).
    + rewrite H in H0. replace none with (oenc None) in H0. eapply oenc_inj in H0. inv H0.
(* Goal: equiv (@onatenc term tenc (@nth term n (L (S n)))) (oenc (R n)) *)
(* Goal: forall x : term, proc (tenc x) *)
      reflexivity.
    + destruct H0 as [? [? ?]]. rewrite H0 in H. eapply oenc_inj in H. inv H. eassumption.
    + value.
    + firstorder.
Qed.

(** ** The class of all terms is enumerable *)

Lemma R_enumerates (R : nat -> option term) (u : term) :
  proc u -> (forall s, exists n, R n = Some s) -> (forall n, u (enc n) ▷ oenc (R n)) ->
  enumerable (fun s => True).
Proof.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
  intros Hp HR Hu. exists u. repeat split; eauto; value.
  - intros . destruct (R n) eqn:E.
    + right. exists t. rewrite Hu, E. eauto.
    + left. rewrite Hu, E. reflexivity.
(* Goal: forall (_ : proc u) (_ : forall n : nat, evaluates (app u (enc n)) (tenc (f n))), recognisable (fun t : term => @ex nat (fun n : nat => @eq term (f n) t)) *)
  - intros. destruct (HR s) as [n H0].
(* Goal: @ex nat (fun n : nat => equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) *)
    exists n. rewrite (Hu n), H0. eauto.
Qed.

Fixpoint L n :=
  match n with
  | 0 => [ ]
  | S n => L n ++ var n :: map_pro L.app (L n) (L n) ++ map lambda (L n)
  end.

Lemma length_L n : |L n| >= n.
Proof.
(* Goal: equiv (app (app Nth (Encodings.enc (S n))) (lenc (@cons X x A))) (onatenc (@nth X (S n) (@cons X x A))) *)
  induction n; cbn.
  - omega.
(* Goal: equiv (app (app Nth (Encodings.enc (S n))) (lenc (@cons X x A))) (onatenc (@nth X (S n) (@cons X x A))) *)
  - rewrite app_length. cbn. omega.
Qed.

Lemma L_exists n : exists s, nth n (L (S n)) = Some s.
Proof.
(* Goal: @ex term (fun s : term => @eq (option term) (@nth term n (L (S n))) (@Some term s)) *)
  edestruct nth_length with (A := L (S n)) (n := n).
  + eapply length_L. 
  + eauto.
Qed.

Lemma L_cum m n : m <= n -> exists A, L n = L m ++ A.
Proof.
(* Goal: forall _ : le m n, @ex (list term) (fun A : list term => @eq (list term) (L n) (@Datatypes.app term (L m) A)) *)
  induction 1.
  - exists []. now simpl_list.
(* Goal: equiv (app (app Nth (Encodings.enc (S n))) (lenc (@cons X x A))) (onatenc (@nth X (S n) (@cons X x A))) *)
  - cbn. destruct IHle as [A ->].
    rewrite <- app_assoc. eauto.
Qed.  

Lemma nth_app_l X (x : X) n A B :
  nth n A = Some x -> nth n (A ++ B) = Some x.
Proof.
(* Goal: forall _ : @eq (option X) (@nth X n A) (@Some X x), @eq (option X) (@nth X n (@Datatypes.app X A B)) (@Some X x) *)
  revert n.
(* Goal: forall (n : nat) (_ : @eq (option X) (@nth X n A) (@Some X x)), @eq (option X) (@nth X n (@Datatypes.app X A B)) (@Some X x) *)
  induction A as [|y A IH]; cbn; intros k H.
  - destruct k; discriminate H.
  - destruct k as [|k]; cbn in *. exact H.
(* Goal: @eq (option X) (@nth X k (@Datatypes.app X A B)) (@Some X x) *)
    apply IH, H.
Qed.

Lemma L_inv m n k s t :
  nth k (L m) = Some s -> nth k (L n) = Some t -> s = t.
Proof.
  intros H1 H2.
(* Goal: le (beta s2) (Init.Nat.add (beta s1) (beta s2)) *)
  assert (m <= n \/ n <= m) as [H3|H3] by omega.
  - destruct (L_cum H3) as [A ?]. rewrite H in *.
    eapply nth_app_l in H1. rewrite H1 in H2. now inv H2.
  - destruct (L_cum H3) as [A ?]. rewrite H in *.
    eapply nth_app_l in H2. rewrite H2 in H1. now inv H1.
Qed.

Definition R n := nth n (L (S n)).

Fixpoint beta s :=
  match s with
  | var n => S n
  | app s t => S (beta s + beta t)
  | lambda s => S (beta s)
  end.

Lemma L_el s m n : s el L m -> m <= n -> s el L n.
Proof.
(* Goal: forall (_ : proc u) (_ : forall n : nat, evaluates (app u (enc n)) (tenc (f n))), recognisable (fun t : term => @ex nat (fun n : nat => @eq term (f n) t)) *)
  intros. induction H0.
  - eauto.
(* Goal: equiv (app (app Nth (Encodings.enc (S n))) (lenc (@cons X x A))) (onatenc (@nth X (S n) (@cons X x A))) *)
  - cbn. eauto.
Qed.
  
Lemma L_beta s : s el L (beta s).
Proof.
(* Goal: equiv (app (app Nth (Encodings.enc (S n))) (lenc (@cons X x A))) (onatenc (@nth X (S n) (@cons X x A))) *)
  induction s; cbn.
  - eauto.
(* Goal: equiv (app (app Nth (Encodings.enc (S n))) (lenc (@cons X x A))) (onatenc (@nth X (S n) (@cons X x A))) *)
  - rewrite !in_app_iff. cbn. rewrite in_app_iff.
(* Goal: or (equiv (app (lambda (app some (app u (var O)))) (enc n)) none) (@ex term (fun s : term => and (equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) (@ex nat (fun n : nat => @eq term (f n) s)))) *)
    do 2 right. left. eapply map_pro_in. repeat eexists; eauto.
    + eapply L_el; eauto. omega.
    + eapply L_el; eauto. omega.
(* Goal: equiv (app (app Nth (Encodings.enc (S n))) (lenc (@cons X x A))) (onatenc (@nth X (S n) (@cons X x A))) *)
  - rewrite !in_app_iff. cbn. rewrite in_app_iff.
(* Goal: or (equiv (app (lambda (app some (app u (var O)))) (enc n)) none) (@ex term (fun s : term => and (equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) (@ex nat (fun n : nat => @eq term (f n) s)))) *)
    do 3 right. eapply in_map_iff. eauto.
Qed.
  
Lemma R_surjective s : exists n, R n = Some s.
Proof.
(* Goal: @ex nat (fun n : nat => @eq (option term) (R n) (@Some term s)) *)
  destruct (el_pos _ (L_beta s)) as [n ? % pos_nth].
(* Goal: @ex nat (fun n : nat => equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) *)
  unfold R. exists n. destruct (L_exists n) as [? ?].
(* Goal: @eq (option term) (@nth term n (L (S n))) (@Some term s) *)
  rewrite H0. f_equal. eapply L_inv; eauto.
Qed.

(** ** Procedural realisation of enumeration *)

(** ** Some list procedures *)

Section Fix_X.

  Variable X : Type.
  Variable enc : X -> term.
  Hypothesis enc_proc : (forall x, proc (enc x)).

  Fixpoint lenc (A : list X) :=
    match A with
    | nil => lambda (lambda 1)
    | a::A => lambda(lambda (0 (enc a) (lenc A)))
    end.

  Definition Nil : term := .\ "n", "c"; "n".
  Definition Cons: term := .\ "a", "A", "n", "c"; "c" "a" "A".

  Lemma lenc_proc A : proc (lenc A).
  Proof.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
    induction A; value.
  Qed.

  Hint Resolve lenc_proc : cbv.

  Lemma Cons_correct a A : Cons (enc a) (lenc A) ≡ lenc(a::A).
  Proof.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    solveeq.
  Qed.

  Definition Append := rho (.\ "app", "A", "B";
                            "A" "B" (.\"a", "A"; !Cons "a" ("app" "A" "B"))).

  Hint Unfold Append : cbv.

  Lemma Append_correct A B : Append (lenc A) (lenc B) ≡ lenc(A ++ B).
  Proof.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    induction A; solveeq.
  Qed.

  Definition sim (F : term) f := proc F /\ forall x, F (enc x) ≡ (enc (f x)).

  Definition Map := rho (.\ "map", "F", "A";
                         "A" !Nil (.\"a", "A"; !Cons ("F" "a") ("map" "F" "A"))).

  Hint Unfold sim Map : cbv.

  Lemma Map_correct f A F : sim F f ->
                            Map F (lenc A) ≡ lenc(map f A).
  Proof.
(* Goal: forall _ : sim2 F f, equiv (app (app (app Map_pro F) (lenc A)) (lenc B)) (lenc (@map_pro X X X f A B)) *)
    intros [[? ?] ?].
(* Goal: equiv (app (app (app Map_pro F) (lenc A)) (lenc B)) (lenc (@map_pro X X X f A B)) *)
    induction A.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    - solveeq.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    - specialize (H1 a). solveeq.
  Qed.

  Definition sim2 (F : term) f := proc F /\ forall x y, F (enc x) (enc y) ≡ (enc (f x y)).

  Definition Map_pro := rho (.\ "map_pro", "f", "A", "B";
                               "A" !Nil (.\"a", "A"; !Append ("map_pro" "f" "A" "B") (!Map (.\"y" ; "f" "a" "y") "B"))).

  Goal proc Map_pro.
  Proof.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
    value.
  Qed.

  Hint Unfold sim2 Map_pro : cbv.

  Lemma Map_pro_correct f A B F : sim2 F f ->
                            Map_pro F (lenc A) (lenc B) ≡ lenc(map_pro f A B).
  Proof.
(* Goal: forall _ : sim2 F f, equiv (app (app (app Map_pro F) (lenc A)) (lenc B)) (lenc (@map_pro X X X f A B)) *)
    intros [[? ?] ?].
(* Goal: equiv (app (app (app Map_pro F) (lenc A)) (lenc B)) (lenc (@map_pro X X X f A B)) *)
    induction A.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    - solveeq.
    - transitivity (Append (Map_pro F (lenc A) (lenc B)) (Map (lambda (F (enc a) 0)) (lenc B))). solvered.
(* Goal: equiv (@onatenc term tenc (@nth term n (L (S n)))) (oenc (R n)) *)
(* Goal: forall x : term, proc (tenc x) *)
      rewrite IHA, Map_correct with (f := f a), Append_correct. reflexivity.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
      split; value. intros. specialize (H1 a x). solveeq.      
  Qed.

  Definition Nth := rho (.\ "nth", "n", "A";
                         "n" ("A" !none (.\ "a", "A"; !some "a"))
                             (.\"n"; ("A" !none (.\"a", "A"; "nth" "n" "A"))) ).

  Definition onatenc x := match x with None => none | Some x => (lambda(lambda(1 (enc x)))) end.

  Lemma Nth_correct A n : Nth (Encodings.enc n) (lenc A) ≡ onatenc(nth n A).
  Proof.
(* Goal: equiv (app (app Nth (Encodings.enc n)) (lenc A)) (onatenc (@nth X n A)) *)
    revert A; induction n; intros A.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    - destruct A; solveeq.
    - destruct A.
      + solveeq.
      + cbn. rewrite <- IHn. solveeq.
  Qed.

End Fix_X.

Definition L_term := rho (.\ "L", "n";
                            "n" !Nil (.\ "n"; !Append ("L" "n") (!Cons (!Var "n") (!Append (!Map_pro !App ("L" "n") ("L" "n")) (!Map !Lam ("L" "n")))))).

Lemma L_term_correct n : L_term (enc n) ≡ lenc tenc (L n).
Proof.
(* Goal: equiv (app L_term (enc n)) (@lenc term tenc (L n)) *)
  induction n.
  - solvered.
  - transitivity (Append (L_term (enc n)) (Cons (Var (enc n)) (Append (Map_pro App (L_term (enc n)) (L_term (enc n))) (Map Lam (L_term (enc n)))))). solvered.
    rewrite IHn, Map_correct with (f := lambda), Map_pro_correct with (f := app), Append_correct, Var_correct, Cons_correct, Append_correct;
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
      intros; value.
    + reflexivity.
    + split. value. exact App_correct.
    + split. value. exact Lam_correct.
Qed.

Definition OfNat : term := .\ "n" ; !Nth "n" (!L_term (!Succ ("n"))).

Lemma OfNat_correct n : OfNat (enc n) ≡ oenc (R n).
Proof.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
  transitivity (Nth (enc n) (L_term (Succ (enc n)))). solveeq.
(* Goal: equiv (@onatenc term tenc (@nth term n (L (S n)))) (oenc (R n)) *)
(* Goal: forall x : term, proc (tenc x) *)
  rewrite Succ_correct, L_term_correct, Nth_correct. reflexivity.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
  intros; value.
Qed.
  
Lemma enumerable_all : enumerable (fun s => True).
Proof.
  eapply R_enumerates with (u := OfNat).
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
  - value.
  - eapply R_surjective.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
  - intros. rewrite OfNat_correct. eapply evaluates_equiv; split; now value.
Qed.

(** ** Recognisable classes are enumerable *)
                                                                
Theorem recognisable_enumerable p : recognisable p -> enumerable p.
Proof.
(* Goal: forall _ : recognisable p, enumerable p *)
  destruct enumerable_all as (Enum & pE & TE & HE).  
(* Goal: forall _ : recognisable p, enumerable p *)
  intros [u [proc_u Hu]]. 

(* Goal: enumerable p *)
  pose (v := (.\ "n"; !Enum "n" (.\ "u"; "u" !(lambda none) (.\ "t", "s"; "t" (.\ "n"; !E "n" (!App !(tenc u) (!Q "s")) (.\ "_"; !some "s") !none) !(lambda (lambda none)) !(lambda none)) !(lambda none)) !none) : term).
  cbn -[none App Q some] in v.
(* Goal: enumerable p *)
  assert (Hv : forall n, v (enc n) ≡ Enum (enc n) (.\ "u"; "u" !(lambda none) (.\ "t", "s"; "t" (.\ "n"; !E "n" (!App !(tenc u) (!Q "s")) (.\ "_"; !some "s") !none) !(lambda (lambda none)) !(lambda none)) !(lambda none)) !none) by (intros; solvered).
(* Goal: enumerable p *)
  exists v.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
  repeat split; value.
(* Goal: forall n : nat, or (equiv (app (lambda (app some (app u (var O)))) (enc n)) none) (@ex term (fun s : term => and (equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) (@ex nat (fun n0 : nat => @eq term (f n0) s)))) *)
  - intros n. destruct (TE n) as [ | H]; try  destruct H as ([ | t1 s | ] & H & _).
    + left. rewrite Hv, H. solveeq.
    + left. rewrite Hv, H. solveeq.
    + destruct t1 as [ m | |].
      * destruct (eval m (u (tenc s))) eqn:He.
(* Goal: or (equiv (app (lambda (app some (app u (var O)))) (enc n)) none) (@ex term (fun s : term => and (equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) (@ex nat (fun n : nat => @eq term (f n) s)))) *)
        -- right. exists s. rewrite Hv, H, some_correct_r. split.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
           transitivity (E (enc m) (App (tenc u) (Q (tenc s))) (lambda (some (tenc s))) none). solveeq.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
           rewrite Q_correct, App_correct, E_correct, He. transitivity (some (tenc s)). solveeq.
(* Goal: equiv (app some (tenc s)) (oenc (@Some term s)) *)
(* Goal: p s *)
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
           now rewrite some_correct.
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
           eapply Hu. eapply eval_evaluates in He. firstorder. value. now value.
(* Goal: or (equiv (app v (enc n)) none) (@ex term (fun s : term => and (equiv (app v (enc n)) (oenc (@Some term s))) (p s))) *)
        -- left. rewrite Hv, H, some_correct_r. 
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
           transitivity (E (enc m) (App (tenc u) (Q (tenc s))) (lambda (some (tenc s))) none). solveeq.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
           rewrite Q_correct, App_correct, E_correct, He. solveeq. value. now value.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
      * left. rewrite Hv, H. solveeq.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
      * left. rewrite Hv, H. solveeq.
    + left. rewrite Hv, H. solveeq.
  - intros s [s' [n H] % evaluates_eval] % Hu.
(* Goal: True *)
(* Goal: @ex nat (fun n : nat => equiv (app v (enc n)) (oenc (@Some term s))) *)
    destruct (HE (n s)). eauto. exists x.
(* Goal: equiv (app v (enc x)) (oenc (@Some term s)) *)
    rewrite Hv, H0.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    transitivity (E (enc n) (App (tenc u) (Q (tenc s))) (lambda (some (tenc s))) none). solveeq.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    rewrite Q_correct, App_correct, E_correct, H. solveeq.
Qed.

Lemma recognisable_range_total f u : proc u -> (forall n, u (enc n) ▷ tenc (f n)) -> recognisable (fun t => exists n, f n = t).
Proof.
(* Goal: forall (_ : proc u) (_ : forall n : nat, evaluates (app u (enc n)) (tenc (f n))), recognisable (fun t : term => @ex nat (fun n : nat => @eq term (f n) t)) *)
  intros. eapply enumerable_recognisable. 
(* Goal: proc (convert (blambda (String (Ascii.Ascii true false true false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true false true false true true true false) EmptyString)) (bter (lambda none))) (blambda (String (Ascii.Ascii false false true false true true true false) EmptyString) (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii false false true false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bapp (bapp (bter App) (bter (tenc u))) (bapp (bter Q) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (blambda (String (Ascii.Ascii true true true true true false true false) EmptyString) (bapp (bter some) (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString))))) (bter none)))) (bter (lambda (lambda none)))) (bter (lambda none)))))) (bter (lambda none))))) *)
(* Goal: proc (convert (bter none)) *)
  exists (lambda (some (u 0))). repeat split; value.
(* Goal: forall n : nat, or (equiv (app (lambda (app some (app u (var O)))) (enc n)) none) (@ex term (fun s : term => and (equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term s))) (@ex nat (fun n0 : nat => @eq term (f n0) s)))) *)
  - intros n. right. exists (f n); split; eauto.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
    specialize (H0 n). solveeq.
(* Goal: equiv (app (lambda (app some (app u (var O)))) (enc n)) (oenc (@Some term (f n))) *)
  - intros s [n]. exists n. specialize (H0 n). subst. solveeq.
Qed.
