(*
   Higher-order syntax for the untyped lambda-calculus
   Venanzio Capretta and Amy Felty       
   March 2006

   see the article
   "Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq"
*)

Require Import deBruijn.

Inductive LCcon: Set :=
  LCapp: LCcon | LCabs: LCcon.

Definition lexp: Set := expr LCcon.

(* Characterization of the correct terms of the lambda-calculus. *)
Fixpoint term_check (e:lexp): bool :=
match e with
  (VAR v) => true
| (BND b) => true
| (APP (CON LCabs) (ABS e)) => term_check e
| (APP (APP (CON LCapp) e1) e2) => andb (term_check e1) (term_check e2)
| _ => false
end.

Definition tcheck: lexp -> Prop :=
  fun e => Is_true (term_check e).

(* Theorem 1 from article: Induction principle on correct expressions. *)
Lemma tcheck_ind:
  forall (P: lexp -> Prop),
    (forall v, P (VAR _ v)) ->
    (forall i, P (BND _ i)) ->
    (forall e, P e -> P (APP (CON LCabs) (ABS e))) ->
    (forall e1 e2, P e1 -> P e2 -> P (APP (APP (CON LCapp) e1) e2)) ->
  forall e, tcheck e -> P e.
Proof.
intros P Hvar Hbnd Habs Happ e'.
apply expr_star_ind with
  (con := LCcon)
  (P := fun e => tcheck e -> P e).
intro e; case e.
intros l IH h; elim h.
intros v IH h; apply Hvar.
intros i IH h; apply Hbnd.
intros a; case a.
intros l; case l.
intros b IH h; elim h.

(* ABS *)
intro b; case b.
intros l1 IH h; elim h.
intros v IH h; elim h.
intros i IH h; elim h.
intros b1 b2 IH h; elim h.
intros b1 IH h; apply Habs.
 inversion_clear IH.
 inversion_clear H2.
 apply H3; exact h.

intros v b IH h; elim h.
intros i b IH h; elim h.
intro a1; case a1.
intro l; case l.

(* APP *)
intros a2 b IH h; inversion_clear IH.
 unfold tcheck in h; simpl in h.
 apply Happ. 
 inversion_clear H0.
 apply H5.
 unfold tcheck; eapply Is_true_conj_left; apply h.
 apply H1.
 unfold tcheck; eapply Is_true_conj_right; apply h.

intros a2 b IH h; elim h.
intros v a2 b IH h; elim h.
intros i a2 b IH h; elim h.
intros a2 a3 a4 b IH h; elim h.
intros a2 a3 b IH h; elim h.
intros a2 b IH h; elim h.
intros a IH h; elim h.
Qed.

(* Definition of lambda-terms: expression with a proof of correctness. *)
Record term: Set := mk_term {
  t_expr: lexp;
  t_check: Is_true (term_check t_expr)
}.

Lemma bshift_aux_check:
  forall e, tcheck e -> forall i, tcheck (bshift_aux e i).
Proof.
intros e' h';
apply tcheck_ind with (P := fun e => forall i, tcheck (bshift_aux e i)).
(* Var *)
intros v i; red; simpl. exact I.
(* Bind *)
intros j i; red; simpl.
case (le_lt_dec i j); intro; exact I.
(* Abs *)
intros e IH i; red; simpl; apply IH.
(* App *)
intros e1 e2 IH1 IH2 i; red; simpl.
apply Is_true_conj; [apply IH1 | apply IH2].

exact h'.
Qed.

Lemma bshift_check: forall e, tcheck e -> tcheck (bshift e).
Proof.
intros e h; unfold bshift; apply bshift_aux_check; exact h.
Qed.

Lemma bsubst_check:
  forall e1 j e2, tcheck e1 -> tcheck e2 ->
                  tcheck (bsubst e1 j e2).
Proof.
intros e1 j e2 h1; generalize e2; generalize j; clear e2; clear j.
apply tcheck_ind with
  (P := fun e1 => forall j e2, tcheck e2 -> tcheck (bsubst e1 j e2)).
