# Syntactic Lambda calculus

Lambda terms modulo alpha-equivalence (and its monadic structure given by the substitution).

Set Implicit Arguments.

Require Export Misc.

## Notations

Reserved Notation "x == y" (at level 70, no associativity).
Reserved Notation "x == y :> X"
(at level 70, y at next level, no associativity).

Reserved Notation "x //= f" (at level 42, left associativity).
Reserved Notation "x //- f" (at level 42, left associativity).

Implicit Type X Y Z : Set.

## Inductive datatype of terms

Inductive term (X : Set) : Set :=
| var : Xterm X
| app : term Xterm Xterm X
| abs : term (option X) → term X.

Hint Extern 1 (_ = _ :> term _) ⇒ autorewrite with slc; simpl : slc.

Fixpoint fct X Y (f : XY) (x : term X) { struct x } : term Y :=
match x with
| var avar (f a)
| app x yapp (x //- f) (y //- f)
| abs xabs (x //- optmap f)
end
where "x //- f" := (@fct _ _ f x).

Lemma fct_fun_cong :
X (x : term X) Y (f g : XY),
( u, f u = g u) → x //- f = x //- g.
Proof.
induction x; simpl; auto.
intros. f_equal. apply IHx.
destruct u; simpl; auto.
Qed.

Lemma fct_fct :
X Y Z (f : XY) (g : YZ) (x : term X) ,
x //- f //- g = x //- (fun ug (f u)).
Proof.
intros. generalize Y Z f g; clear Y Z f g.
induction x; simpl; intros; auto.
f_equal. rewrite IHx.
apply fct_fun_cong. destruct u; reflexivity.
Qed.
Hint Rewrite fct_fct : slc.

Lemma fct_id : X (f : XX) (x : term X),
( u, f u = u) → x //- f = x.
Proof.
induction x; intros; simpl; f_equal; auto.
apply IHx.
destruct u; simpl; auto.
Qed.

Definition shift X (x : term X) : term (option X) :=
x //- @Some X.

Lemma shift_fct : X Y (f : XY) (x : term X),
shift (x //- f) = x //- fun aSome (f a).
Proof.
unfold shift. intros. rewrite fct_fct. reflexivity.
Qed.

Lemma fct_shift : X Y (f : option XY) (x : term X),
shift x //- f = x //- fun af (Some a).
Proof.
unfold shift. intros. rewrite fct_fct. reflexivity.
Qed.

Hint Rewrite shift_fct fct_shift : slc.

Definition comm
(X Y : Set) (f : Xterm Y) (x : option X) : term (option Y) :=
match x with
| Some ashift (f a)
| Nonevar None
end.

Remark comm_var : X (u : option X), comm (@var X) u = var u.
Proof.
destruct u; reflexivity.
Qed.

Fixpoint slc_bind X Y (f : Xterm Y) (x : term X) { struct x } : term Y :=
match x with
| var xf x
| app x yapp (x //= f) (y //= f)
| abs xabs (x //= comm f)
end
where "x //= f" := (@slc_bind _ _ f x).

Ltac slc :=
intros;
repeat first [ progress simpl fct
| progress simpl slc_bind
| progress autorewrite with slc ];
auto with slc.

Lemma slc_bind_fun_cong : X (x : term X) Y (f g : Xterm Y),
( u, f u = g u) → x //= f = x //= g.
Proof.
induction x; simpl; intros; auto.
f_equal. apply IHx.
destruct u; simpl; auto.
Qed.

Lemma slc_bind_var : X Y (f : Xterm Y) (x : X),
var x //= f = f x.
Proof.
reflexivity.
Qed.

Lemma slc_var_bind_match : X (x : term X) (f : Xterm X),
( u, f u = var u) → x //= f = x.
Proof.
induction x; simpl; intros; auto.
f_equal. apply IHx.
destruct u; simpl. rewrite H. reflexivity. reflexivity.
Qed.
Hint Resolve slc_var_bind_match : slc.

Lemma slc_var_bind : X (x : term X),
x //= @var X = x.
Proof.
intros. apply slc_var_bind_match. reflexivity.
Qed.

Lemma slc_fct_bind : X Y Z (f : Xterm Y) (g : YZ) (x : term X),
x //= f //- g = x //= fun uf u //- g.
Proof.
intros. generalize Y Z f g; clear Y Z f g.
induction x; simpl; intros; f_equal; auto.
rewrite IHx.
apply slc_bind_fun_cong.
destruct u; slc.
Qed.
Hint Rewrite slc_fct_bind : slc.

Lemma slc_bind_fct : X Y Z (f : XY) (g : Yterm Z) (x : term X),
x //- f //= g = x //= fun ug (f u).
Proof.
intros; generalize Y Z f g; clear Y Z f g.
induction x; simpl; intros; f_equal; auto.
rewrite IHx.
apply slc_bind_fun_cong. clear x IHx.
destruct u; reflexivity.
Qed.
Hint Rewrite slc_bind_fct : slc.

Lemma slc_shift_bind : X Y (f : Xterm Y) (x : term X),
shift (x //= f) = x //= fun ashift (f a).
Proof.
unfold shift. intros.
rewrite slc_fct_bind. reflexivity.
Qed.

Lemma slc_bind_shift : X Y (f : option Xterm Y) (x : term X),
shift x //= f = x //= fun af (Some a).
Proof.
unfold shift. intros.
rewrite slc_bind_fct. reflexivity.
Qed.

Hint Rewrite slc_shift_bind slc_bind_shift : slc.

Lemma slc_bind_bind : X Y Z
(f : Xterm Y) (g : Yterm Z) (x : term X),
x //= f //= g = x //= fun uf u //= g.
Proof.
intros. generalize Y Z f g; clear Y Z f g.
induction x; simpl; intros; f_equal; auto.
rewrite IHx.
apply slc_bind_fun_cong.
clear x IHx. destruct u; slc.
Qed.
Hint Rewrite slc_bind_bind : slc.

Lemma slc_fct_as_bind : X Y (f : XY) (x : term X),
x //- f = x //= (fun avar (f a)).
Proof.
intros. generalize Y f; clear Y f.
induction x; simpl; intros; auto.
rewrite IHx; clear IHx.
f_equal. apply slc_bind_fun_cong.
destruct u; reflexivity.
Qed.

Definition app1 X (x : term X) : term (option X) :=
app (shift x) (var None).

Lemma app1_app : X (x : term X),
app1 x = app (shift x) (var None).
Proof.
reflexivity.
Qed.

Opaque app1.

Lemma fct_app1 : X Y (f : XY) (x : term X),
app1 x //- (optmap f) = app1 (x //- f).
Proof.
intros.
do 2 rewrite app1_app.
simpl. slc.
Qed.
Hint Rewrite fct_app1 : slc.

Lemma app_as_app1 : X (x y : term X),
app x y = app1 x //= default (@var _) y.
Proof.
intros. rewrite app1_app. slc.
symmetry. slc.
Qed.

Lemma slc_bind_app1 : X Y (f : option Xterm Y) (x : term X),
app1 x //= f = app (x //= fun u : Xf (Some u)) (f None).
Proof.
intros. rewrite app1_app. simpl. slc.
Qed.

Hint Rewrite slc_bind_app1 : slc.

Inductive Beta X : term Xterm XProp :=
| beta_intro : (x1 : term (option X)) (x2 : term X),
Beta (app (abs x1) x2) (x1 //= (default (fun avar a) x2)).

Lemma beta_intro_alt : X (x1 : term (option X)) (x2 y : term X),
x1 //= (default (fun avar a) x2) = yBeta (app (abs x1) x2) y.
Proof.
intros. subst y. apply beta_intro.
Qed.

Inductive lcr (X : Set) : term Xterm XProp :=
| lcr_var : a : X, var a == var a
| lcr_app : x1 x2 y1 y2 : term X,
x1 == x2y1 == y2app x1 y1 == app x2 y2
| lcr_abs : x y : term (option X), x == yabs x == abs y
| lcr_beta : x y : term X, Beta x yx == y
| lcr_eta : x : term X, abs (app1 x) == x
| lcr_sym : x y : term X, y == xx == y
| lcr_trs : x y z : term X, lcr x ylcr y zlcr x z
where "x == y" := (@lcr _ x y).

Hint Resolve lcr_var lcr_app lcr_abs lcr_eta lcr_beta lcr_trs : slc.
Hint Immediate lcr_sym : slc.

Lemma lcr_rfl : X (x : term X), x == x.
Proof.
induction x; constructor; auto.
Qed.
Hint Resolve lcr_rfl : slc.

Lemma lcr_eq : X (x y : term X), x = yx == y.
Proof.
intros; subst y; slc.
Qed.
Hint Resolve lcr_eq : slc.

Lemma eta_fct : X Y (f : XY) (x : term X),
abs (app1 x) //- f = abs (app1 (x //- f)).
Proof.
induction x; simpl; slc.
Qed.

Lemma lcr_fct : X Y (f : XY) (x y : term X),
x == yx //- f == y //- f.
Proof.
intros. generalize Y f. clear Y f.
induction H; intros; try solve [simpl; slc].
2: eauto with slc.
destruct H.
simpl. slc.
apply lcr_beta. apply beta_intro_alt.
slc.
apply slc_bind_fun_cong.
destruct u; reflexivity.
Qed.

Hint Resolve lcr_fct : slc.

Lemma slc_eta_bind : X Y (f : Xterm Y) (x : term X),
abs (app1 x) //= f = abs (app1 (x //= f)).
Proof.
intros. simpl. slc.
rewrite app1_app. slc.
Qed.

Lemma lcr_bind_arg : X Y (f : Xterm Y) (x y : term X),
x == yx //= f == y //= f.
Proof.
intros. generalize Y f; clear Y f.
induction H; intros; try solve [simpl; slc].
3: eauto with slc.
2: rewrite slc_eta_bind; slc.
destruct H. simpl.
rewrite slc_bind_bind.
apply lcr_beta.
apply beta_intro_alt.
rewrite slc_bind_bind.
apply slc_bind_fun_cong.
destruct u; simpl; slc.
Qed.

Lemma lcr_bind_fun : X Y (f g : Xterm Y) (x : term X),
( u, f u == g u) → x //= f == x //= g.
Proof.
intros. generalize Y f g H; clear Y f g H.
induction x; intros; simpl; slc.
apply lcr_abs.
apply IHx.
destruct u; simpl; unfold shift; slc.
Qed.

Lemma lcr_bind : X Y (f g : Xterm Y) (x y : term X),
( u, f u == g u) → x == yx //= f == y //= g.
Proof.
intros.
apply lcr_trs with (x //= g).
apply lcr_bind_fun; assumption.
apply lcr_bind_arg; assumption.
Qed.

Lemma lcr_app1 : X (x y : term X),
x == yapp1 x == app1 y.
Proof.
intros. do 2 rewrite app1_app. unfold shift. slc.
Qed.