Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS
Created May 19, 2025 15:45
Show Gist options
  • Save EduardoRFS/03765241b3353511a143909b45cfb657 to your computer and use it in GitHub Desktop.
Save EduardoRFS/03765241b3353511a143909b45cfb657 to your computer and use it in GitHub Desktop.
Require Import List.
Import ListNotations.
Require Import Bool.
Require Import PeanoNat.
Require Import Lia.
Definition Index := nat.
Definition Level := nat.
Inductive Term :=
| T_var : forall (n : Index), Term
| T_apply : forall (funct : Term) (arg : Term), Term
| T_lambda : forall (body : Term), Term.
Fixpoint shift by_ depth term :=
match term with
| T_var var =>
match Nat.ltb var depth with
| true => T_var var
| false => T_var (by_ + var)
end
| T_apply funct arg =>
let funct := shift by_ depth funct in
let arg := shift by_ depth arg in
T_apply funct arg
| T_lambda body =>
let body := shift by_ (1 + depth) body in
T_lambda body
end.
Fixpoint subst to_ depth term :=
match term with
| T_var var =>
match Nat.compare var depth with
| Lt => T_var var
| Eq => shift depth 0 to_
| Gt => T_var (pred var)
end
| T_apply funct arg =>
let funct := subst to_ depth funct in
let arg := subst to_ depth arg in
T_apply funct arg
| T_lambda body =>
let body := subst to_ (1 + depth) body in
T_lambda body
end.
Fixpoint count var term :=
match term with
| T_var n =>
match Nat.eqb n var with
| true => 1
| false => 0
end
| T_apply funct arg =>
count var funct + count var arg
| T_lambda body => count (1 + var) body
end.
Fixpoint size term :=
match term with
| T_var _ => 0
| T_apply funct arg => size funct + size arg
| T_lambda body => 1 + size body
end.
Lemma shift_preserves_size term by_
: forall depth, size (shift by_ depth term) = size term.
induction term; intuition.
-
simpl; destruct (n <? depth); reflexivity.
-
rename term1 into lam; rename IHterm1 into IHlam.
rename term2 into arg; rename IHterm2 into IHarg.
specialize (IHlam depth); specialize (IHarg depth).
simpl; rewrite IHlam, IHarg.
reflexivity.
-
rename term into body; rename IHterm into IHbody.
specialize (IHbody (1 + depth)).
simpl in *; rewrite IHbody.
reflexivity.
Defined.
Lemma subst_preserves_size term to_
: forall depth, size (subst to_ depth term) =
size term + (size to_ * count depth term).
induction term; intuition.
-
simpl.
destruct (Nat.compare_spec n depth); simpl.
rewrite shift_preserves_size.
rewrite H; rewrite (Nat.eqb_refl depth); lia.
destruct (Nat.eqb_spec n depth); lia.
destruct (Nat.eqb_spec n depth); lia.
-
rename term1 into lam; rename IHterm1 into IHlam.
rename term2 into arg; rename IHterm2 into IHarg.
specialize (IHlam depth); specialize (IHarg depth).
simpl; rewrite IHlam, IHarg; lia.
-
rename term into body; rename IHterm into IHbody.
specialize (IHbody (1 + depth)).
simpl in *; rewrite IHbody; reflexivity.
Qed.
Unset Automatic Proposition Inductives.
Inductive Step : Term -> Term -> Type :=
| ST_beta : forall body arg (H : count 0 body = 1),
Step (T_apply (T_lambda body) arg) (subst arg 0 body)
| ST_app_funct : forall funct funct' arg, Step funct funct' ->
Step (T_apply funct arg) (T_apply funct' arg)
| ST_app_arg : forall funct arg arg', Step arg arg' ->
Step (T_apply funct arg) (T_apply funct arg')
| ST_lambda : forall body body', Step body body' ->
Step (T_lambda body) (T_lambda body').
Lemma step_preserve_size term term' (step : Step term term')
: 1 + size term' = size term.
induction step; simpl; first [ lia | idtac ].
rewrite subst_preserves_size; lia.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment