# User:Rsimmons/CR2

 This is Literate TwelfCode: hereStatus: %% OK %% Output: here.

## Syntax

```exp : type.  %name exp E.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.```

When we use this %block, it expresses that we can be working in a context with arbitrary expression variables.

```%block exps : block {x: exp}.
%worlds (exps) (exp).```

## Reduction

We can reduce under binders and reduce both sides of an application "in parallel." If we have a β-redex (λx.ea) eb, then after reducing ea (with x free) to ea' (with x free) and reducing eb to eb', we can return [eb'/x]ea', the substitution of eb' into ea'. When we introduce a new variable, we always add in the fact that it can evaluate to itself.

The %block exps_id explicitly states that we will be reducing in a setting with free variables, with the invariant that every variable is added with the invariant that it can evaluate to itself.

```reduce : exp -> exp -> type.
%mode reduce +E -E'.

%block exps_id : block {x: exp}{d: reduce x x}.

reduce/lam : reduce (lam E) (lam E')
<- ({x:exp} reduce x x -> reduce (E x) (E' x)).

reduce/app : reduce (app E1 E2) (app E1' E2')
<- reduce E1 E1'
<- reduce E2 E2'.

reduce/beta : reduce (app (lam E1) E2) (E1' E2')
<- ({x:exp} reduce x x -> reduce (E1 x) (E1' x))
<- reduce E2 E2'.

%worlds (exps_id) (reduce _ _).
%total E (reduce E _).```

## Substitution

The substitution theorem says that if we have a term e with x free that reduces to e' (with x still free) and earg reduces to e'arg, then [earg/x]e reduces to [e'arg/x]e'.

The proof is by induction on the structure of the term with the free variable.

```substitute
: ({x: exp} reduce x x -> reduce (E x) (E' x))
-> reduce Earg Earg'
-> reduce (E Earg) (E' Earg') -> type.
%mode substitute +D +Darg -D'.```

We actually need to think about what block this theorem will take place in. The "variable case" of our lemma is one where the first argument is [x: exp] [idx: red x x] y, where y is not equal to x. In this case, we will need to insert into the context the lemma that, if

```%block exp_subst
: block {x: exp}{idx: reduce x x}
{subst
: {z: exp}{z': exp}{red: reduce z z'} substitute ([_][_] idx) red idx}.

- : substitute
([x] [idx: reduce x x] idx)
(D : reduce Earg Earg') D.

- : substitute
([x] [idx: reduce x x]
reduce/lam
(D x idx : {y} reduce y y -> reduce (E x y) (E' x y)))
(Darg: reduce Earg Earg')
(reduce/lam D'
: reduce (lam ([y] (E Earg) y)) (lam ([y] (E' Earg') y)))
<- ({y} {idy: reduce y y}
({z}{z'}{red_z: reduce z z'} substitute ([_] [_] idy) red_z idy)
-> substitute ([x] [idx: reduce x x] D x idx y idy) Darg
(D' y idy : reduce (E Earg y) (E' Earg' y))).

- : substitute
([x] [idx: reduce x x]
reduce/app
(Db x idx : reduce (Eb x) (Eb' x))
(Da x idx : reduce (Ea x) (Ea' x)))
(Darg: reduce Earg Earg')
(reduce/app Db' Da'
: reduce (app (Ea Earg) (Eb Earg)) (app (Ea' Earg') (Eb' Earg')))
<- substitute Da Darg (Da': reduce (Ea Earg) (Ea' Earg'))
<- substitute Db Darg (Db': reduce (Eb Earg) (Eb' Earg')).

- : substitute
([x] [idx: reduce x x]
reduce/beta
(Db x idx : reduce (Eb x) (Eb' x))
(Da x idx : {y} reduce y y -> reduce (Ea x y) (Ea' x y)))
(Darg: reduce Earg Earg')
(reduce/beta Db' Da'
: reduce (app (lam (Ea Earg)) (Eb Earg)) ((Ea' Earg') (Eb' Earg')))
<- ({y} {idy: reduce y y}
({z}{z'}{red_z: reduce z z'} substitute ([_] [_] idy) red_z idy)
-> substitute ([x] [idx: reduce x x] Da x idx y idy) Darg
(Da' y idy : reduce (Ea Earg y) (Ea' Earg' y)))
<- substitute Db Darg (Db': reduce (Eb Earg) (Eb' Earg')).

%worlds (exp_subst) (substitute _ _ _).
%total D (substitute D _ _).```