Library ski

Require Import String.
Require Import List.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import directed.
Require Import plotkin.
Require Import joinable.
Require Import approx_rels.
Require Import cpo.
Require Import profinite.
Require Import discrete.

Soundness, adequacy and strong normalization for simply-typed SKI with booleans.

As a demonstration of the system in action, here is a proof of soundness and adequacy for a simply-typed SKI calculus. The adequacy proof goes via a standard logical-relations argument. As a corollary of the main logical-relations lemma, we achieve strong normalization for the calculus.
We have arrow types and a single base type of booleans.
Inductive ty :=
  | ty_bool
  | ty_arrow : ty -> ty -> ty.

Delimit Scope ty_scope with ty.
Notation "2" := ty_bool : ty_scope.
Notation "x ⇒ y" := (ty_arrow (x)%ty (y)%ty) : ty_scope.

Delimit Scope ski_scope with ski.
Open Scope ski_scope.

Terms are boolean constants, the standard combinators S, K and I, and an IF/THEN/ELSE combinator; and applications.
Inductive term : ty -> Type :=

  | tbool : forall b:bool,
                term 2

  | tapp : forall σ σ,
                term (σ σ) ->
                term σ ->
                term σ

  | tI : forall σ,
                term (σ σ)

  | tK : forall σ σ,
                term (σ σ σ)

  | tS : forall σ σ σ,
                term ((σ σ σ) (σ σ) σ σ)

  | tIF : forall σ,
                term (2 σ σ σ).

Notation "x • y" := (tapp x y)
  (at level 52, left associativity, format "x • y") : ski_scope.

The operational semantics is given in a big-step style, with the specification of redexes split out into a separate relation.

Inductive redex : forall σ σ, term (σ σ) -> term σ -> term σ -> Prop :=
  | redex_I : forall σ x,
                  redex _ _ (tI σ) x x
  | redex_K : forall σ σ x y,
                  redex σ σ (tK σ σ y) x y
  | redex_S : forall σ σ σ f g x,
                  redex _ _ (tS σ σ σ f g)
  | redex_IFtrue : forall σ th el,
                  redex _ _ (tIF σ tbool true th) el th
  | redex_IFfalse : forall σ th el,
                  redex _ _ (tIF σ tbool false th) el el.

Inductive eval : forall τ, term τ -> term τ -> Prop :=
  | ebool : forall b, eval 2 (tbool b) (tbool b)
  | eI : forall σ, eval _ (tI σ) (tI _)
  | eK : forall σ σ, eval _ (tK σ σ) (tK _ _)
  | eS : forall σ σ σ, eval _ (tS σ σ σ) (tS _ _ _)
  | eIF : forall σ , eval _ (tIF σ) (tIF σ)
  | eapp1 : forall σ σ m₁ m₂ n₁ n₂ r z,
             eval (σ σ) m₁ n₁ ->
             eval σ m₂ n₂ ->
             redex σ σ n₁ n₂ r ->
             eval σ r z ->
             eval σ (m₁ m₂) z
  | eapp2 : forall σ σ m₁ m₂ n₁ n₂,
             eval (σ σ) m₁ n₁ ->
             eval σ m₂ n₂ ->
             ~(exists r, redex σ σ n₁ n₂ r) ->
             eval σ (m₁ m₂) (n₁ n₂).

Syntactic types have decicable equality, which implies injectivity for dependent pairs with (syntactic) types as the type being depended upon.
Lemma inj_pair2_ty : forall (F:ty -> Type) τ x y,
  existT F τ x = existT F τ y -> x = y.

Ltac inj_ty :=
  repeat match goal with
           [ H : existT _ _ _ = existT _ _ _ |- _ ] =>
             apply inj_pair2_ty in H

Ltac inv H :=
  inversion H; subst; inj_ty; repeat subst.

Values are terms that evaluate to themselves.
Definition value σ (t:term σ) := eval _ t t.

Here are some basic techincal results about the operational semantics.
Lemma eval_value τ x y :
  eval τ x y -> value y.

