(** * Additional results not mentioned in the paper *)

From Undecidability.L Require Import Encodings.

(** ** Natural numbers *)

(** *** Predecessor and multiplication *)

Definition Pred : term := .\"n"; "n" !Zero (.\"n"; "n").

Hint Unfold Pred : cbv.

Lemma Pred_correct n : Pred (enc n) ≡ enc (pred n).
Proof.
(* Goal: equiv (app Pred (enc n)) (enc (Init.Nat.pred n)) *)
  destruct n; solveeq.
Qed.

Definition Mul := rho (.\ "Mul", "m", "n"; "m" !Zero (.\ "m"; !Add "n" ("Mul" "m" "n"))).

Lemma Mul_correct m n :
  Mul (enc n) (enc m) ≡ enc (n * m).
Proof.
(* Goal: equiv (app (app Mul (enc n)) (enc m)) (enc (Init.Nat.mul n m)) *)
  induction n.
  - solveeq.
  - transitivity (Add (enc m) (Mul (enc n) (enc m))). solveeq.
(* Goal: equiv (app (app Add (enc m)) (app (app Mul (enc n)) (enc m))) (enc (Init.Nat.mul (S n) m)) *)
    now rewrite IHn, Add_correct.
Qed.

(** ** Trivial and finite classes are decidable *)

From Undecidability.L Require Import DecidableRecognisable Enumerable.

Lemma decidable_ext p q : (forall x, p x <-> q x) -> decidable p -> decidable q.
Proof.
(* Goal: forall (_ : forall x : term, iff (p x) (q x)) (_ : decidable p), decidable q *)
  intros H [u Hu].
  exists u. intuition. intros ?. now rewrite <- H.
Qed.

Definition finite p := exists l : list term, forall x, p x <-> x el l.

Lemma decidable_finite p : finite p -> decidable p.
Proof.
(* Goal: forall _ : finite p, decidable p *)
  intros (l & Hl).
(* Goal: decidable p *)
  revert p Hl. induction l; intros p Hl.
  - eapply decidable_ext with (p := (fun x => False)). intros. rewrite Hl. intuition.
(* Goal: evaluates (app (lambda I) (tenc t)) I *)
    exists (lambda (F)). split; value. intros. right. intuition. solveeq.
  - cbn in Hl.
(* Goal: decidable p *)
    destruct (IHl (fun x => x el l)) as (u & proc_u & Hu). reflexivity.
(* Goal: and (closed t) (equiv t (tenc t)) *)
    exists (lambda ((Eq 0 (tenc a)) T (u 0))). split; value.
(* Goal: decides (lambda (app (app (app (app Eq (var O)) (tenc a)) T) (app u (var O)))) p *)
    intros s.
    assert ((lambda (((Eq 0) (tenc a)) T (u 0))) (tenc s) ≡
            ((benc (term_eq_bool s a)) T (u (tenc s)))).
(* Goal: evaluates (app (lambda I) (tenc t)) I *)
    assert (H := Eq_correct' s a). solveeq. 
(* Goal: or (and (p s) (evaluates (app (lambda (app (app (app (app Eq (var O)) (tenc a)) T) (app u (var O)))) (tenc s)) T)) (and (not (p s)) (evaluates (app (lambda (app (app (app (app Eq (var O)) (tenc a)) T) (app u (var O)))) (tenc s)) F)) *)
    rewrite H. clear H. unfold term_eq_bool.
(* Goal: or (and (p s) (evaluates (app (app (benc (if @decision (@eq term s a) (term_eq_dec s a) then true else false)) T) (app u (tenc s))) T)) (and (not (p s)) (evaluates (app (app (benc (if @decision (@eq term s a) (term_eq_dec s a) then true else false)) T) (app u (tenc s))) F)) *)
    decide (s = a).
    + destruct (Hu a) as [ [] | [] ]; left; ( split; [ firstorder | subst; solveeq]).
    + destruct (Hu s) as [ [] | [] ]; [ left | right ] ; ( split ; [firstorder | solveeq] ).
Qed.

Lemma decidable_empty : decidable (fun x => False).
Proof.
(* Goal: decidable (fun _ : term => False) *)
  eapply decidable_finite. exists []. tauto.
Qed.

Lemma decidable_full : decidable (fun x => True).
Proof.
(* Goal: decidable (fun _ : term => True) *)
  now eapply decidable_ext; [ | eapply decidable_complement, decidable_empty ].
Qed.

(** ** First fixed-point theorem *)

Theorem FirstFixedPoint (s : term) :  closed s -> exists t, closed t /\ s t ≡ t.
Proof.
(* Goal: forall _ : closed s, @ex term (fun t : term => and (closed t) (equiv (app s t) t)) *)
  pose (A := .\ "x"; !s ("x" "x")).
(* Goal: forall _ : closed s, @ex term (fun t : term => and (closed t) (equiv (app s t) t)) *)
  pose (t := A A).
(* Goal: @ex term (fun t : term => and (closed t) (equiv t (tenc t))) *)
  exists t. split;[subst t A;value|].
(* Goal: equiv (app s (convert t)) (convert t) *)
  symmetry. cbv. solvered.
Qed.

Goal exists t, closed t /\ t ≡ (tenc t).
Proof.
(* Goal: @ex term (fun t : term => and (closed t) (equiv t (tenc t))) *)
  destruct (SecondFixedPoint) with ( s := I) as [t [cls_t A]]. value.
(* Goal: @ex term (fun t : term => and (closed t) (equiv t (tenc t))) *)
  exists t.
(* Goal: and (closed t) (equiv t (tenc t)) *)
  split; value. symmetry in A. eapply (eqTrans A). solvered.
Qed.

(** ** Some corollaries of Rice's theorem *)

Require Import Rice.

Goal forall t, ~ recognisable (fun s => ~ pi s t).
Proof.
(* Goal: forall t : term, not (recognisable (fun s : term => not (pi s t))) *)
  intros t. eapply Rice_pi.
  - hnf; intuition. eapply H1. intros. rewrite H2. eauto.
  - exists (lambda I). repeat split; value. intros H; eapply H. exists I. solveeq.
  - intros A. eapply (D_pi t); eauto.
Qed.

Goal ~ recognisable (fun s => exists t, ~ pi s t).
Proof.
(* Goal: not (recognisable (fun s : term => not (pi s t))) *)
  eapply Rice_pi.
  - hnf; intuition. destruct H1 as [u H1].
    exists u. now rewrite <- H2.
  - exists (lambda I). split; value. intros [? H]. eapply H. eexists; eapply evaluates_equiv; split;[|eexists;reflexivity]. solvered.
  - exists I. now rewrite D_pi.
Qed.

(** * Lines of code for major results *)

(** 
    Our development consists of 1850 lines of code (630 spec and 1220 proofs), 100 of them needed to 
    implement L-specific automation. We do not count the Standard library-like Preliminaries.v.

    We list the lines of code we need for some major results, always considering exactly the parts of
    the development needed to establish the result. 
    
    - Definition of L: 400 lines
    - Rice's Theorem, including properties of decidable/recognisable classes: 900 lines
    - Step-indexed interpreter: 900 lines
    - Totality: 1200 lines
    - Parallel or, including Post's theorem and closure of recognisable classes under union: 120
    - Equivalence of enumerability and recognisability: 1500
    - Markov: 1650

*)