(* VAR *)
intros v j e2 h2; exact I.
(* BND *)
intros i j e2 h2; simpl.
case (bnd_dec i j).
intros _; exact h2.
intros _; exact I.
(* ABS *)
intros e IH j e2 h2.
change (tcheck (bsubst e (S j) (bshift e2))).
apply IH.
apply bshift_check; exact h2.
(* APP *)
intros a b IHa IHb j e2 h2.
unfold tcheck; simpl.
apply Is_true_conj.
apply IHa; exact h2.
apply IHb; exact h2.

exact h1.
Qed.

Lemma ebind_check:
  forall e, tcheck e -> forall w j, tcheck (ebind w j e).
Proof.
intros e' h'.
apply tcheck_ind with
  (P := fun e => forall w j, tcheck (ebind w j e)).
(* VAR *)
intros v w j; simpl.
case (var_dec v w).
intros _; exact I.
intros _; exact I.
(* BND *)
intros i w j; simpl.
case (bnd_dec i j).
intros _; exact I.
intros _; exact I.
(* ABS *)
unfold tcheck; intros e IH w j; simpl.
apply IH.
(* APP *)
unfold tcheck; intros e1 e2 IH1 IH2 w j; simpl.
apply Is_true_conj; [apply IH1 | apply IH2].

exact h'.
Qed.

Lemma term_check_unicity:
  forall (e:lexp)(c1 c2: tcheck e), c1=c2.
Proof.
intro e; unfold tcheck.
case (term_check e); simpl.
intros [] []; trivial.
intro c1; case c1.
Qed.

Lemma mk_term_unicity:
  forall (e1 e2:lexp), e1=e2 ->
    forall (c1:tcheck e1)(c2:tcheck e2),
      mk_term e1 c1 = mk_term e2 c2.
Proof.
intros e1 e2 Heq; rewrite Heq.
intros c1 c2; rewrite (term_check_unicity e2 c1 c2).
trivial.
Qed.

(* Lemma 2 from article. *)
Lemma term_unicity:
  forall a1 a2, (t_expr a1)=(t_expr a2) -> a1=a2.
Proof.
intros [e1 c1] [e2 c2] Heq; simpl in Heq.
apply mk_term_unicity.
exact Heq.
Qed.

(* Definition of the higher-order syntax of lambda-terms. *)

Definition Var (i:var): term := mk_term (VAR _ i) I.

Definition Bind (i:bnd): term := mk_term (BND _ i) I.

Definition tApp (a1 a2:term): term :=
  mk_term (APP (APP (CON LCapp) (t_expr a1)) (t_expr a2))
             (Is_true_conj (t_check a1) (t_check a2)).
Notation "A '@' B" := (tApp A B) (at level 23, right associativity).

Section Lambda_Abstraction.

Variable f: term -> term.

Definition nvar := newvar (t_expr (f (Bind 0))).
Definition tvar := f (Var nvar).
Definition tbind := ebind nvar 0 (t_expr tvar).

Lemma tbind_check: tcheck tbind.
Proof.
unfold tbind.
apply ebind_check.
exact (t_check (f (Var nvar))).
Qed.

(* The "function body": f applied to (Bind 0). *)
Definition tbody: term :=
  mk_term tbind tbind_check.

(* Higher-order lambda-abstraction. *)
Definition tFun: term :=
  mk_term (APP (CON LCabs) (ABS tbind)) tbind_check.

End Lambda_Abstraction.

Notation "'Fun' V , A" := (tFun (fun V => A)) (at level 20).

Lemma tbind_extensional:
  forall f1 f2: term->term,
    (forall x, f1 x = f2 x) -> tbind f1 = tbind f2.
Proof.
intros f1 f2 H.
unfold tbind; simpl.
unfold tvar; simpl.
unfold nvar; simpl.
rewrite H.
rewrite H.
trivial.
Qed.

(* The inverse operation: given a term, build the function. *)

Section Term_To_Function.

Variables (e:lexp)(h:tcheck e).
Variable x:term.

Let xe := t_expr x.
Let xh := t_check x.
Let esx := bsubst e 0 xe.

Lemma esx_check: tcheck esx.
Proof.
unfold esx.
apply bsubst_check; [exact h | exact xh].
Qed.

Definition tfun := mk_term esx esx_check.

End Term_To_Function.

Definition tapp (a:term): term -> term :=
  tfun (t_expr a) (t_check a).