Lemma redex_eq τ τ x y z1 z2 :
  redex τ τ x y z1 ->
  redex τ τ x y z2 ->
  z1 = z2.

Lemma eval_eq τ x y1 y2 :
  eval τ x y1 -> eval τ x y2 -> y1 = y2.

Lemma eval_trans τ x y z :
  eval τ x y -> eval τ y z -> eval τ x z.

Lemma eval_app_congruence σ σ : forall x x' y y' z,
  (forall q, eval _ x q -> eval _ x' q) ->
  (forall q, eval _ y q -> eval _ y' q) ->
  eval _ (@tapp σ σ x y) z ->
  eval _ (@tapp σ σ x' y') z.

Types are interpreted as unpointed domains, using the discrete domain of booleans and the exponential in PLT.
Fixpoint tydom (τ:ty) : PLT :=
  match τ with
  | 2%ty => disc finbool
  | (τ τ)%ty => tydom τ tydom τ

The denotation of terms is given by a simple fixpoint on term structure. The denotation of each combinator is a straightforward interpretation of the usual lambda term into the operations of a cartesian closed category.

Fixpoint denote (τ:ty) (m:term τ) : 1 tydom τ :=
  match m in term τ return 1 tydom τ with
  | tbool b => disc_elem b

  | tapp σ σ m₁ m₂ => apply m₁, m₂

  | tI σ => Λ(π)

  | tK σ σ => Λ(Λ(π π))

  | tS σ σ σ => Λ(Λ(Λ(
                    apply apply π π π, π
                            , apply π π, π

  | tIF σ => Λ (disc_cases (fun b:bool =>
                 if b then Λ(Λ(π π))
                      else Λ(Λ(π))

 where "〚 m 〛" := (denote _ m) : ski_scope.

Every redex preserves the meaning of terms.
Lemma redex_soundness : forall σ σ x y z,
  redex σ σ x y z ->
  apply x,y z.

Evaluation preserves the denotation of terms.
Theorem soundness : forall τ (m z:term τ),
  eval τ m z -> m z.

The logical relations lemma

Now we define the logical relation. It is defined by induction on the structure of types, in a standard way.
Fixpoint LR (τ:ty) : term τ -> (1 tydom τ) -> Prop :=
  match τ as τ' return term τ' -> (1 tydom τ') -> Prop
  | ty_bool => fun m h =>
        exists b:bool, m = tbool b /\ h disc_elem b
  | ty_arrow σ σ => fun m h =>
        forall n h',
          LR σ n h' -> eval σ n n ->
          exists z,
            eval _ (mn) z /\
            LR σ z (apply h, h')

Lemma LR_equiv τ : forall m h h',
  h h' -> LR τ m h -> LR τ m h'.

Now we need a host of auxilary definitions to state the main lemmas regarding the logical relation. These definitions allow us to apply an arbitrary number of arguments to a syntactic term and to the denotation of terms.
Fixpoint lrtys (ts:list ty) (z:ty) : ty :=
  match ts with
  | nil => z
  | t::ts' => (t (lrtys ts' z))%ty

Fixpoint lrsyn (ts:list ty) : Type :=
  match ts with
  | nil => unit
  | t::ts' => prod (lrsyn ts') (term t)

Fixpoint lrsem (ts:list ty) : Type :=
  match ts with
  | nil => unit
  | t::ts' => prod (lrsem ts') (1 tydom t)

Fixpoint lrhyps (ls:list ty) : lrsyn ls -> lrsem ls -> Prop :=
  match ls with
  | nil => fun _ _ => True
  | t::ts => fun xs ys =>
      eval _ (snd xs) (snd xs) /\
      LR t (snd xs) (snd ys) /\
      lrhyps ts (fst xs) (fst ys)

Fixpoint lrapp (ls:list ty) z : lrsyn ls -> term (lrtys ls z) -> term z :=
  match ls as ls' return lrsyn ls' -> term (lrtys ls' z) -> term z with
  | nil => fun _ m => m
  | t::ts => fun xs m => lrapp ts _ (fst xs) (m (snd xs))

Fixpoint lrsemapp (ls:list ty) z :
  lrsem ls -> (1 tydom (lrtys ls z)) -> (1 tydom z) :=
  match ls as ls' return
    lrsem ls' -> (1 tydom (lrtys ls' z)) -> (1 tydom z)
  | nil => fun _ h => h
  | t::ts => fun ys h => lrsemapp ts _ (fst ys) (apply h, snd ys)

Lemma eval_lrapp_congruence ls : forall xs τ m m' z,
  (forall q, eval _ m q -> eval _ m' q) ->
  eval τ (lrapp ls τ xs m) z ->
  eval τ (lrapp ls τ xs m') z.

Lemma lrsemapp_equiv ls : forall τ ys h h',
  h h' -> lrsemapp ls τ ys h lrsemapp ls τ ys h'.

This fact is important in the base cases of the fundamental lemma; it allows unwind a stack of applications.
Lemma LR_under_apply ls :
   forall (τ : ty) (m z0 : term (lrtys ls τ)) (xs : lrsyn ls)
     (ys : lrsem ls) (h : 1 (tydom (lrtys ls τ))),
   eval (lrtys ls τ) m z0 ->
   lrhyps ls xs ys ->
   LR (lrtys ls τ) z0 h ->
   exists z : term τ,
     eval τ (lrapp ls τ xs m) z /\ LR τ z (lrsemapp ls τ ys h).

Now we prove that each of the base combinators stands in the logical relation with their denotations.
Lemma LR_I σ : LR _ (tI σ) tI σ.

Lemma LR_K σ σ : LR _ (tK σ σ) tK σ σ.

Lemma LR_S σ σ σ : LR _ (tS σ σ σ) tS σ σ σ.

Lemma LR_IF σ : LR _ (tIF σ) tIF σ.

The fundamental lemma states that every term stands in the logical relation with its denotation when applied related term/denotation pairs.
Lemma fundamental_lemma : forall σ (n:term σ) ls τ m xs ys
  (Hσ : σ = lrtys ls τ),
  eq_rect σ term n (lrtys ls τ) Hσ = m ->
  lrhyps ls xs ys ->
  exists z,
    eval _ (lrapp ls τ xs m) z /\
    LR τ z (lrsemapp ls τ ys m).

A simpified form of the fundamental lemma that follows from the inductively-strong one above.
Lemma fundamental_lemma' : forall τ (m:term τ),
  exists z, eval τ m z /\ LR τ z m .

Contextual equivalance and the adequacy theorem.

Now we define contextual equivalance. Contexts here are given in "inside-out" form, which makes the induction in the adequacy proof significantly easier.
Inductive context τ : ty -> Type :=
  | cxt_top : context τ τ
  | cxt_appl : forall σ σ,
                    term σ ->
                    context τ σ ->
                    context τ (σ σ)
  | cxt_appr : forall σ σ,
                    term (σ σ) ->
                    context τ σ ->
                    context τ σ.

Fixpoint plug τ σ (C:context τ σ) : term σ -> term τ :=
  match C in context _ σ return term σ -> term τ with
  | cxt_top => fun x => x
  | cxt_appl σ σ t C' => fun x => plug τ _ C' (tapp x t)
  | cxt_appr σ σ t C' => fun x => plug τ _ C' (tapp t x)

Definition cxt_eq τ σ (m n:term σ):=
  forall (C:context τ σ) (z:term τ),
    eval τ (plug τ σ C m) z <-> eval τ (plug τ σ C n) z.

Adequacy means that terms with equivalant denotations are contextually equivalant in any boolean context.
Theorem adequacy : forall τ (m n:term τ),
  m n -> cxt_eq 2 τ m n.

As a corollary of the fundamental lemma, we learn that the calculus is strongly normalizing.
Corollary normalizing : forall τ (m:term τ), exists z, eval τ m z.

These should print "Closed under the global context", meaning these theorems hold without the use of any axioms.
Print Assumptions adequacy.
Print Assumptions normalizing.