Church Rosser... Right?

church-rosser.elf

%{ Proving the Church Rosser theorem for lambda calculus in Twelf }%

%{ First, let's define the untyped lambda calculus }%

term : type.
ap  : term -> term   -> term.
lam : (term -> term) -> term.

%{ Evaluation }%

runs : term -> term -> type.
runs/lam : runs (lam F) (lam F).
runs/ap  : runs (ap F A) V
            <- runs F (lam F')
            <- runs (F' A) V.

%{ We next prove that evaluation actually gives back a value
   if it terminates
}%

val : term -> type.
val/l : val (lam F).

runs-to-val : runs L L' -> val L' -> type.
%mode runs-to-val +A -B.

- : runs-to-val runs/lam val/l.
- : runs-to-val (runs/ap R2 R1) V
     <- runs-to-val R2 V.

%worlds () (runs-to-val _ _).
%total (T) (runs-to-val T _).

%{ Now we want to show that normal forms are unique }%

eq : term -> term -> type.
refl : eq E E.

%{ Because Twelf's termination checker is very unhappy if we
   try to assert that a recursive "call" gives back refl, we
   have a lemma which turns the pattern matching into an input
   coverage problem. This needs mutual reduction and the terms
   only decrease in one direction. To help with this, we have
   big and small. big contains small. By giving the lemma which
   calls church-rosser on the same size arguments a big and
   church-rosser itself, we can convince Twelf this is total via
   lexigraphical induction.

   The weird tricks you learn with proof assistants...
}%

small : type.
s     : small.

big : type.
mkBig : small -> big.

%abbrev b : big = mkBig s.

%{ Lemma for pattern matching on equalities }%
destruct-eq : big
               -> eq (lam E) (lam E')
               -> runs (E  A) V
               -> runs (E' A) V'
               -> eq V V'
               -> type.
%mode destruct-eq +A +B +C +D -E.

%{ The main lemma, this is basically CR but with an extra
   small argument, for no particular reason I'm not going
   to call this CH yet
}%

main-lemma : small -> runs E V -> runs E V' -> eq V V' -> type.
%mode main-lemma +A +B +C -D.

- : destruct-eq b refl R1 R2 Eq
     <- main-lemma s R1 R2 Eq.

- : main-lemma s runs/lam runs/lam refl.
- : main-lemma s (runs/ap R2 R1) (runs/ap R2' R1') Eq'
     <- main-lemma s R1 R1' (Eq : eq (lam F) (lam F'))
     <- destruct-eq b Eq (R2 : runs (F A) _) (R2' : runs (F' A) _) Eq'.

%worlds ()
(destruct-eq _ _ _ _ _)
(main-lemma _ _ _ _).

%total {(A1 A2) (B1 B2)}
(destruct-eq B1 _ A1 _ _)
(main-lemma B2 A2 _ _).

%{ Proper statement }%

church-rosser : runs E V -> runs E V' -> eq V V' -> type.
%mode church-rosser +A +B -C.

- : church-rosser R1 R2 Eq
     <- main-lemma s R1 R2 Eq.

%worlds () (church-rosser _ _ _).
%total (T) (church-rosser T _ _).

%{ And there you have it }%