(* Lemma 4 from article. *)
Lemma tbody_tapp: forall a, tbody (tapp a) = a.
Proof.
intros [e h]; apply term_unicity; unfold tbody; unfold tapp; simpl.
unfold tfun; unfold tbind; simpl.
unfold nvar; simpl.
rewrite bsubst_bnd.
rewrite ebind_bsubst_eq.
trivial.
Qed.

(* Definition 1 from article. *)

(* "Canonical form" of a function on terms. *)
Definition funt: (term -> term) -> (term -> term) :=
fun f => tapp (tbody f).

Definition is_abst (f:term->term): Prop :=
  forall x, f x = funt f x.

Inductive eval: term -> term -> Prop :=
  eval_Fun: forall e:term -> term, eval (Fun x, e x) (Fun x, e x)
| eval_App: forall (e1 e2 v:term) (e:term->term), (eval e1 (tFun e)) ->
            (is_abst e) ->
            (eval (e e2) v) -> (eval (e1 @ e2) v).

(* Lemma 5 of article. *)
Lemma Fun_inj :
  forall e1 e2:term->term, (is_abst e1) -> (is_abst e2) ->
  (tFun e1)=(tFun e2) -> forall x:term, (e1 x)=(e2 x).
Proof.
unfold is_abst; intros e1 e2 H H0 H1 x.
generalize (H x); clear H; intro H.
generalize (H0 x); clear H0; intro H0.
rewrite H; rewrite H0; clear H H0.
unfold tFun in H1.
assert (tbody e1 = tbody e2).
inversion H1.
unfold tbody.
apply term_unicity.
simpl; auto.
unfold funt; rewrite H.
reflexivity.
Qed.

(* Theorem 3 of article. *)
Theorem eval_unicity :
  forall e v1:term, (eval e v1) -> forall v2:term, (eval e v2) -> v1=v2.
Proof.
intros e v1; induction 1.
intros v2 H.
inversion H.
unfold tFun.
apply mk_term_unicity.
rewrite -> H1.
reflexivity.
intros v2 H2.
inversion H2.
apply IHeval2.
specialize term_unicity with (1:=H3); intro H9.
specialize term_unicity with (1:=H4); intro H10.
subst.
clear H3 H4.
generalize (IHeval1 (tFun e4) H5); intro H3.
generalize (Fun_inj e e4 H0 H6 H3 e2); intro H4.
rewrite -> H4; auto.
Qed.

(* Theorem 2 in article: Induction principle for lambda-terms. *)
Theorem term_induction:
  forall P:term->Prop,
    (forall v, P (Var v)) ->
    (forall i, P (Bind i)) ->
    (forall t1 t2, P t1 -> P t2 -> P (t1 @ t2)) ->
    (forall f, P (tbody (fun x => f x)) -> P (Fun x, f x)) ->
  forall t, P t.
Proof.
intros P Hv Hb Hap Hab t; case t.
intros e c; generalize c.
apply tcheck_ind with (P := fun e => forall c, P (mk_term e c)).
(* Var *)
intros v cv; rewrite term_unicity with (a2 := Var v).
apply Hv.
trivial.
(* Bind *)
intros i ci; rewrite term_unicity with (a2 := Bind i).
apply Hb.
trivial.
(* Fun *)
intros e1 IH c1; rewrite term_unicity with (a2 := Fun x, tfun e1 c1 x).
apply Hab.
rewrite term_unicity with (a2 := mk_term e1 c1).
apply IH.
simpl.
unfold tbind; unfold nvar; unfold tfun; simpl.
unfold nvar; unfold tfun; simpl.
rewrite bsubst_bnd.
exact (ebind_bsubst_eq e1 0).
simpl.
unfold tbind; unfold nvar; unfold tfun; simpl.
unfold nvar; unfold tfun; simpl.
rewrite bsubst_bnd.
rewrite ebind_bsubst_eq.
trivial.
(* @ *)
intros e1 e2 IH1 IH2 c'; simpl in c'.
rewrite term_unicity with
  (a2 := (mk_term e1 (Is_true_conj_left c')) @
         (mk_term e2 (Is_true_conj_right c'))).
apply Hap.
apply IH1.
apply IH2.
trivial.

exact c.
Qed.