Proc

Require Export SumBool Decidability LNat.

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

Instance term_dclosedb : internalized dclosedb.
Proof.
  internalizeR.
  revert y. induction y0;intros [];recStep P; crush.
  dec;destruct nat_le_dec;try tauto; crush.
Defined.

Lemma dclosedb_spec k t : Bool.reflect (dclosed k t) (dclosedb k t).
Proof.
  revert k. induction t;intros;cbn.
  -dec;constructor. now constructor. intros H. inv H. auto.
  -specialize (IHt1 k). specialize (IHt2 k). inv IHt1;simpl.
   +inv IHt2;constructor.
    *now constructor.
    *intros C. now inv C.
   +constructor. intros C. now inv C.
  -specialize (IHt (S k)). inv IHt;constructor.
   +now constructor.
   +intros C. now inv C.
Qed.

Instance term_dclosed_dec : internalized dclosed_dec.
Proof.
  pose (f x y := to_sumbool (dclosedb x y)).
  internalizeWith f. abstract (crush;
  apply reflect_dec;
  apply dclosedb_spec).
Defined.

Instance term_closed_dec : internalized closed_dec.
Proof.
  pose (f x := decision (dclosed 0 x)).
  abstract (
  internalizeWith f; crush; destruct closed_dec,dclosed_dec;try reflexivity;
  assert (H:=closed_dcl y); exfalso;intuition).
Defined.

Instance term_lambda_dec : internalized lambda_dec.
Proof.
  pose (f x := to_sumbool (match x with lam _ => true | _ => false end)).
  internalizeWith f;crush. destruct y;crush.
Defined.

Lemma ldec_lambda : ldec lambda.
Proof.
  apply dec_ldec.
Qed.

Lemma ldec_closed : ldec closed.
Proof.
  apply dec_ldec.
Qed.

Lemma ldec_proc : ldec proc.
Proof.
  apply ldec_conj. apply ldec_closed. apply ldec_lambda.
Qed.