Library LC_Basis
Definitions
Inductive term := Var (n : nat) | App (s t : term) | Lam (s : term).
Coercion App : term >-> Funclass.
Implicit Types s t : term.
Definition renaming := nat -> nat.
Definition substitution := nat -> term.
Implicit Types xi zeta : renaming.
Implicit Types sigma tau : substitution.
Definition sub xi := Var o xi.
Definition upr : renaming -> renaming :=
fun xi n => match n with
| 0 => 0
| S n => S (xi n)
end.
Fixpoint apply_ren (xi : renaming) (s : term) : term :=
match s with
| Var n => Var (xi n)
| App s t => App (apply_ren xi s) (apply_ren xi t)
| Lam s => Lam (apply_ren (upr xi) s)
end.
Notation "xi '!!' s" := (apply_ren xi s) (at level 52, right associativity).
Definition up : substitution -> substitution :=
fun sigma n => match n with
| 0 => Var 0
| S n => S !! sigma n
end.
Fixpoint apply_subst (sigma : substitution) (s : term) : term :=
match s with
| Var n => sigma n
| App s t => App (apply_subst sigma s) (apply_subst sigma t)
| Lam s => Lam (apply_subst (up sigma) s)
end.
Notation "sigma '!' s" := (apply_subst sigma s) (at level 52, right associativity).
Equivalence of substitutions
Let ren_eq xi zeta s :
xi =1 zeta -> xi !! s = zeta !! s.
Proof.
intros A. revert xi zeta A.
induction s as [n |s IHs t IHt|s IHs];
intros xi zeta A; simpl; f_equal; auto.
- apply IHs. intros [|n]; simpl; f_equal; auto.
Qed.
Lemma subst_eq sigma tau s :
sigma =1 tau -> sigma ! s = tau ! s.
Proof.
intros A. revert sigma tau A.
induction s as [n |s IHs t IHt|s IHs];
intros sigma tau A; simpl; f_equal; auto.
- apply IHs. intros [|n]; simpl; f_equal; auto.
Qed.
Agreement
Lemma subst_ren xi s :
xi !! s = sub xi ! s.
Proof.
revert xi.
induction s as [n |s IHs t IHt|s IHs];
intros xi; simpl; f_equal; auto.
- rewrite IHs. apply subst_eq.
intros [|n]; reflexivity.
Qed.
Identity laws
Lemma subst_var s :
Var ! s = s.
Proof.
induction s as [n |s IHs t IHt|s IHs] ;
simpl; f_equal; auto.
- rewrite <- IHs at 2.
apply subst_eq. intros [|n]; reflexivity.
Qed.
Lemma subst_id sigma s :
sigma =1 Var -> sigma ! s = s.
Proof.
intros A. rewrite <- subst_var. apply subst_eq, A.
Qed.
Composition laws
Definition comp_subst sigma tau n := sigma ! tau n.
Arguments comp_subst sigma tau n /.
Notation "sigma '#' tau" := (comp_subst sigma tau) (at level 51).
Lemma subst_S sigma s :
sub S # sigma =1 up sigma # sub S.
Proof.
intros n. simpl. rewrite subst_ren. reflexivity.
Qed.
Let subst_comp_ren sigma xi s :
sigma ! xi !! s = sigma # sub xi ! s.
Proof.
revert sigma xi.
induction s as [n|s IHs t IHt|s IHs];
intros sigma xi ; simpl; f_equal; auto.
- rewrite IHs. apply subst_eq.
intros [|n]; reflexivity.
Qed.
Let ren_comp_subst xi sigma s :
xi !! sigma ! s = sub xi # sigma ! s.
Proof.
revert xi sigma.
induction s as [n|s IHs t IHt|s IHs]; intros xi sigma; simpl.
- apply subst_ren.
- congruence.
- f_equal. rewrite IHs. apply subst_eq.
intros [|n]; simpl. reflexivity.
rewrite subst_comp_ren.
rewrite <- subst_ren. rewrite subst_ren.
rewrite subst_comp_ren. reflexivity.
Qed.
Let up_distri sigma tau :
up (sigma # tau) =1 up sigma # up tau.
Proof.
intros [|n]; simpl. reflexivity.
rewrite subst_comp_ren, ren_comp_subst.
apply subst_eq. simpl.
symmetry; apply subst_ren.
Qed.
Lemma subst_comp sigma tau s :
sigma ! tau ! s = sigma # tau ! s.
Proof.
revert sigma tau.
induction s as [n |s IHs t IHt|s IHs];
intros sigma tau; simpl; f_equal; auto.
- rewrite IHs. apply subst_eq.
symmetry; apply up_distri.
Qed.
Beta reduction
Definition beta (t : term) : substitution :=
fun n => match n with
| 0 => t
| S n' => Var n'
end.
Inductive step : term -> term -> Prop :=
| stepB s t :
step ((Lam s) t) (beta t ! s)
| stepAL s s' t :
step s s' -> step (s t) (s' t)
| stepAR (s t t' : term) :
step t t' -> step (s t) (s t')
| stepL s s' :
step s s' -> step (Lam s) (Lam s').
Lemma subst_beta_S t s :
beta t ! S !! s = s.
Proof.
rewrite subst_ren, subst_comp. apply subst_var.
Qed.
Lemma subst_beta_com sigma t s :
sigma ! beta t ! s = beta (sigma ! t) ! up sigma ! s.
Proof.
repeat rewrite subst_comp. apply subst_eq. intros [|n]; simpl.
- reflexivity.
- now rewrite subst_beta_S.
Qed.
Lemma step_substitutive sigma s t :
step s t -> step (sigma ! s) (sigma ! t).
Proof.
intros A. revert sigma.
induction A as [s t|s s' t _ IHs | s t t' _ IHt | s s' _ IHs];
simpl; intros sigma; auto using step.
- rewrite subst_beta_com. constructor.
Qed.
Closed Terms
Inductive dclosed (d : nat) : term -> Prop :=
| dclosedV n : n < d -> dclosed d (Var n)
| dclosedA s t : dclosed d s -> dclosed d t -> dclosed d (App s t)
| dclosedL s : dclosed (S d) s -> dclosed d (Lam s).
Definition closed s := dclosed 0 s.
Arguments closed / s.
Lemma dclosed_mono d d' s :
d <= d' -> dclosed d s -> dclosed d' s.
Proof.
intros A B. revert d' A.
induction B; intros d' A; constructor; intuition; omega.
Qed.
Let subst_dclosed d sigma s :
dclosed d s -> (forall n, n < d -> sigma n = Var n) -> sigma ! s = s.
Proof.
intros A. revert sigma.
induction A; intros sigma B; simpl; f_equal; auto.
- apply IHA. intros [|n] C; simpl. reflexivity.
rewrite B; simpl. reflexivity. omega.
Qed.
Lemma subst_closed s sigma :
closed s -> sigma!s = s.
Proof.
intros A. apply (subst_dclosed A). intros n B. inv B.
Qed.
Arguments subst_closed {s sigma} _.