# Library Proc

Require Export Decidability.

Fixpoint dcl (k : nat) (t : term) : bool :=
match t with
| #n => if decision ( n < k) then Datatypes.true else Datatypes.false
| app s t => andb (dcl k s) (dcl k t)
| lam s => dcl (S k) s
end.

Lemma dcl_dclosed k s : Datatypes.true = dcl k s -> dclosed k s.

Proof.

revert k; induction s; simpl; intros k H.

- decide (n < k).

+ econstructor.
omega.
+ discriminate H.

- eapply Bool.andb_true_eq in H.

econstructor; [eapply IHs1|eapply IHs2]; tauto.

- econstructor.
eapply IHs. eassumption.
Qed.

Lemma dclosed_dcl k s : dclosed k s -> Datatypes.true = dcl k s.

Proof.

induction 1; simpl.

- decide (n < k); try reflexivity; omega.

- rewrite <- IHdclosed1, <- IHdclosed2; reflexivity.

- congruence.

Qed.

Lemma leb_lt n m : leb (S n) m = Datatypes.true <-> n < m.

Proof.

split.

+ eapply leb_complete.

+ eapply leb_correct.

Qed.

Definition Leb := R (lam (lam (
#0 (lam true) (lam (lam (#0 false (lam (#4 #2 #0)))))))).

Lemma Leb_rec_0 m : Leb (enc 0) (enc m) == true.

Proof.

crush.

Qed.

Lemma Leb_rec_Sm_0 m : Leb (enc (S m)) (enc 0) == false.

Proof.

crush.

Qed.

Lemma Leb_rec_Sm_Sn m n : Leb (enc (S m)) (enc (S n)) == Leb (enc m) (enc n).

Proof.

crush.

Qed.

Definition benc (b : bool) := if b then true else false.

Lemma Leb_correct m n : Leb (enc m) (enc n) == benc (leb m n).

Proof.

destruct m.

- eapply Leb_rec_0.

- revert m; induction n; intros m.

+ now rewrite Leb_rec_Sm_0.

+ rewrite Leb_rec_Sm_Sn; destruct m; eauto using Leb_rec_0.

Qed.

Definition Lt := lam (lam (Leb (Succ #1) (#0))).

Hint Unfold Lt Leb : cbv.

Lemma Lt_correct n k : Lt (enc n) (enc k) == true /\ n < k \/
Lt (enc n) (enc k) == false /\ ~ n < k.

Proof.

decide (n < k) as [Hlt | Hlt].

- left.
split.
+ transitivity (Leb (Succ (enc n)) (enc k)).
crush. simpl in Hlt.
now rewrite Succ_correct, Leb_correct, leb_correct.

+ omega.

- right.
split.
+ transitivity (Leb (Succ (enc n)) (enc k)).
crush.
rewrite Succ_correct, Leb_correct.
destruct (leb (S n) k) eqn:H.
* eapply leb_complete in H.
omega.
* reflexivity.

+ eassumption.

Qed.

Definition Dclosed := R (lam (lam (lam (
#0 (lam ((Lt #0 #2) true false))
(lam (lam (Andalso (#4 #3 #1) (#4 #3 #0))))
(lam (#3 (Succ #2) #0))
)))).

Lemma Dclosed_rec_var n k : Dclosed (enc k) (tenc #n) == Lt (enc n) (enc k) true false.

Proof.

crush.

Qed.

Lemma Dclosed_rec_app k s t : Dclosed (enc k) (tenc (app s t)) ==
Andalso (Dclosed (enc k) (tenc s)) (Dclosed (enc k) (tenc t)).

Proof.

transitivity (Andalso ((lam (Dclosed #0)) (enc k) (tenc s)) ((lam (Dclosed #0)) (enc k) (tenc t))).

crush.

now rewrite !Eta; value.

Qed.

Lemma Dclosed_rec_lam k s : Dclosed (enc k) (tenc (lam s)) ==
Dclosed (enc (S k)) (tenc s).

Proof.

crush.

Qed.

Lemma Andalso_correct s t : Andalso (benc s) (benc t) == benc (s && t).

Proof.

destruct s, t; simpl; crush.

Qed.

Lemma Dclosed_correct k s : Dclosed (enc k) (tenc s) == benc (dcl k s).

Proof.

revert k; induction s; intros k.

- rewrite Dclosed_rec_var.
destruct (Lt_correct n k) as [[H Hnk] | [H Hnk]]; rewrite H; simpl; decide (n < k); try omega; crush.
- now rewrite Dclosed_rec_app, IHs1, IHs2, Andalso_correct.

- now rewrite Dclosed_rec_lam, IHs.

Qed.

Definition Closed := Dclosed (enc 0).

Proof.

destruct (dcl 0 s) eqn:H.

- left.
split.
+ unfold Closed; rewrite Dclosed_correct.
now rewrite H.
+ rewrite closed_dcl.
eapply dcl_dclosed. auto.
- right.
split.
+ unfold Closed; rewrite Dclosed_correct.
now rewrite H.
+ symmetry in H.
intros cls_s. rewrite closed_dcl in cls_s. eapply dclosed_dcl in cls_s.
rewrite <- H in cls_s.
inv cls_s.
Qed.

Lemma ldec_closed : ldec closed.

Proof.

eexists (lam (Closed #0)).

split.

- split.
intros k r. reflexivity. eexists. reflexivity.
- intros s.
destruct (Closed_correct s); [left | right];
split; try tauto; transitivity (Closed (tenc s)); try tauto; crush.

Qed.

Definition Lambda := lam (#0 (lam false) (lam (lam false)) (lam true)).

Hint Unfold Lambda : cbv.

Proof.

destruct s.

+ right.
split. crush. intros [x H]; inv H.
+ right.
split. crush. intros [x H]; inv H.
+ left.
split. crush. eexists; reflexivity.
Qed.

Lemma ldec_lambda : ldec lambda.

Proof.

exists Lambda.
split; value. intros.
assert (H := Lambda_correct s).
firstorder.
Qed.

Lemma ldec_proc : ldec proc.

Proof.

eapply ldec_conj.

- eapply ldec_closed.

- eapply ldec_lambda.

Qed.