Library st_lam_fix


Require Import String.

Require Import atoms.
Require Import permutations.

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

Require Import List.

The simply-typed λ-calculus with booleans and fixpoints

This file develops the call-by-value simply-typed λ-calculus with named variables and a fixpoint operator. Types are interpreted as pointed domains in ∂PLT.
Soundness and adequacy of the denotational semantics are proved with respect to a standard big-step operational semantics. This uses the standard logical relation approach.

Types and type denotations

We have a boolean base type and functions.
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 lam_scope with lam.
Open Scope lam_scope.

Types are interpreted via a straightforward translation into ∂PLT domains.
Fixpoint tydom (τ:ty) : PLT :=
  match τ with
  | 2%ty => flat enumbool
  | (τ τ)%ty => colift (tydom τ tydom τ)
  end.

The syntax of types has decidable equality. This is important because it allows us to work around some problems that arise with dependent types.
Lemma ty_dec : forall x y:ty, {x=y}+{x<>y}.

Type contexts

Now we instantiate a module for finite products. This gives us a domain in PLT for representing type contexts, and provides operations and lemmas we need for working with them.
Module env_input <: FINPROD_INPUT.
  Definition A := ty.
  Definition Adec := ty_dec.
  Definition F τ := U (tydom τ).
End env_input.

Module ENV := finprod.finprod(env_input).

Notation env := ENV.env.
Notation inenv := ENV.inenv.
Canonical Structure ENV.env_supported.

Notation cxt := ENV.finprod.
Notation castty := (cast ENV.ty).
Notation proj := ENV.proj.
Notation bind := ENV.bind.

Terms and term denotations

Terms are intrinsicly-typed, carrying both a type environment for their free variables and the final type of the term.
Variables carry a name (atom) and a proof that (x,σ) appears in the type environment. Lambdas and the fixpoint operator extend the type environment in the standard way.
Inductive term (Γ:env) : ty -> Type :=
  | tvar : forall x σ,
                inenv Γ x σ ->
                term Γ σ
  | tbool : forall n:bool,
                term Γ 2
  | tapp : forall σ σ,
                term Γ (σ σ) ->
                term Γ σ ->
                term Γ σ
  | tif : forall σ,
                term Γ 2 ->
                term Γ σ ->
                term Γ σ ->
                term Γ σ
  | tlam : forall x σ σ,
                term ((x,σ)::Γ) σ ->
                term Γ (σ σ)
  | tfix : forall x σ,
                term ((x,σ)::Γ) σ ->
                term Γ σ.

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

Notation subst := (ENV.subst term).
Notation term_wk := (ENV.tm_wk term).
Notation term_subst := (ENV.tm_subst term).

The terms in environment Γ with type τ are interpreted as ∂PLT-homs from cxt Γ to U (tydom τ).
Definition dom (Γ:env) (τ:ty) : Type := cxt Γ U (tydom τ).

