LambdaSigmaCalc.v

Inductive term :=
    | One : term 
    | App : term -> term -> term
    | Abs : term -> term
    | Subst : term -> subst -> term 

with subst :=
    | ids 
    | shift
    | cons : term -> subst -> subst
    | compose : subst -> subst -> subst.

Notation λ := Abs.
Infix "<*>" := App(at level 50, left associativity).
Notation "[ t <- s ] " := (Subst t s)(at level 50).
Notation "↑" := shift.
Notation "t ∙ s" := (cons t s) (at level 50).
Notation "s1 ∘ s2" := (compose s1 s2) (at level 50).
Notation "1" := One.

    
Inductive reduce : term -> term -> Prop :=
    | R_Beta a b : reduce ((λ a) <*> b) ([a <- (b ∙ ids)])
    | R_VarId : reduce ([1 <- ids]) 1
    | R_VarCons a s : reduce ([1 <- a ∙ s]) a
    | R_AppSubst a b s : reduce ([a <*> b <- s]) ([a <- s] <*> [b <- s])
    | R_AbsSubst a s : reduce ([λ a <- s]) (λ ([a <- 1 ∙ (s ∘ ↑)]))
    | R_Clos a s t : reduce ([[a <- s] <- t]) ([a <- s ∘ t])

    | R_Abs t t' : reduce t t' -> reduce (λ t) (λ t')
    | R_App1 f f' v : reduce f f' -> reduce (f <*> v) (f' <*> v)
    | R_App2 f v v' : reduce v v' -> reduce (f <*> v) (f <*> v')
    | R_Subst1 t t' s : reduce t t' -> reduce ([t <- s]) ([t' <- s])
    | R_Subst2 t s s' : reduceS s s' -> reduce ([t <- s]) ([t <- s'])



with reduceS : subst -> subst -> Prop :=
    | RS_IdL s : reduceS (ids ∘ s) s
    | RS_ShiftId : reduceS (↑ ∘ ids) ↑
    | RS_ShiftCons a s : reduceS (↑ ∘ (a ∙ s)) s
    | RS_Map a s t : reduceS ((a ∙ s) ∘ t) ([a <- t] ∙ (s ∘ t))
    | RS_Ass s1 s2 s3 : reduceS ((s1 ∘ s2) ∘ s3) (s1 ∘ (s2 ∘ s3))

    | RS_Cons1 t t' s : reduce t t' -> reduceS (t ∙ s) (t' ∙ s)
    | RS_Cons2 t s s' : reduceS s s' -> reduceS (t ∙ s) (t ∙ s')
    | RS_Compose1 t t' s : reduceS t t' -> reduceS (t ∘ s) (t' ∘ s)
    | RS_Compose2 t s s' : reduceS s s' -> reduceS (t ∘ s) (t ∘ s').


Hint Constructors reduce reduceS.
Infix "→" := (reduce)(at level 30).


Inductive step : term -> term -> Prop :=
    | st_refl t : step t  t
    | st_step t t' t'' : reduce t t' -> step t' t'' -> step t t''.

Infix  "⟶" := (step) (at level 30).

Definition normal (t : term) := ~ exists t', reduce t t'.