Created
May 19, 2025 15:45
-
-
Save EduardoRFS/03765241b3353511a143909b45cfb657 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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