(*
   Syntax for terms with deBruijn indices
   Venanzio Capretta and Amy Felty       
   March 2006

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

Require Export Arith.
Require Export Bool.
Require Export Max.

Inductive empty: Set := .

Lemma Is_true_conj_left:
  forall b1 b2, Is_true (b1 && b2) -> Is_true b1.
Proof.
intro b1; case b1; simpl; trivial.
Defined.

Implicit Arguments Is_true_conj_left [b1 b2].

Lemma Is_true_conj_right:
  forall b1 b2, Is_true (b1 && b2) -> Is_true b2.
Proof.
intros b1 b2; case b1; case b2; simpl; trivial.
Defined.

Implicit Arguments Is_true_conj_right [b1 b2].

Lemma Is_true_conj:
  forall b1 b2, Is_true b1 -> Is_true b2 -> Is_true (b1 && b2).
Proof.
intros b1 b2; case b1; case b2; intro h1; case h1; intro h2; case h2; auto.
Defined.

Implicit Arguments Is_true_conj [b1 b2].

Lemma Is_true_conj_eq:
  forall (b1 b2: bool)(h:Is_true (b1 && b2)),
    h = Is_true_conj (Is_true_conj_left  h) (Is_true_conj_right h).
Proof.
intros b1 b2; case b1; case b2; intro h; case h; auto.
Qed.

Section deBruijn.

Set Implicit Arguments.

Definition var : Set := nat.
Definition var_dec: forall v1 v2:var, {v1=v2}+{v1<>v2}
                  := eq_nat_dec.

Definition bnd : Set := nat.
Definition bnd_dec: forall b1 b2:var, {b1=b2}+{b1<>b2}
                  := eq_nat_dec.

Variable con: Set.

Inductive expr : Set :=
  CON : con -> expr
| VAR : var -> expr
| BND : bnd -> expr
| APP : expr -> expr -> expr
| ABS : expr -> expr.

(* Syntactic recursion on expressions. *)

(* The extension of a family to all subexpressions. *)
Fixpoint fam_star (P: expr->Set)(e:expr){struct e}: Set :=
match e with
  (CON c) => unit
| (VAR v) => unit
| (BND i) => unit
| (APP e1 e2) => (((P e1)*(fam_star P e1))*((P e2)*(fam_star P e2)))%type
| (ABS e') => ((P e')*(fam_star P e'))%type
end.

Fixpoint fam_star_rec
  (P:expr->Set)(H: forall e, fam_star P e -> P e)(e:expr){struct e}:
  fam_star P e :=
match e return (fam_star P e) with
  (CON c) => tt
| (VAR v) => tt
| (BND i) => tt
| (APP e1 e2) => let y1:=(fam_star_rec P H e1) in
                 let y2:=(fam_star_rec P H e2) in
                   ((H e1 y1,y1),(H e2 y2, y2))
| (ABS e') => let y':=(fam_star_rec P H e') in
                (H e' y',y')
end.

Definition expr_star_rec:
  forall (P:expr->Set), (forall e, fam_star P e -> P e) -> forall e, P e :=
fun P H e => H e (fam_star_rec P H e).

(* Syntactic induction on expressions. *)

(* Extension of a predicate to all subexpressions. *)
Inductive pred_star (P: expr->Prop): expr -> Prop:=
  pred_star_CON: forall c, pred_star P (CON c)
| pred_star_VAR: forall v, pred_star P (VAR v)
| pred_star_BND: forall i, pred_star P (BND i)
| pred_star_APP: forall e1 e2, P e1 -> pred_star P e1 ->
                               P e2 -> pred_star P e2 ->
                               pred_star P (APP e1 e2)
| pred_star_ABS: forall e', P e' -> pred_star P e' ->
                            pred_star P (ABS e').

Definition pred_star_induction:
  forall (P:expr->Prop), (forall e, pred_star P e -> P e)
                         -> forall e, pred_star P e.

intros P H e; elim e.
intro c; apply pred_star_CON.
intro v; apply pred_star_VAR.
intro b; apply pred_star_BND.
intros e1 IHe1 e2 IHe2; apply pred_star_APP.
  apply H; apply IHe1.
  apply IHe1.
  apply H; apply IHe2.
  apply IHe2.
intros e' IH; apply pred_star_ABS.
  apply H; apply IH.
  apply IH.
Qed.

Definition expr_star_ind:
  forall (P:expr->Prop), (forall e, pred_star P e -> P e) -> forall e, P e.

intros P H e; apply H.
apply pred_star_induction; exact H.
Qed.

(* Increment by 1 all dangling variables with index >=j. *)
Fixpoint bshift_aux (e:expr)(j:bnd){struct e}: expr :=
match e with
  CON c => CON c
| VAR v => VAR v
| BND i => if (le_lt_dec j i) then (BND (S i)) else (BND i)
| APP e1 e2 => APP (bshift_aux e1 j) (bshift_aux e2 j)
| ABS e' => ABS (bshift_aux e' (S j))
end.

(* Increment by 1 the indeces of all dangling variables. *)
Definition bshift (e:expr): expr := bshift_aux e 0.

(* Bound variable substitution. *)
Fixpoint bsubst (e:expr)(j:bnd)(x:expr){struct e}: expr :=
match e with
  CON c => CON c
| VAR v => VAR v
| BND i => if (bnd_dec i j) then x else (BND i)
| APP e1 e2 => APP (bsubst e1 j x) (bsubst e2 j x)
| ABS e' => ABS (bsubst e' (S j) (bshift x))
end.

(* Swappin of the free variable w and the bound variable j. *)
(* If j doesn't occur, then it just binds w to j! *)
Fixpoint ebind (w:var)(j:bnd)(e:expr){struct e}: expr :=
match e with
  CON c => CON c
| VAR v => if (var_dec v w) then (BND j) else (VAR v)
| BND i => if (bnd_dec i j) then (VAR w) else (BND i)
| APP e1 e2 => APP (ebind w j e1) (ebind w j e2)
| ABS e' => ABS (ebind w (S j) e')
end.

(* A new free variable. *)
Fixpoint newvar (e:expr): var :=
match e with
  CON c => 0
| VAR v => (S v)
| BND i => 0
| APP e1 e2 => max (newvar e1) (newvar e2)
| ABS e' => newvar e'
end.

Lemma bshift_bnd: forall i, bshift (BND i) = BND (S i).
Proof.
auto.
Qed.

Lemma bsubst_bnd:
  forall e i, bsubst e i (BND i) = e.
Proof.
intro e; elim e; auto.
intros j i; simpl.
 case (bnd_dec j i).
 intro Heq; rewrite Heq; reflexivity.
 trivial.
intros e1 IH1 e2 IH2 i; simpl.
  rewrite IH1; rewrite IH2; reflexivity.
intros e' IH i; simpl.
  simpl.
  rewrite bshift_bnd.
  rewrite (IH (S i)).
  reflexivity.
Qed.

Lemma bshift_var: forall v, bshift (VAR v) = VAR v.
Proof.
auto.
Qed.

Lemma ebind_bsubst_aux_eq:
  forall e i n, n>=(newvar e) ->
    ebind n i (bsubst e i (VAR n)) = e.
Proof.
intro e; elim e; auto.
intros v i n Hn; simpl.
 case (var_dec v n).
 simpl in Hn.
 intro Heq; rewrite Heq in Hn.
 red in Hn.
 elim (le_Sn_n n Hn).
 trivial.
intros j i n Hn; simpl.
 case (bnd_dec j i).
 intro H; simpl.
 case (var_dec n n).
 intros _;rewrite H; reflexivity. 
 intro HH; elim HH; trivial.
 intro H; simpl.
 case (bnd_dec j i).
 intro H1; elim H; exact H1.
 trivial.
intros e1 IH1 e2 IH2 i n Hn; simpl.
 rewrite IH1.
 rewrite IH2.
 reflexivity.
 red in Hn; simpl in Hn; red.
 apply le_trans with (2:=Hn). 
 apply le_max_r.
 red in Hn; simpl in Hn; red.
 apply le_trans with (2:=Hn).
 apply le_max_l.
intros e' IH i n Hn; simpl.
 rewrite bshift_var.
 rewrite IH.
 reflexivity.
 exact Hn.
Qed.

(* Lemma 1 from article. *)
Lemma ebind_bsubst_eq:
  forall e i, ebind (newvar e) i (bsubst e i (VAR (newvar e))) = e.
Proof.
intros e i; apply ebind_bsubst_aux_eq.
auto.
Qed.

Unset Implicit Arguments.

End deBruijn.