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).

Lemma Closed_correct s : Closed (tenc s) == true /\ closed s \/
                         Closed (tenc s) == false /\ ~ closed s.
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.

Lemma Lambda_correct s : Lambda (tenc s) == true /\ lambda s \/
                         Lambda (tenc s) == false /\ ~ lambda s.
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.