Require Import Encodings.
Fixpoint unenc s :=
match s with
| lambda (lambda 1) => Some 0
| lambda (lambda (app 0 s)) => match unenc s with Some n => Some (S n) | x=>x end
| _ => None
end.
Lemma unenc_correct m : (unenc (enc m)) = Some m.
Proof.
induction m; simpl; now try rewrite IHm.
Qed.
Lemma unenc_correct2 t n : unenc t = Some n -> enc n = t.
Proof.
revert n. eapply (size_induction (f := size) (p := (fun t => forall n, unenc t = Some n -> enc n = t))). clear t. intros t IHt n H.
destruct t; try now inv H.
destruct t; try now inv H.
destruct t; try now inv H.
destruct n0; try now inv H. destruct n0; try now inv H.
destruct t1; try now inv H. destruct n0; try now inv H.
simpl in H. destruct (unenc t2) eqn:A.
specialize (IHt t2).
assert (B : size t2 < size (lambda (lambda 0 t2))). simpl. omega.
eapply IHt in B.
destruct n. inv H. inversion H. subst n0.
simpl. repeat f_equal. eassumption. eassumption. inv H.
Qed.
Definition Pred : term := .\"n"; "n" !Zero (.\"n"; "n").
Hint Unfold Pred : cbv.
Lemma Pred_correct n : Pred (enc n) ≡ enc (pred n).
Proof.
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.
induction n.
- solveeq.
- transitivity (Add (enc m) (Mul (enc n) (enc m))). solveeq.
now rewrite IHn, Add_correct.
Qed.
Require Import DecidableRecognisable Enumerable.
Lemma decidable_ext p q : (forall x, p x <-> q x) -> decidable p -> decidable q.
Proof.
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.
intros (l & Hl).
revert p Hl. induction l; intros p Hl.
- eapply decidable_ext with (p := (fun x => False)). intros. rewrite Hl. intuition.
exists (lambda (F)). split; value. intros. right. intuition. solveeq.
- cbn in Hl.
destruct (IHl (fun x => x el l)) as (u & proc_u & Hu). reflexivity.
exists (lambda ((Eq 0 (tenc a)) T (u 0))). split; value.
intros s.
assert ((lambda (((Eq 0) (tenc a)) T (u 0))) (tenc s) ≡
((benc (term_eq_bool s a)) T (u (tenc s)))).
assert (H := Eq_correct' s a). solveeq.
rewrite H. clear H. unfold term_eq_bool.
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.
eapply decidable_finite. exists []. tauto.
Qed.
Lemma decidable_full : decidable (fun x => True).
Proof.
now eapply decidable_ext; [ | eapply decidable_complement, decidable_empty ].
Qed.
Theorem FirstFixedPoint (s : term) : closed s -> exists t, closed t /\ s t ≡ t.
Proof.
pose (A := .\ "x"; !s ("x" "x")).
pose (t := A A).
exists t. split;[subst t A;value|].
symmetry. cbv. solvered.
Qed.
Goal exists t, closed t /\ t ≡ (tenc t).
Proof.
destruct (SecondFixedPoint) with ( s := I) as [t [cls_t A]]. value.
exists t.
split; value. symmetry in A. eapply (eqTrans A). solvered.
Qed.
Require Import Interpreter.
Lemma computable_function u X Y (R : X -> Y -> Prop) encX encY unencY :
(forall y, unencY (encY y) = y) ->
(forall x, lam (encX x)) ->
(forall y, lam (encY y)) ->
(forall m, exists n, u (encX m) ≡ encY n /\ R m n) -> { f | forall m, R m (f m) }.
Proof.
intros HencY HlamX HlamY H.
assert (forall m, eva (u (encX m))). intros. destruct (H m) as (n & ? & ?). exists (encY n). eapply evaluates_equiv; split; value; tauto.
exists (fun m => unencY (proj1_sig (computable_eva (H0 m)))).
intros. destruct (H m) as (n & Hn & Rn).
destruct computable_eva as (v & Hv).
rewrite Hv in Hn. eapply unique_normal_forms in Hn; value.
subst. cbn. now rewrite HencY. eauto using evaluates_abst.
Qed.
Lemma computable_nat u R : (forall m, exists n, u (enc m) ≡ enc n /\ R m n) -> { f | forall m, R m (f m) }.
Proof.
eapply computable_function with (unencY := fun x => match unenc x with Some n => n | _ => 0 end); intros; value.
intros; now rewrite unenc_correct.
Qed.
Require Import Rice.
Goal forall t, ~ recognisable (fun s => ~ pi s t).
Proof.
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.
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.