Library skiy

Require Import String.
Require Import List.
Require Import Arith.
Require Import Omega.

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 profinite_adj.
Require Import strict_utils.
Require Import fixes.
Require Import flat.

Soundness and adequacy simply-typed SKI with booleans and fixpoints.

The adequacy proof goes via a standard logical-relations argument. As a corollary of the main logical-relations lemma, we show that nonvalues are denoted by ⊥.
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. We also have the call-by-value fixpoint combinator Y. As usual for the CBV fixpoint operator, it only calculates fixpoints at function types.
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 σ σ σ)

  | tY : forall σ σ,
                term ( ((σ σ) (σ σ)) (σ σ) ).

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

  | redex_Y : forall σ σ (f:term ((σ σ) (σ σ))) x,
                  redex _ _ (tY σ σ f) x
                            (f•(tY σ σ f)•x).

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 σ)
  | eY : forall σ σ, eval _ (tY σ σ) (tY _ _)
  | 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.

Lemma eval_no_redex : forall σ σ x x',
  eval σ x x' ->
  forall m₁ m₂ n₁ n₂ r,
    x' = @tapp σ σ m₁ m₂ ->
    eval _ m₁ n₁ -> eval _ m₂ n₂ -> redex _ _ n₁ n₂ r -> False.

Lemma value_app_inv σ σ x y :
  value (@tapp σ σ x y) ->
  value x /\ value y.

"Inert" terms are those that will not evaluate if applied to one more argument. We prove that every term at function type is either intert or forms a redex if applied to another term.
Inductive inert : forall σ σ, term (σ σ) -> Prop :=
  | inert_K : forall σ σ,
                  inert _ _ (tK σ σ)
  | inert_S1 : forall σ σ σ,
                  inert _ _ (tS σ σ σ)
  | inert_S2 : forall σ σ σ x,
                  inert _ _ (tS σ σ σ x)
  | inert_IF1 : forall σ,
                  inert _ _ (tIF σ)
  | inert_IF2 : forall σ x,
                  inert _ _ (tIF σ x)
  | inert_Y : forall σ σ,
                  inert _ _ (tY σ σ).

Fixpoint tmsize τ (x:term τ) : nat :=
  match x with
  | tapp σ σ a b => (1 + tmsize _ a + tmsize _ b)%nat
  | _ => 1%nat

Lemma redex_inert_false : forall σ σ f g r,
  redex σ σ f g r ->
  inert σ σ f ->

Lemma redex_or_inert' n :
  forall τ (x:term τ) σ σ (f:term (σ σ))
    (Hτ : τ = (σ σ)%ty)
    (Hx : eq_rect τ term x _ Hτ = f)
    (Hsz : tmsize τ x = n),
    value f ->
    (forall g, exists r, redex σ σ f g r) \/ inert σ σ f.

Lemma redex_or_inert :
  forall σ σ (f:term (σ σ)),
    value f ->
    (forall g, exists r, redex σ σ f g r) \/ inert σ σ f.

Lemma canonical_bool : forall x,
  eval 2 x x ->
  x = tbool true \/ x = tbool false.

Types are interpreted as pointed domains. Booleans are the flat domain over booleans and the arrow type is the lifted strict function space.
Fixpoint tydom (τ:ty) : PLT :=
  match τ with
  | ty_bool => flat enumbool
  | ty_arrow τ τ => colift (tydom τ tydom τ)