Fixpoint denote (Γ:env) (τ:ty) (m:term Γ τ) : dom Γ τ :=
  match m in term _ τ' return dom Γ τ' with
  | tvar x σ IN => castty IN proj Γ x
  | tbool b => flat_elem' b
  | tif σ x y z =>
      flat_cases' (fun b:bool => if b then y else z) id, x
  | tapp σ σ m₁ m₂ => strict_app' m₁, m₂
  | tfix x σ m' => fixes (cxt Γ) (tydom σ) (Λ(m' bind Γ x σ))
  | tlam x σ σ m' => strict_curry' (m' bind Γ x σ)
  end
 where "〚 m 〛" := (denote _ _ m) : lam_scope.

Here we define a generic traversal function. This traversal is uniformly used to define both weakening and substitution by exploiting the finprod library. Defining this traversal and its correctness proof is sufficent to get out a definition of substitution and a proof of correctness.
Section traverse.
  Variable thingy:env -> atom -> ty -> Type.
  Variable thingy_term : forall Γ x σ, thingy Γ x σ -> term Γ σ.
  Variable rename_var : env -> atom -> atom.
  Variable weaken_vars : forall Γ₁ Γ₂ y τ,
    (forall x σ, inenv Γ₁ x σ -> thingy Γ₂ x σ) ->
    (forall x σ, inenv ((y,τ)::Γ₁) x σ -> thingy ((rename_var Γ₂ y,τ)::Γ₂) x σ).

  Fixpoint traverse
    (Γ₁ Γ₂:env) (σ:ty)
    (VAR : forall x σ, inenv Γ₁ x σ -> thingy Γ₂ x σ)
    (m:term Γ₁ σ) : term Γ₂ σ :=

    match m with
    | tvar x σ IN => thingy_term Γ₂ x σ (VAR x σ IN)
    | tbool b => tbool Γ₂ b
    | tapp σ σ m₁ m₂ =>
        @tapp Γ₂ σ σ (traverse Γ₁ Γ₂ σ) VAR m₁)
                       (traverse Γ₁ Γ₂ σ VAR m₂)
    | tif σ x y z =>
           tif Γ₂ σ (traverse Γ₁ Γ₂ ty_bool VAR x)
                    (traverse Γ₁ Γ₂ σ VAR y)
                    (traverse Γ₁ Γ₂ σ VAR z)
    | tlam x σ σ m' =>
           let x' := rename_var Γ₂ x in
           tlam Γ₂ x' σ σ
                (traverse ((x,σ)::Γ₁) ((x',σ)::Γ₂) σ
                  (weaken_vars Γ₁ Γ₂ x σ VAR)
                  m')

    | tfix x σ m' =>
           let x' := rename_var Γ₂ x in
           tfix Γ₂ x' σ
                (traverse ((x,σ)::Γ₁) ((x',σ)::Γ₂) σ
                   (weaken_vars Γ₁ Γ₂ x σ VAR)
                   m')

    end.

  Hypothesis weaken_sem_bind : forall Γ₁ Γ₂ x σ VAR,
    bind Γ₁ x σ PLT.pair_map (ENV.varmap_denote term denote thingy thingy_term Γ₁ Γ₂ VAR) id
     ENV.varmap_denote term denote thingy thingy_term ((x,σ)::Γ₁) ((rename_var Γ₂ x,σ)::Γ₂)
       (weaken_vars Γ₁ Γ₂ x σ VAR) bind Γ₂ (rename_var Γ₂ x) σ.

  Hypothesis varmap_denote_proj : forall Γ₁ Γ₂ VAR x σ i,
     thingy_term Γ₂ x σ (VAR x σ i)
     castty i proj Γ₁ x ENV.varmap_denote term denote thingy thingy_term Γ₁ Γ₂ VAR.

  Lemma traverse_correct
    (Γ₁ Γ₂:env) (σ:ty)
    (m:term Γ₁ σ) : forall
    (VAR : forall x σ, inenv Γ₁ x σ -> thingy Γ₂ x σ),

    denote _ _ (traverse Γ₁ Γ₂ σ VAR m)
    denote _ _ m ENV.varmap_denote term denote thingy thingy_term Γ₁ Γ₂ VAR.
End traverse.

Register terms together with the denotation and traversal functions as a term model. This gives us access to the generic substitution definition in finprod.
Restate the substitution correctness lemma.
Lemma subst_soundness Γ x σ σ n₁ n₂ :
    n₁ bind Γ x σ id, n₂ subst Γ σ σ x n₁ n₂ .

Operational semantics and soundness

This is a standard call-by-value operational semantics.
Notation: mz means that m evaluates to z. m means that m evaluates to itself; i.e., m is a value.
Reserved Notation "m ⇓ z" (at level 82, left associativity).
Reserved Notation "m ↓" (at level 82, left associativity).

Inductive eval (Γ:env) : forall τ, term Γ τ -> term Γ τ -> Prop :=
  | ebool : forall b,
               tbool Γ b
  | eif : forall σ x y z b q,
               x (tbool Γ b) ->
               (if b then y else z) q ->
               (tif Γ σ x y z) q
  | elam : forall x σ σ m,
               tlam Γ x σ σ m
  | efix : forall x σ m z,
               subst Γ σ σ x m (tfix Γ x σ m) z ->
               tfix Γ x σ m z
  | eapp : forall x σ σ m₁ m₂ n₁ n₂ z,
               m₁ (tlam Γ x σ σ n₁) ->
               m₂ n₂ ->
               subst Γ σ σ x n₁ n₂ z ->
               m₁ m₂ z
 where "m ⇓ z" := (eval _ _ m z)
  and "m ↓" := (eval _ _ m m).

Every syntactic value is a semantic value.
Lemma value_semvalue Γ τ (m z:term Γ τ) : m z -> semvalue z.

Applications, if/then/else, and fixpoints are nonvalues.
Lemma app_not_value Γ σ (x y:term Γ σ) :
  xy -> forall σ (m:term Γ (σ σ)) n, y = mn -> False.

Lemma if_not_value Γ σ (x y:term Γ σ) :
  xy -> forall a b c, y = tif Γ σ a b c -> False.

Lemma fix_not_value Γ σ (x y:term Γ σ) :
  xy -> forall x m, y = tfix Γ x σ m -> False.

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

Misc technical lemmas

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.

Lemma env_dec : forall a b:env, {a=b}+{a<>b}.

Ltac inj_ty :=
  repeat match goal with
           [ H : existT _ _ _ = existT _ _ _ |- _ ] =>
             apply inj_pair2_ty in H ||
             apply (Eqdep_dec.inj_pair2_eq_dec _ string_dec) in H ||
             apply (Eqdep_dec.inj_pair2_eq_dec _ env_dec) in H
           end.

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

We will need a variety of technical results about the operational semantics.
Lemma eval_value Γ τ x y :
  eval Γ τ x y -> eval Γ τ y y.

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.

Alpha congruence

Here we define alpha congruence of terms.
Inductive var_cong : env -> env -> atom -> atom -> Prop :=
 | vcong_here : forall Γ₁ Γ₂ x₁ x₂ y₁ y₂ τ,
                   x₁ = y₁ -> x₂ = y₂ ->
                   var_cong ((x₁,τ)::Γ₁) ((x₂,τ)::Γ₂) y₁ y₂
 | vcong_there : forall Γ₁ Γ₂ x₁ x₂ y₁ y₂ τ,
                   x₁ <> y₁ -> x₂ <> y₂ ->
                   var_cong Γ₁ Γ₂ y₁ y₂ ->
                   var_cong ((x₁,τ)::Γ₁) ((x₂,τ)::Γ₂) y₁ y₂.

Inductive alpha_cong : forall Γ Γ' (τ:ty), term Γ τ -> term Γ' τ -> Prop :=

  | acong_var : forall Γ Γ' τ x₁ x₂ H₁ H₂,
                  var_cong Γ Γ' x₁ x₂ ->
                  alpha_cong Γ Γ' τ (tvar Γ x₁ τ H₁) (tvar Γ' x₂ τ H₂)

  | acong_bool : forall Γ Γ' b,
                  alpha_cong Γ Γ' ty_bool (tbool Γ b) (tbool Γ' b)

  | acong_app : forall Γ Γ' σ σ m₁ m₂ n₁ n₂,
                  alpha_cong Γ Γ' (σ σ) m₁ n₁ ->
                  alpha_cong Γ Γ' σ m₂ n₂ ->
                  alpha_cong Γ Γ' σ (m₁ m₂) (n₁ n₂)

  | acong_if : forall Γ Γ' σ x1 x2 y1 y2 z1 z2,
                  alpha_cong Γ Γ' ty_bool x1 x2 ->
                  alpha_cong Γ Γ' σ y1 y2 ->
                  alpha_cong Γ Γ' σ z1 z2 ->
                  alpha_cong Γ Γ' σ (tif Γ σ x1 y1 z1) (tif Γ' σ x2 y2 z2)
  
  | acong_fix : forall (Γ Γ':env) (x₁ x₂:atom) σ m₁ m₂,
                  alpha_cong ((x₁,σ)::Γ) ((x₂,σ)::Γ') σ m₁ m₂ ->
                  alpha_cong Γ Γ' σ (tfix Γ x₁ σ m₁) (tfix Γ' x₂ σ m₂)

  | acong_lam : forall (Γ Γ':env) (x₁ x₂:atom) σ σ m₁ m₂,
                  alpha_cong ((x₁,σ)::Γ) ((x₂,σ)::Γ') σ m₁ m₂ ->
                  alpha_cong Γ Γ' (σ σ) (tlam Γ x₁ σ σ m₁) (tlam Γ' x₂ σ σ m₂).

Alpha congruence is reflexive, transitive and symmetric.
Lemma var_cong_refl Γ x τ:
  inenv Γ x τ ->
  var_cong Γ Γ x x.

Lemma var_cong_sym Γ₁ Γ₂ x y :
  var_cong Γ₁ Γ₂ x y ->
  var_cong Γ₂ Γ₁ y x.

Lemma var_cong_trans Γ₁ Γ₂ x y z :
  var_cong Γ₁ Γ₂ x y ->
  forall Γ₃,
  var_cong Γ₂ Γ₃ y z ->
  var_cong Γ₁ Γ₃ x z.

Lemma alpha_eq_refl Γ σ (m:term Γ σ) :
  alpha_cong Γ Γ σ m m.

Lemma alpha_eq_sym Γ₁ Γ₂ τ m n :
  alpha_cong Γ₁ Γ₂ τ m n ->
  alpha_cong Γ₂ Γ₁ τ n m.

Lemma alpha_eq_trans Γ₁ τ (m:term Γ₁ τ) :
  forall Γ₂ Γ₃ (n:term Γ₂ τ) (o:term Γ₃ τ),
  alpha_cong Γ₁ Γ₂ τ m n ->
  alpha_cong Γ₂ Γ₃ τ n o ->
  alpha_cong Γ₁ Γ₃ τ m o.

Alpha congruent terms have equal denotations.
Lemma alpha_cong_denote (Γ₁ Γ₂:env) τ (m:term Γ₁ τ) (n:term Γ₂ τ) :
  alpha_cong Γ₁ Γ₂ τ m n ->

  forall A
    (h₁:A cxt Γ₁) (h₂:A cxt Γ₂),

  (forall a b τ (IN1:inenv Γ₁ a τ) (IN2:inenv Γ₂ b τ),
    var_cong Γ₁ Γ₂ a b ->
    castty IN1 proj Γ₁ a h₁ castty IN2 proj Γ₂ b h₂) ->

  m h₁ n h₂.

Lemma alpha_cong_denote' Γ τ (m:term Γ τ) (n:term Γ τ) :
  alpha_cong Γ Γ τ m n -> m n.

We'll end up needing quite a few facts about alpha congruence. Here we collect them together before defining the logical relation and tackling the fundamental lemma.
Congruence is preserved by weakening.
Lemma alpha_cong_wk : forall (Γm Γn Γm' Γn':env) τ m n H₁ H₂,
  (forall a b, var_cong Γm Γn a b -> var_cong Γm' Γn' a b) ->
  alpha_cong Γm Γn τ m n ->
  alpha_cong _ _ τ (term_wk Γm Γm' τ H₁ m)
                   (term_wk Γn Γn' τ H₂ n).

Variable congruence is closely related the inenv relation.
Lemma varcong_inenv1 Γ₁ Γ₂ a b :
  var_cong Γ₁ Γ₂ a b -> exists τ, inenv Γ₁ a τ.

Lemma varcong_inenv2 Γ₁ Γ₂ a b :
  var_cong Γ₁ Γ₂ a b -> exists τ, inenv Γ₂ b τ.

Lemma varcong_eq Γ₁ Γ₂ a b :
  var_cong Γ₁ Γ₂ a b -> Γ₁ = Γ₂ -> a = b.

Lemma inenv_varcong Γ a τ :
  inenv Γ a τ -> var_cong Γ Γ a a.

Lemma env_supp_inenv (Γ:env) a :
  a Γ <-> exists τ, inenv Γ a τ.

When congruent substitutions are applied to congruence terms, the resulting terms are congruent.
Lemma term_subst_cong : forall Γ τ (m:term Γ τ) Γ' (n:term Γ' τ) Γ₁ Γ₂
  (VAR1 : ENV.varmap term Γ Γ₁) (VAR2 : ENV.varmap term Γ' Γ₂),
  
  (forall a1 a2 σ IN1 IN2,
    var_cong Γ Γ' a1 a2 ->
    alpha_cong Γ₁ Γ₂ σ (VAR1 a1 σ IN1) (VAR2 a2 σ IN2)) ->

  alpha_cong Γ Γ' τ m n ->

  alpha_cong Γ₁ Γ₂ τ
    (term_subst Γ Γ₁ τ VAR1 m)
    (term_subst Γ' Γ₂ τ VAR2 n).

Evaluation commutes with alpha congruence.
Lemma eval_alpha Γ τ (m z:term Γ τ) :
  (m z) -> forall Γ' (n:term Γ' τ),
  alpha_cong Γ Γ' τ m n ->
  exists z', (n z') /\ alpha_cong Γ Γ' τ z z'.

The property of being a value is preserved by alpha congruence.
Lemma alpha_cong_value Γ Γ' σ x y :
  alpha_cong Γ Γ' σ x y -> x -> y.

Lemma term_wk_ident : forall Γ σ m H,
  term_wk Γ Γ σ H m = m.

Lemma term_wk_compose : forall Γ₁ σ m Γ₂ Γ₃ H1 H2 H3,
  term_wk Γ₂ Γ₃ σ H2 (term_wk Γ₁ Γ₂ σ H1 m) = term_wk Γ₁ Γ₃ σ H3 m.

Lemma term_wk_compose' : forall Γ₁ σ m Γ₂ Γ₃ H1 H2,
  term_wk Γ₂ Γ₃ σ H2 (term_wk Γ₁ Γ₂ σ H1 m) =
  term_wk Γ₁ Γ₃ σ (fun x τ H => H2 x τ (H1 x τ H)) m.

Lemma alpha_cong_eq Γ σ x y :
  x = y ->
  alpha_cong Γ Γ σ x y.

Weakening commutes with substition, up to alpha congruence.
Lemma term_subst_wk_cong : forall Γ τ (m:term Γ τ) Γ₁ Γ₂ Γ₃ Γ₄
  (VAR1 : ENV.varmap term Γ Γ₁) (VAR2:ENV.varmap term Γ₃ Γ₄) H₁ H₂,

  (forall a σ Ha1 Ha2 H,
    alpha_cong _ _ σ (term_wk Γ₁ Γ₂ σ H (VAR1 a σ Ha1)) (VAR2 a σ Ha2)) ->

  alpha_cong _ _ τ
    (term_wk Γ₁ Γ₂ τ H₁ (term_subst Γ Γ₁ τ VAR1 m))
    (term_subst Γ₃ Γ₄ τ VAR2 (term_wk Γ Γ₃ τ H₂ m)).

A sequence of substitutions is equal to a single composed substitution, up to alpha equivalance.
Lemma compose_term_subst : forall Γ₁ τ (m:term Γ₁ τ),
  forall (Γ₂ Γ₃:env) (g:ENV.varmap term Γ₂ Γ₃) (f:ENV.varmap term Γ₁ Γ₂),
  alpha_cong _ _ _
    (term_subst Γ₁ Γ₃ τ (ENV.varmap_compose term _ _ _ g f) m)
    (term_subst Γ₂ Γ₃ τ g (term_subst Γ₁ Γ₂ τ f m)).

This technical lemma allows us to prove that applying the identity subtitution is alpha congruent to the original term.
Lemma subst_weaken_alpha Γ Γ' σ
  (x:term Γ σ) (y:term Γ' σ) :

  alpha_cong Γ Γ' σ x y ->

  forall Γ₁ Γ₂ (VAR:ENV.varmap term Γ₁ Γ₂) H,

  (forall a b τ H1 H2, var_cong Γ Γ' a b ->
    alpha_cong Γ₂ Γ' τ (VAR a τ H1) (tvar Γ' b τ H2)) ->
    
  alpha_cong _ _ σ (term_subst _ _ σ VAR (term_wk _ _ _ H x)) y.

Applying the identity substuition is alpha congruenct to the original term.
Lemma subst_alpha_ident Γ Γ' σ
  (x:term Γ σ) (y:term Γ' σ) :
  alpha_cong Γ Γ' σ x y ->

  forall Γ₂ (VAR:ENV.varmap term Γ Γ₂),

  (forall a b τ H1 H2, var_cong Γ Γ' a b ->
    alpha_cong Γ₂ Γ' τ (VAR a τ H1) (tvar Γ' b τ H2)) ->
    
  alpha_cong _ _ σ (term_subst _ _ σ VAR x) y.

This lemma show that extending a substitution is alpha congruent to first shifting and then extending.
Lemma extend_shift_alpha : forall
  (Γ : env)
  (x : atom)
  (σ : ty)
  (VAR : ENV.varmap term Γ nil)
  (n : term nil σ)
  (a1 a2 : atom)
  (σ : ty)
  (IN1 : inenv ((x, σ) :: Γ) a1 σ)
  (IN2 : inenv ((x, σ) :: Γ) a2 σ)
  (x':atom) Hx,

   var_cong ((x, σ) :: Γ) ((x, σ) :: Γ) a1 a2 ->

   alpha_cong nil nil σ
     (ENV.varmap_compose term ((x, σ) :: Γ) ((x', σ) :: nil) nil
        (ENV.extend_map term nil nil (tvar nil) x' σ n)
        (ENV.shift_vars term term_wk tvar Γ nil x x' σ Hx VAR) a1 σ IN1)
     (ENV.extend_map term Γ nil VAR x σ n a2 σ IN2).

Logical relation and the fundamental lemma

Now we define the logical relation. It is defined by induction on the structure of types, in a standard way. Note that alpha congruence is explicitly built-in.
Fixpoint LR (τ:ty) : term nil τ -> (cxt nil U (tydom τ)) -> Prop :=
  match τ as τ' return term nil τ' -> (cxt nil U (tydom τ')) -> Prop
  with
  | ty_bool => fun m h =>
        exists b:bool, m = tbool nil b /\ h flat_elem' b
  | ty_arrow σ σ => fun m h =>
        forall n h',
          LR σ n h' -> n -> semvalue h' ->
          semvalue (strict_app' h, h' ) ->
          exists z1 z2,
            eval _ _ (mn) z1 /\
            alpha_cong nil nil σ z1 z2 /\
            LR σ z2 (strict_app' h, h')
  end.

The logical relation respects hom equality.
Lemma LR_equiv τ : forall m h h',
  h h' -> LR τ m h -> LR τ m h'.

The logical relation respects alpha congruence.
Lemma LR_alpha_cong τ : forall m1 m2 h,
  alpha_cong nil nil τ m1 m2 ->
  LR τ m1 h -> LR τ m2 h.

If the supremum of a set of closed denotations is a semantic value, there exists some value denotation in the set.
The logical relation is closed under the directed suprema of semantic values. This is key for proving the fundamental lemma case for fixpoints.
Lemma LR_admissible τ :
  forall m (XS:dirset (PLT.homset_cpo _ _ (U (tydom τ)))),
  semvalue (XS) ->
  (forall x, x XS -> semvalue x -> LR τ m x) -> LR τ m (XS).

The fundamental lemma states that every term stands in the logical relation (up to alpha congruence) with its denotation when applied to related substitutions.
This lemma is the linchpin of the adequacy proof.
Lemma fundamental_lemma : forall Γ τ (m:term Γ τ)
  (VAR:ENV.varmap term Γ nil) (VARh : cxt nil cxt Γ),
  (forall a σ (H:inenv Γ a σ),
       semvalue (castty H proj Γ a VARh) ->
       exists z,
         (VAR a σ H z) /\
         LR σ z (castty H proj Γ a VARh)) ->
  semvalue (m VARh) ->
  exists z,
    eval nil τ (term_subst Γ nil τ VAR m) z /\
    LR τ z (m VARh ).

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

Contextual equivalance and adequacy

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 τ : env -> ty -> Type :=
  | cxt_top : context τ nil τ
  | cxt_if : forall Γ σ,
                    term Γ σ ->
                    term Γ σ ->
                    context τ Γ σ ->
                    context τ Γ ty_bool
  | cxt_appl : forall Γ σ σ,
                    term Γ σ ->
                    context τ Γ σ ->
                    context τ Γ (σ σ)
  | cxt_appr : forall Γ σ σ,
                    term Γ (σ σ) ->
                    context τ Γ σ ->
                    context τ Γ σ
  | cxt_fix : forall Γ (x:atom) σ,
                    context τ Γ σ ->
                    context τ ((x,σ)::Γ) σ

  | cxt_lam : forall Γ (x:atom) σ σ,
                    context τ Γ (σ σ) ->
                    context τ ((x,σ)::Γ) σ.

Fixpoint plug τ Γ σ (C:context τ Γ σ) : term Γ σ -> term nil τ :=
  match C in context _ Γ' σ' return term Γ' σ' -> term nil τ with
  | cxt_top => fun x => x
  | cxt_if Γ σ y z C' => fun x => plug τ _ _ C' (tif Γ σ x y z)
  | cxt_appl Γ σ σ t C' => fun x => plug τ _ _ C' (tapp x t)
  | cxt_appr Γ σ σ t C' => fun x => plug τ _ _ C' (tapp t x)
  | cxt_lam Γ a σ σ C' => fun x => plug τ _ _ C' (tlam Γ a σ σ x)
  | cxt_fix Γ a σ C' => fun x => plug τ _ _ C' (tfix Γ a σ x)
  end.

Definition cxt_eq τ Γ σ (m n:term Γ σ):=
  forall (C:context τ Γ σ) (z:term nil τ),
    eval nil τ (plug τ Γ σ C m) z <-> eval nil τ (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 a term fails to evaluate iff its denotation is ⊥.
Corollary denote_bottom_nonvalue : forall τ (m:term nil τ),
  (~exists z, eval nil τ 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.