pisigma-0.1.0.3: examples/SubjectReduction.pi

-- Context:
--   Recursion with boxes
--   Thorsten Altenkirch
--   http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=104

Stream : Type;
Stream = [∞ Stream];

ticks : Stream;
ticks = [ticks];

Eq : (A : Type) → A → A → Type;
Eq = λ A x y → (P : A → Type) → P x → P y;

refl : (A : Type) → (x : A) → Eq A x x;
refl = λ A x P px → px;

unfold : Eq Stream ticks [ticks];
unfold = refl Stream ticks;

-- We can prove this variant of congruence for boxes:

cong : (xs ys : Stream) → Eq Stream xs ys →
       Eq Stream [let zs : Stream = xs in zs]
                 [let zs : Stream = ys in zs];
cong = λ xs ys eq P p → eq (λ zs → P [let us : Stream = zs in us]) p;

-- This does not (obviously) break subject reduction, because the
-- following property can be proved using refl:

unfoldInContext : Eq Stream [let xs : Stream =  ticks  in xs]
                            [let xs : Stream = [ticks] in xs];
unfoldInContext = cong ticks [ticks] unfold;
unfoldInContext = refl Stream [let xs : Stream = ticks in xs];

-- Note also that unlimited unfolding is not possible (using refl):

-- unfoldTwiceInContext : Eq Stream [let xs : Stream =   ticks   in xs]
--                                  [let xs : Stream = [[ticks]] in xs];
-- unfoldTwiceInContext = refl Stream [let xs : Stream = ticks in xs];

-- However, we can move lets through boxes, so the idea from
-- Thorsten's blog post needs to be qualified.

letThroughBox : (xs : Stream) →
                Eq Stream [let ys : Stream = xs in  ys]
                          (let ys : Stream = xs in [ys]);
letThroughBox = λ xs → refl Stream [let ys : Stream = xs in ys];

letThrough2Boxes : (xs : Stream) →
                   Eq Stream [[let ys : Stream = xs in  ys]]
                             (let ys : Stream = xs in [[ys]]);
letThrough2Boxes = λ xs → refl Stream [[let ys : Stream = xs in ys]];

anotherExample : (A : Type) → (x : A) →
                 Eq (∞ (∞ A)) [let y : A = x in [y]]
                              (let y : A = x in [[let z : A = y in z]]);
anotherExample = λ A x → refl (∞ (∞ A)) (let y : A = x in [[y]]);