Here we define the semantics of the Y combinator.
Section Ydefn.
  Variables σ σ:ty.

  Definition Ybody
    : U (colift (tydom (σ σ) tydom (σ σ)))
        PLT.exp (U (tydom (σ σ))) (U (tydom (σ σ)))

    := PLT.curry (strict_curry'

        (strict_app' strict_app' π π, π π〉, π)

  Lemma Ybody_unroll : forall Γ
    (f:Γ U (tydom ((σ σ) (σ σ))))
    (x:Γ U (tydom σ)),

    semvalue x ->

    let Yf := (fixes _ _ Ybody) f in

    strict_app' Yf, x
    strict_app' strict_app' f,Yf , x.

  Definition Ysem Γ
    : Γ U (tydom (((σ σ) (σ σ)) (σ σ)))
    := strict_curry' (fixes _ _ Ybody π).
End Ydefn.

Notation "'Λ' f" := (strict_curry' f) : ski_scope.

The denotation of terms. The denotation of the S, K and I combinators a straightforward interpretation of the usual lambda term into the strict lambda and strict application denotation functions.
Fixpoint denote (τ:ty) (m:term τ) : 1 U (tydom τ) :=
  match m in term τ return 1 U (tydom τ) with
  | tbool b => flat_elem' b
  | tapp σ σ m₁ m₂ => strict_app' m₁,m₂
  | tI σ => Λ(π)
  | tK σ σ => Λ(Λ(π π))
  | tS σ σ σ => Λ(Λ(Λ(
                        strict_app' π π π, π
                       , strict_app' π π, π
  | tIF σ => Λ(flat_cases' (fun b:bool =>
                if b then Λ(Λ(π π))
                     else Λ(Λ(π))
  | tY σ σ => Ysem σ σ 1
 where "〚 m 〛" := (denote _ m) : ski_scope.

This mutual induction shows that operational values have semantic values as denotations, and that inert operational values yield semantic values when applied to any semantic value.
Lemma value_inert_semvalue : forall n,
  (forall σ x,
    tmsize _ x = n ->
    eval σ x x -> semvalue x) /\
  (forall σ σ x (y:1 U (tydom σ)),
    tmsize _ x = n ->
    value x ->
    inert σ σ x ->
    semvalue y ->
    semvalue (strict_app' x, y)).

Lemma value_semvalue : forall σ (x:term σ),
  value x -> semvalue x.

Lemma inert_semvalue σ σ x y :
  value x -> inert σ σ x -> semvalue y ->
  semvalue (strict_app' x, y ).

Hint Resolve value_semvalue.

Now we can show the soundness of redexes.
Lemma redex_soundness : forall σ σ x y z,
  value x ->
  value y ->
  redex σ σ x y z ->
  strict_app' x,y z.

This leads easily into the soundness of evaluation.
Lemma soundness : forall τ (m z:term τ),
  eval τ m z -> mz.

The logical relations lemma

Now define the logical relation for adequacy. It is defined by induction on the structure of types, in a standard way.
Fixpoint LR (τ:ty) :
  term τ -> (1 U (tydom τ)) -> Prop :=
  match τ as τ' return
    term τ' -> (1 U (tydom τ')) -> Prop
  | ty_bool => fun m h => exists b:bool,
        m = tbool b /\ h flat_elem' b
  | ty_arrow σ σ => fun m h =>
        forall n h',
          LR σ n h' -> value n -> semvalue h' ->
          semvalue (strict_app' h, h') ->
          exists z,
            eval _ (m n) z /\
            LR σ z (strict_app' 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) :=
  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 U (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) /\ semvalue (snd ys)) /\
    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 U (tydom (lrtys ls z))) -> (1 U (tydom z)) :=
  match ls as ls' return
    lrsem ls' -> (1 U (tydom (lrtys ls' z))) -> (1 U (tydom z))
  | nil => fun _ h => h
  | t::ts => fun ys h => lrsemapp ts _ (fst ys) (strict_app' 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'.

Lemma semvalue_lrsemapp_out ls : forall τ ys h,
   semvalue (lrsemapp ls τ ys h) -> semvalue 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 U (tydom (lrtys ls τ))),
   eval (lrtys ls τ) m z0 ->
   lrhyps ls xs ys ->
   semvalue (lrsemapp ls τ ys h) ->
   LR (lrtys ls τ) z0 h ->
   exists z : term τ,
     eval τ (lrapp ls τ xs m) z /\ LR τ z (lrsemapp ls τ ys h).

If a sup is a semantic value, then there is some element of the set is a semantic value.
Lemma semvalue_sup (B:PLT) (XS:dirset (PLT.homset_cpo _ 1 (U B))) :
  semvalue (XS) -> exists x, x XS /\ semvalue x.

The logical relation is admissible. This is key to the fundamental lemma case for Y.
Lemma LR_admissible τ :
  forall m (XS:dirset (PLT.homset_cpo _ 1 (U (tydom τ)))),
  semvalue (XS) ->
  (forall x, x XS -> semvalue x -> LR τ m x) -> LR τ m (XS).

Here we prove fundamental lemma case for he main body of Y combinator. This proof goes by Scott induction.
Lemma LR_Ybody σ σ
  (f:term ((σ σ) σ σ)) hf :
  LR _ f hf -> value f -> semvalue hf ->

  forall (x:term σ) hx,
    LR σ x hx -> value x -> semvalue hx ->
    semvalue (strict_app' fixes _ _ (Ybody σ σ) hf, hx) ->
    exists z:term σ,
      eval _ (tY σ σ f x) z /\
      LR _ z (strict_app' fixes _ _ (Ybody σ σ) hf, hx).

Now we can prove the fundamental lemma cases for each of the system combinators.

Lemma LR_I σ : LR _ (tI σ) tI σ.

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

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

Lemma LR_Y σ σ : LR _ (tY σ σ) tY σ σ.

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

Now the fundamental lemma follows by induction on terms.
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 ->
  semvalue (lrsemapp ls τ ys m) ->
  exists z,
    eval _ (lrapp ls τ xs m) z /\
    LR τ z (lrsemapp ls τ ys m).

A specialization of the fundamental lemma to empty contexts
Lemma fundamental_lemma' : forall τ (m:term τ),
  semvalue m ->
  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 τ),
  mn -> cxt_eq 2 τ m n.

Every term fails to evaluate iff the denotation is bottom.
Corollary denote_bottom_nonvalue : forall τ (m:term τ),
  (~exists z, eval τ m z) <-> m .

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