===============================
* Explicitly Monadic F* (EMF*)
===============================

       A dependently typed, monadic language, (inspired by) a subset of F*

============
EMF* Syntax:
============

//predicative universe hierarchy
u ::= Z
   |  1 + u

   max u u' = if u >= u' then u else u'

T ::= unit                               // unit type constant
   | Type_u
   | prod | pair | fst | snd            // products
   | sum | inl | inr                    // sums

wp, t, e ::= x | a                             -- where x and a are both variables
          |  T
	  |  x:t1{t2}
          |  x:t -> C
          |  fun (x:t) -> e
          |  e1 e2
          |  case (e as y) x.e1 y.e2 returns t     -- dependent sum elimination
          |  run e                                 -- "reify" for pure terms
          |  reify e
          |  reflect e
          |  M.return t e                          -- written explicitly
          |  M.bind t1 t2 wp1 e1 wp2 x.e2
          |  M.lift_M' t wp e
          |  M.a ts                                -- fully applied actions

Notation: M.a stands for action, nothing to do with type variables (a)

Notation: We write Type0 for Type_Z and Type1 for Type_(1 + Z).

Computation type:
 C  ::= Tot t                     -- used to break circularity
      | Pure t wp
      | F t wp                    -- user-defined effects

Effect label:
 M  in {Pure, F}

Contexts:
        G ::= . | G, x:t

Effect definition:
        //Pure is axiomatized
        Pure_wp = \a:Type0. (a -> Type0) -> Type0
        PD  := Pure (a:Type0) (wp:Pure_wp a) {
                   return_wp:(a:Type0 -> x:a -> Pure_wp a) = fun a x p. p x

                   bind_wp: (a:Type0 -> b:Type0 -> wp1:Pure_wp a ->
                                                   wp2:(x:a -> Pure_wp b) -> Pure_wp b)
                          = fun a b wp1 wp2 p. wp1 (fun x. (wp2 x) p)
        }

        D ::= PD
	   //derived from source definitions
	   |  F (a:Type0) (w:t_wp a) = t a w where {
	          return  = e, wp;                 -- wps are basically e*
	          bind    = e, wp;
	          a_1 (xs_1:ts_1) : t_1 = e, wp;   -- Several actions,
	          ...
	          a_n (xs_n:ts_n) : t_n = e, wp;   -- with their types
	      }

Effect ordering: L ::= M.lift_M' = e, wp

Signature:
        S ::= S, D
	   |  S, L
	   |  PD

* Some notation:
================

   0. Implicit Tot
      x:t -> t' =def= x:t->Tot t'

   1. Currying:
      x0:t0 -> ... xn:tn -> C =def= x:t0 -> Tot ( ... -> Tot (xn:tn -> C))


   2. Projecting from an effect definition:

       Given D in S, where D = M a x = t a x with {
       	       	     	   return = e, wp
			   ...
       	       	     }

        we write    M.t         for t
        also write  M.return_e  for e
	        and M.return_wp for wp
        likewise for the other combinators


* Well-formedness of an effect definition:    (S |- D)
==========================================

     D = (F a (x:t_wp a) = t a x where { ... })

     S; . |- t_wp : a:Type0 -> Type1
     S; . |- t    : a:Type0 -> t_wp a -> Type0

     S; . |- F.return_wp : a:Type0 ->   a -> Tot (t_wp a)
     S; . |- F.return_e  : a:Type0 -> x:a -> Tot (F.t a (F.return_wp a x))

     S; . |- F.bind_wp  : a:Type0 -> b:Type0 -> t_wp a -> (a -> t_wp b) -> t_wp b
     S; . |- F.bind_e   : a:Type0 -> b:Type0
		    -> wp_f:t_wp a
		    ->    f:(F.t a wp_f)
		    -> wp_g:(a -> t_wp b)
		    ->    g:(x:a -> Tot (F.t b (wp_g x)))
		    -> Tot (F.t b (F.bind_wp a b wp_f wp_g))

     forall i. where a_i (xs_i:ts_i) : t_i = F.a_i_e, F.a_i_wp
        .; .         |- ts_i     : Type_i    //ts_i effect-free, typable in empty signature
	.; xs_i:ts_i |- t_i      : Type0
	S; xs_i:ts_i |- F.a_i_wp : t_wp t_i
	S; xs_i:ts_i |- F.a_i_e  : t t_i F.a_i_wp


     //monad laws for expressions (made complicated by the wps)
     S; a,b:Type0, x:a, wp_f:(a->t_wp b), f:(x:a-> t b (wp_f x))
       |= F.bind_e a b (F.return_wp a x) (F.return_e a x) wp_f f = f x
     S; a,b:Type0, wp_e:(t_wp a), e:(t a wp_e)
       |= F.bind_e a b wp_e e (F.return_wp a) (F.return_e a) = e
     ...

     //monad laws for wps
     // These laws should hold for Pure also, therefore using M.
     S; a,b:Type0, x:a, wp:(a->t_wp b)
       |= M.bind_wp a b (M.return_wp a x) wp <=>_M wp x  : t_wp b
     S; a,b:Type0, wp:(t_wp a)
       |= M.bind_wp a b wp (M.return_wp a)   <=>_M wp    : t_wp a
     ...

* Typing of lifts
=================

     S(M a (x:t_wp a))   = t a x  { ... }
     S(M' b (y:t_wp' b)) = t' b y { ... }
     S; . |- wp : a:Type0 -> (t_wp a) -> Tot (t_wp' a)
     S; . |- e : a:Type0 -> x:t_wp a -> f:t a x -> Tot (t' a (wp a x))
    --------------------------------------------------------------------- [WF-L]
     S; . |- M.lift_M' = e, wp

* Typing of constants
=====================

  Type_i   : Type_{1 + i}
  unit     : Type0
  prod     : Type0 -> Type0 -> Tot Type0
  pair     : a:Type0 -> b:Type0 -> a -> b -> prod a b
  fst      : a:Type0 -> b:Type0 -> prod a b -> Tot a
  snd      : a:Type0 -> b:Type0 -> prod a b -> Tot b
  sum      : Type0 -> Type0 -> Tot Type0
  inl      : a:Type0 -> b:Type0 -> a -> sum a b
  inr      : a:Type0 -> b:Type0 -> b -> sum a b

* Derived logical connectives
=============================

  squash t = _:unit{t}

  false : Type0
  false = squash (p:Type0 -> p)

  and : Type0 -> Type0 -> Tot Type0
  and a b = squash (prod a b)

  eq_i : a:Type_i -> a -> a -> Tot Type0
  eq_i a x y = squash (p:Type0 -> p x -> p y)

  forall_i : a:Type_i -> (x:a -> Tot Type0) -> Tot Type0
  forall_i a p = squash (x:a -> p x)

  p ==> q   =def=   forall p (\x. q)    with x ∉ FV(q)

  p <==> q  =def=   p ==> q /\ q ==> p


  ~p        =def=   p ==> false


  p \/ q    =def=   ~p ==> q
  
  exists (p:Type_i) (q:(x:p -> Type0)) =def= ~(forall p (\x. ~(q x)))

* Notation
===========

forall (x:a). p =def= forall a (\x. p)
exists (x:a). b =def= exists a (\x. b)


* Static judgments
** The main typing judgment (S; G |- e : C)

  Some sugar:
       S; G |- e : t    =def=    S;G |- e : Tot t

       Type_{i,i'} =def= Type_(max i i')


          |- S; G, x:t, G'
    ---------------------------- [T-Var]
     S; G, x:t, G' |- x : t


          |- S; G
    ------------------ [T-Const]
     S; G |- T : t_T


     S; G       |- t1 : Type_i
     S; G, x:t1 |- t2 : Type_j
    ----------------------------- [T-Refine]
     S; G |- x:t1{t2} : Type_i


     S; G       |- e : t1
     S; G, x:t1 |- t2 : Type_i
     S; G       |= t2[e/x]
    ----------------------------- [T-RefineI]
     S; G |- e : x:t1{t2}


     S; G      |- t : Type_i
     S; G, x:t |- C : Type_i'
    --------------------------------- [T-Arr]
     S; G |- x:t -> C : Type_{i,i'}


     S; G      |- t : Type_i
     S; G, x:t |- e : C
    ------------------------------------- [T-Abs]
     S; G |- fun (x:t) -> e : (x:t -> C)


     S; G |- e1 : Tot (x:t -> C)
     S; G |- e2 : Tot t
    ---------------------------- [T-App]
     S; G |- e1 e2 : C[e2/x]


     S; G              |- e : sum t1 t2
     S; G, y:sum t1 t2 |- t : Type0
     S; G, x:t1        |- e1 : M (t[Inl x/y]) wp1
     S; G, x:t2        |- e2 : M (t[Inr x/y]) wp2
    ------------------------------------------------------ [T-Case]
     S; G |- case (e as y) x.e1 x.e2 returns t
             : M (t[e/y]) (case (e as _) x.wp1 x.wp2 returns M.t_wp t[e/y])

     S; G              |- e  : sum t1 t2
     S; G, y:sum t1 t2 |- t  : Type_i
     S; G, x:t1        |- e1 : Tot (t[Inl x/y])
     S; G, x:t2        |- e2 : Tot (t[Inr x/y])
    ----------------------------------------------------------- [T-CaseTot]
     S; G |- case (e as y) x.e1 x.e2 returns t : Tot (t[e/y])


     S; G |- t : Type0
     S; G |- e : Tot t
    ---------------------------------------------- [T-Return]
     S; G |- M.return t e : M t (M.return_wp t e)


     S; G       |- t1 : Type0
     S; G       |- t2 : Type0           -- NOTE: t2 can't depend on x
     S; G       |- wp1: M.t_wp t1
     S; G       |- e1 : M t1 wp1
     S; G       |- wp2: x:t1 -> M.t_wp t2
     S; G, x:t1 |- e2 : M t2 (wp2 x)
    -------------------------------------------------------------------------------- [T-Bind]
     S; G |- M.bind t1 t2 wp1 e1 wp2 x.e2 : M t2 (M.bind_wp t1 t2 wp1 wp2)


     S; G |- e : Pure t wp
     S; G |= exists p. wp p  //wp should be satisfiable
     ----------------------- [T-Run]
     S; G |- run e : Tot t


     S; G |- e : F t' wp
    --------------------------------------- [T-Reify]
     S; G |- reify e : Tot (F.t t' wp)


     S; G |- e : Tot (F.t t' wp)
    ------------------------------ [T-Reflect]
     S; G |- reflect e : F t' wp


     S (M.lift_M') = _, wp_l
     S; G |- e : M t wp
    ---------------------------------------------------- [T-Lift]
     S; G |- M.lift_M' t wp e : M' t (wp_l t wp)


     S(M a x) = t a x { ... a_i (xs_i:ts_i) : t_i = e, wp ...}
     S; G |- es_i : ts_i
    --------------------------------------------------------------- [T-Action]
     S; G |- M.a_i es : M (t_i[es/xs]) (wp[es/xs])


     S; G |- e : C
     S; G |- C <: C'
    --------------------- [T-Sub]
     S; G |- e : C'


** Typing of computation types (S; G |- C : Type_i)


  ---------------------
 | S; G |- C : Type_i  | An auxiliary judgment for computation types
  ---------------------

     S; G |- t : Type_i
    ----------------------- [C-Tot]
     S; G |- Tot t : Type_i

     S; G |- t  : Type0
     S; G |- wp : Tot (M.t_wp t)
    ------------------------------ [C-M]
     S; G |- M t wp : Type0


** Sub-computations (S; G |- C <: C')

    S; G |- Pure t wp : Type_i
    S; G |- t' <: t
    S; G |= forall p:(t -> Type0). wp p ==> wp' p
    ---------------------------------------------- [S-CompPure]
    S;G |- Pure t' wp' <: Pure t wp


    S; G |- F t' wp' : Type_i
    S; G |- F.t t wp <: F.t t' wp'
    ------------------------------ [S-CompF]
    S;G |- F t wp <: F t' wp'


    S; G |- t <: t'
    ------------------------------- [S-TotTot]
    S;G |- Tot t <: Tot t'


** Sub-typing (S; G |- t <: t)


    S; G |- t' : Type_i
    t ~>* t'  \/  t' ~>* t
   --------------------------- [Sub-Conv]
    S;G |- t <: t'


    S; G |- x:t1{t2} : Type_i
   ---------------------------- [Sub-RefineL]
    S; G |- x:t1{t2} <: t1


    S; G       |- t1 <: t1'
    S; G, x:t1 |= t2
   ------------------------- [Sub-RefineR]
    S; G |- t1 <: x:t1'{t2}
 

    S; G      |- x:t -> C : Type_i    
    S; G      |- t <: t'
    S; G, x:t |- C' <: C
    --------------------------------- [Sub-Fun]
    S;G |- (x:t' -> C') <: (x:t -> C)


    S;G |- t1 <: t2
    S;G |- t2 <: t3
    ---------------- [Sub-Trans]
    S;G |- t1 <: t3


    S;G |- a <: a'
    S;G |- b <: b'
    ----------------------- [Sub-Prod]
    S;G |- a × b <: a' × b'


    S;G |- a <: a'
    S;G |- b <: b'
    ----------------------- [Sub-Sum]
    S;G |- a + b <: a' + b'


** Well-formedness of effect signature   S |- S'


   --------- [Sig-Emp]
   S |- .

   S     |- S'
   S, S' |- D
   ------------ [Sig-D]
   S |- S', D

   S     |- S'
   S, S' |- L
   ------------ [Sig-L]
   S |- S', L


** Well-formedness of type environement    S |- G

   -------- [En-Emp]
   S |- .


   S    |- G
   S; G |- t : Type_i
   x \notin dom (G)
   ------------------- [En-Bnd]
   S |- G, x:t


** Well-formedness of typing context    |- S; G


     |- S
   S |- G
   ---------- [Ctxt-WF]
   |- S; G


** Logical entailment (S; G |= t)


 .-----------.
 | S; G |= t |  Logical entailment
 .-----------.

   S; G |- e : Tot t
   ----------------- [V-Assume]
   S; G |= t


   S; G |- e : x:t1{t2}
   --------------------- [V-Refine]
   S; G |= t2[e/x]


   S; G |= a          S; G, x:a |= b            x ∉ FV(b)
   --------------------------------- [V-Bind]
   S; G |= b


   S |- e ~> e'
   S; G |- e : Tot t
   S; G |- e' : Tot t
   --------------------- [V-EqRed]
   S; G |= eq t e e'


   S; G |- e : Tot t
   ----------------- [V-EqRefl]
   S; G |= eq t e e


   S; G |= eq t a b
   ---------------- [V-EqSym]
   S; G |= eq t b a


   S; G |= eq t a b
   S; G |= eq t b c
   ---------------- [V-EqTrans]
   S; G |= eq t a c


   S; G |= eq t t1 t2
   S; G |= t1
   --------------------- [V-Eq*]
   S; G |= t2

[note: order matters. look at definition of \/]
   S;G |- a : Type0
   ----------------- [V-ExMiddle]
   S;G |= ~a \/ a


   S; G |- P : a+b -> Type0
   S; G |= ∀x:a, P (inl x)
   S; G |= ∀x:b, P (inr x)
   -------------------------------- [V-SumInd]
   S; G |= ∀x:a+b, P x


   S; G |= eq t a b
   S; G |- P : t -> t'
   ------------------------- [V-EqP]
   S; G |= eq t' (P a) (P b)


   S; G |= A
   S; G |= B
   S; G |- A : Type0
   S; G |- B : Type0
   -------------------- [V-AndIntro]
   S; G |= and A B


   S; G |= and A B
   ---------------- [V-AndElim1]
   S; G |= A


   S; G |= and A B
   ---------------- [V-AndElim2]
   S; G |= B


   S; G, x:t |= phi
   ----------------- [V-∀i]
   S; G |= ∀x:t. phi


   S; G |= ∀x:t. phi
   S; G |- e : Tot t
   ----------------- [V-∀e]
   S; G |= phi[e/x]


   S; G |= false
   S; G |- phi : Type0
   -------------------- [V-Expl]
   S; G |= phi


   S; G |- e : prod t1 t2
   ------------------------------------------------------------------ [V-ProdInv]
   S; G |- eq (prod t1 t2) e (pair t1 t2 (fst 1 t2 e) (snd t1 t2 e))


   S; G |- P1 : t -> t'
   S; G |- P2 : t -> t'
   S; G |- forall a. eq t' (P1 a) (P2 a)
   --------------------------------------- [V-Ext]
   S; G |- eq (t -> t') P1 P2



** Derived rules
*** V-MP

   S; G |= a ==> b
   S; G |= a
   ------------------------- [V-MP]
   S; G |= b


               S; G |= a ==> b
               -------------------- [WL]
               S; G, x:a |= a ==> b
               -------------------- [≡]  ----------------- [T-Var]
               S; G, x:a |= ∀_:a. b      S;G, x:a |- x : a
               ------------------------------------------- [V-∀e]
   S; G |= a               S; G, x:a |= b
   -------------------------------------- [V-Bind]
   S; G |= b


*** V-EqExp

   S |- e ~> e'
   S; G |- e : Tot t
   ----------------- [V-EqExp]
   S; G |= eq t e' e

   S |- e ~> e'      S; G |- e : Tot t
   ----------------------------------- [V-EqRed]
          S; G |= eq t e e'
          ----------------- [V-EqSym]
          S; G |= eq t e' e


*** V-ExistsIntro

   S; G      |- e : a         //P1
   S; G      |= b[e/x]        //P2
  -------------------------------- [V-ExistsIntro]
   S; G      |= exists (x:a). b


  -------------------------------------------------------------------------- [T-Var]
   S; G, z:forall a (\x. (b ==> false)) |- z : forall a (\x. (b ==> false))
  -------------------------------------------------------------------------- [V-Assume]
   S; G, z:forall a (\x. (b ==> false)) |= forall a (\x. (b ==> false))                 S; G |- e : a  (P1)
   --------------------------------------------------------------------------------------------------------- [V-foralle] (after weakening P1)
   S; G, z:forall a (\x. (b ==> false)) |= b[e/x] ==> false              S; G |= b[e/x]  (P2)
   ------------------------------------------------------------------------------------------- [V-MP] (after weakening P2)
   S; G, z:forall a (\x. (b ==> false)) |= false
   ----------------------------------------------------------- [V-foralli]
   S; G |- forall (forall a (\x. (b ==> false))) (\y. false)
   ----------------------------------------------------------- Sugaring (==> false)
   S; G |= (forall a (\x. ~b)) ==> false
   --------------------------------------- Sugaring (==> false)
   S; G |= ~ (forall a (\x. ~b))

   We show exists (x:a). b =def= ~ (forall a (\x. ~b))
   exists (x:a). b =def= exists a (\x. b)
                   =def= ~ (forall a (\y. ~ ((\x. b) y)))

*** V-Subst

   S; G |= e1 = e2
   S; G |= P[e1/x]
   ---------------
   S; G |= P[e2/x]

   Trivial by V-Red, V-Eq* and V-EqP. (Briefly: P[e1/x] = (λx.P) e1 = (λx.P) e2 = P[e2/x]).


* Dynamic semantics
===================

  A small-step, pure reduction relation,
  with respect to a signature S defining the available effects.
  Full beta-reduction.

      .--------------.
      | S |- e ~> e' |
      .--------------.


  The main guiding principle is that the semantics of the language is
  pure. In order to trigger execution of an effectful computation, you
  have to reify it to something pure and then apply it, e.g., to some
  initial state or whatever, depending on the monad. The occurrence of
  such a reify operation propagates through a term as it reduces,
  triggering the execution of sub-terms etc.

  Values: v ::= Type0
	     |  unit
	     |  and
	     |  false
	     |  ...            -- all the remaining constants
	     |  and v
	     |  and v1 v2      -- and their (partial) applications
             |  (v1, .)
	     |  (v1, v2)
	     |  inl v
	     |  inr v
	     |  fun (x:t) -> e -- lambda abstractions
	     |  x:v -> v       -- arrows

  Evaluation contexts:
	 E ::= o               -- hole
	    |  fun (x:t) -> E
	    |  E e
	    |  e E
	    |  case (E as _) x.e1 x.e2 returns t
	    |  case (e as _) x.E1 x.e2 returns t
	    |  case (e as _) x.e1 x.E2 returns t
	    |  run E
	    |  reify E
	    |  reflect E
	    |  M.return t E
	    |  M.bind t1 t2 wp_E E wp2 x.e2
	    |  M.lift_M' t wp E
            |  M.a (es .. E .. es)



     S |- e ~> e'
    -------------------- [Context]
     S |- E[e] ~> E[e']


    ------------------------------------- [Beta]
     S |- (fun (x:t) -> e) e' ~> e[e'/x]


    --------------------------- [Proj-L]
     S |- fst t1 t2 e1 e2 ~> e1


    -------------------------- [Proj-R]
     S |- snd t1 t2 e1 e2 ~> e2


     ------------------------------------------------------------ [Case-L]
     S |- case (inl e as _) x.e1 y.e2 returns t ~> e1[e/x]


    ------------------------------------------------------------ [Case-R]
     S |- case (inr e as _) x.e1 y.e2 returns t ~> e2[e/y]


    ----------------------------- [Reify-Reflect]
     S |- reify (reflect e) ~> e


    -------------------------------------- [Run-PureRet]
     S |- run (Pure.return t e) ~> e


    ---------------------------------------------- [Reify-Ret]
     S |- reify (F.return t e) ~> F.return_e t e


    ------------------------------------------------------------------------------ [PureBind]
     S |- Pure.bind t1 t2 wp1 (Pure.return t1' e1) wp2 x.e2 ~> e2[e1/x]


    --------------------------------------------------------------- [Reify-Bind]
     S |- reify (F.bind t1 t2 wp1 e1 wp2 x.e2) ~>
          F.bind_e t1 t2 wp1 (reify e1) wp2 x.(reify e2)


     S (M a x) = _ with { ... a_i (xs_i:ts_i) :t_i = e_i, wp_i ... }
     ------------------------------------------------------------- [Reify-Action]
     S |- reify (M.a_i es) ~> e_i [es/xs]

     S (M'.lift_M) = e_l, _
     -------------------------------------------------------------- [Reify-Lift]
     S |- reify (M'.lift_M t' wp' e) ~> e_l t' wp' (reify e)


====================================================


================
EMF Metatheory
================


In what follows below, we denote J for the following judgments:

S; G |- e : C
S; G |- C : Type_i
S; G |- C <: C
S; G |- t <: t'
S; G |= t

-------------------------------
Lemma: Commuting-Substitution
-------------------------------

Let x != y

(1) C[e1/x][e2/y] = C[e2/y][e1[e2/y]/x]

/\

(2) e[e1/x][e2/y] = e[e2/y][e1[e2/y]/x]

-----------------
Lemma: Weakening
-----------------

S; G,G' |- J /\ |- S; (G, x:t, G') ==> S; (G, x:t, G') |- J

------------------------------
Lemma: Reduction-substitutive
------------------------------

If S |- e1 ~> e2, then S |- e1[e/z] ~> e2[e/z]

Proof: By induction on derivation of e1 ~> e2, case analysis on the last rule.


Case [Context]:    e1 = E[e']    e2 = E[e'']
--------------------------------------------

From premise:

(1) S |- e' ~> e''

Using I.H. on (1):

(2) S |- e'[e/z] ~> e''[e/z]

Apply rule [Context] with (2), with E = E[e/z]:

(3) S |- (E[e/z])[e'[e/z]] ~> (E[e/z])[e''[e/z]]

Since (E[e'])[e/z] = E[e/z][e'[e/z]], we get the proof.


Case [Beta]:    e1 = (fun x -> e') e''    e2 = e'[e''/x]
---------------------------------------------------------

We have:

(1) e1[e/z] = (fun x -> e'[e/z]) (e''[e/z])    since z != x

Using rule [Beta],

(2) (fun x -> e'[e/z]) (e''[e/z]) ~> (e'[e/z])([e''[e/z]/x])

Using Lemma (Commuting-Substitution):

(3) e'[e/z][e''[e/z]/x] = e'[e''/x][e[e''/x]/z]

Since x does not occur free in e,

(4) e'[e/z][e''[e/z]/x] = e'[e''/x][e/z]

Substituting in (2), we have the proof.


Case [Proj-L] [Proj-R]: Immediate.
------------------------------------


Case [Case-L]:    e1 = case (inl e' as _) x.e1 y.e2 returns t    e2 = e1[e'/x]
-------------------------------------------------------------------------------

We have:

(1) e1[e/z] = case (inl e'[e/z] as _) (x.e1)[e/z] (y.e2)[e/z] returns _

Since x != z:

(2) e1[e/z] = case (inl e'[e/z] as _) x.e1[e/z] y.e2[e/z] returns _

Using rule [Case-L]:

(3) case (inl e'[e/z] as _) x.e1[e/z] y.e2[e/z] returns _ ~> e1[e/z][e'[e/z]/x]

Using Lemma (Commuting-Substitution), we can prove that e1[e/z][e'[e/z]/x] = e1[e'/x][e/z], and we have the proof.


Case [Case-R]: Similar to [Case-L].
-----------------------------------


Case [Reify-Reflect] [Run-PureRet] [Reify-Ret]: Immediate.
----------------------------------------------------------


Case [PureBind]:
-----------------

We need to reason that e2[e1/x][e/z] = e2[e/z][e1[e/z]/x]

Using Lemma (Commuting-Substitution) we get the proof.


Case [Reify-Bind]: Immediate.
------------------------------


Case [Reify-Action]:    e1 = reify (M.a_i es)    e2 = e'[es/xs]
----------------------------------------------------------------

We have:

(1) e1[e/z] = reify (M.a_i es[e/z])
(2) e2[e/z] = e'[es/xs][e/z]

We need to show e'[es[e/z]/xs] = e'[es/xs][e/z], which follows similar to case [Beta] above and using the face that z does not occur free in e'. We get the proof.


Case [Reify-Lift]: Immediate.
------------------------------


Qed.


-------------------------------
Lemma: Reduction-substitutive*
-------------------------------

If S |- e1 ~>* e2, then S |- e1[e/z] ~>* e2[e/z]


Proof: Induction on number of steps in ~>*, and using Lemma (Reduction-substitutive).


--------------------
Lemma: Substitution
--------------------

S; G |- e' : Tot t ==>

(1) S; G, x:t, G' |- e : C        ==> S; G, G'[e'/x] |- e[e'/x] : C[e'/x]

(2) S; G, x:t, G' |- C : Type_i   ==> S; G, G'[e'/x] |- C[e'/x] : Type_i

(3) S; G, x:t, G' |- C <: C'      ==> S; G, G'[e'/x] |- C[e'/x] <: C'[e'/x]

(4) S; G, x:t, G' |- t' <: t''    ==> S; G, G'[e'/x] |- t'[e'/x] <: t''[e'/x]

(5) S; G, x:t, G' |= t'           ==> S; G, G'[e'/x] |= t'[e'/x]


Proof: By mutual induction on the derivation of premises, case analysis on the last rule used.

(1)

Case [T-Var]:    e = y
-----------------------

From premise:

(6) |- S; G, x:t, G'

  - y = x. C = Tot t. x \notin FV(t) (derivable from (6)).

    To prove: S; G, G'[e'/x] |- e' : Tot t. Immediate from the premise after applying Lemma (Weakening).

  - y != x. C= Tot t'. y:t' in G.

    x \notin FV(t') (x is not free in G, and |- S; G, x:t, G')

    To prove: S; G, G'[e'/x] |- y : Tot t'. Immediate from y:t' in G, and Lemma (Weakening)

  - y != x. C = Tot t'. y:t' in G'

    To prove, S; G, G'[e'/x] |- y : Tot t'[e'/x]. Immediate from [T-Var]


Case [T-Const]:   e = T
------------------------

From premise:

(6) |- S; G, x:t, G'

x \notin FV(e) and x \notin FV(C). Conclusion follows from [T-Const] and Lemma (Weakening).


Case [T-Refine]:    e = y:t1{t2}    C = Type_i
-----------------------------------------------

From premises:

(6) S; G, x:t, G'       |- t1 : Type_i
(7) S; G, x:t, G', y:t1 |- t2 : Type_j

Using I.H. (1) on (6) and (7):

(8) S; G, G'[e'/x]             |- t1[e'/x] : Type_i
(9) S; G, G'[e'/x], y:t1[e'/x] |- t2[e'/x] : Type_j

Using [T-Refine] with (8) and (9):

S; G, G'[e'/x] |- y:t1[e'/x]{t2[e'/x]} : Type_i

We have the proof.


Case [T-RefineI]:    C = Tot (y:t1{t2})
---------------------------------------

From premises:

(6) S; G, x:t, G'       |- e : t1
(7) S; G, x:t, G', y:t1 |- t2 : Type_i
(8) S; G, x:t, G'       |= t2[e/y]

Applying I.H. on (6), (7), and (8):

(8)  S; G, G'[e'/x]             |- e[e'/x] : t1[e'/x]
(9)  S; G, G'[e'/x], y:t1[e'/x] |- t2[e'/x] : Type_i
(10) S; G, G'[e'/x]             |= t2[e/y][e'/x]

Using Lemma (Commuting-Substitution) on (10):

(11) S; G, G'[e'/x] |= t2[e'/x][e[e'/x]/y]

Using rule [T-RefineI] on (8), (9), and (11):

(12) S; G, G'[e'/x] |- e[e'/x] : x:t1[e'/x]{t2[e'/x]}

We get the proof.


Case [T-Arr]:    e = y:t' -> C'    C = Type_{i, i'}
----------------------------------------------------

From premises:

(6) S; G, x:t, G'       |- t' : Type_i
(7) S; G, x:t, G', y:t' |- C' : Type_i'

Using I.H. (1) with (6):

(8) S; G, G'[e'/x] |- t'[e'/x] : Type_i

Using I.H. (2) with (7):

(9) S; G, G'[e'/x], y:t'[e'/x] |- C'[e'/x] : Type_i'

Apply [T-Arr] with (8) and (9) for the conclusion.


Case [T-App]:    e = e1 e2    C = C'[e2/y]
-------------------------------------------

From premises:

(6) S; G, x:t, G' |- e1 : Tot (y:t' -> C')
(7) S; G, x:t, G' |- e2 : Tot t'

To prove: S; G, G'[e'/x] |- e1[e'/x] e2[e'/x] : (C'[e2/y])[e'/x]

Using I.H. (1) with (6) and (7), and applying [T-App], we get:

(8) S; G, G'[e'/x] |- e1[e'/x] e2[e'/x] : (C'[e'/x])[e2[e'/x]/y]

So, we need to show: (C'[e2/y])[e'/x] = (C'[e'/x])[e2[e'/x]/y], which follows from Lemma (Commuting-Substitution).


Case [T-Case]:    e = case (e as y) z.e1 z.e2 returns t'    C = M (t'[e/y]) (case (e as _) \z.wp1 \z.wp2 returns M.t_wp t'[e/y]
--------------------------------------------------------------------------------------------------

From premises:

(6) S; G, x:t, G'              |- e : sum t1 t2
(7) S; G, x:t, G', y:sum t1 t2 |- t' : Type_i
(8) S; G, x:t, G', z:t1        |- e1 : M (t'[Inl z/y]) wp1
(9) S; G, x:t, G', z:t2        |- e2 : M (t'[Inr z/y]) wp2

Applying I.H. on (6), (7), (8), and (9):

(10) S; G, G'[e'/x]                          |- e[e'/x] : sum t1[e'/x] t2[e'/x]
(11) S; G, G'[e'/x], y:sum t1[e'/x] t2[e'/x] |- t'[e'/x] : Type_i
(12) S; G, G'[e'/x], z:t1[e'/x]              |- e1[e'/x] : M (t'[Inl z/y][e'/x]) wp1[e'/x]
(13) S; G, G'[e'/x], z:t2[e'/x]              |- e2[e'/x] : M (t'[Inr z/y][e'/x]) wp2[e'/x]

Using rule [T-Case] with (10), (11), (12), and (13):

(14) S; G, G'[e'/x] |- case (e[e'/x] as y) z.(e1[e'/x]) z.(e2[e'/x]) returns t'[e'/x]
                       : M (t'[e'/x][e[e'/x]/y]) (case (e[e'/x] as _) \z.(wp1[e'/x]) \z.(wp2[e'/x]) returns M.t_wp t[e'/x][e[e'/x]/y])

We need to prove that:

S; G, G'[e'/x] |- case (e[e'/x] as y) (z.e1)[e'/x] (z.e2)[e'/x] returns t'[e'/x]
                  : M (t'[e/y][e'/x]) (case (e[e'/x] as _) (\z.wp1)[e'/x] (\z.wp2)[e'/x] returns M.t_wp t'[e'/y][e'/x]

We have:

(15) (z.e1)[e'/x]   = z.e1[e'/x]          since x != z, z is not free in e'
(16) (z.e2)[e'/x]   = z.e2[e'/x]          since x != z, z is not free in e'
(17) t'[e/y][e'/x]  = t'[e'/x][e[e'/x]/y] by Lemma (Commuting-Substitution)
(18) (\z.wp1)[e'/x] = \z.wp1[e'/x]        since x != z, z is not free in e'
(19) (\z.wp2)[e'/x] = \z.wp2[e'/x]        since x != z, z is not free in e'

Using (15), (16), (17), (18), and (19) on (14), we have the proof.


Case [T-CaseTot]:    e = case (e as y) z.e1 z.e2 returns t'    C = Tot t'[e/y]
-------------------------------------------------------------------------------

From premises:

(6) S; G, x:t, G'              |- e  : sum t1 t2
(7) S; G, x:t, G', y:sum t1 t2 |- t  : Type_i
(8) S; G, x:t, G', z:t1        |- e1 : Tot (t'[Inl z/y])
(9) S; G, x:t, G', z:t2        |- e2 : Tot (t'[Inr z/y])

Using I.H. on (6), (7), (8), and (9):

(10) S; G, G'[e'/x]                          |- e[e'/x]  : sum t1[e'/x] t2[e'/x]
(11) S; G, G'[e'/x], y:sum t1[e'/x] t2[e'/x] |- t[e'/x]  : Type_i
(12) S; G, G'[e'/x], z:t1[e'/x]              |- e1[e'/x] : Tot (t'[Inl z/y][e'/x])
(13) S; G, G'[e'/x], z:t2[e'/x]              |- e2[e'/x] : Tot (t'[Inr z/y][e'/x])

Since x does not occur free in Inl z and Inr z, we have using Lemma (Commuting-Substitution):

(14) t'[Inl z/y][e'/x] = t'[e'/x][Inl z/y] 
(15) t'[Inr z/y][e'/x] = t'[e'/x][Inr z/y]

Using (10), (11), (12), (13), (14), and (15), and applying [T-TotCase]:

(16) S; G, G'[e'/x] |- case (e[e'/x] as y) z.e1[e'/x] z.e1[e'/x] returns t[e'/x] : Tot (t'[e'/x][e/y])

We have (z.e1)[e'/x] = z.e1[e'/x] and similarly for z.e2.

So, we need to prove: t'[e/y][e'/x] = t'[e'/x][e/y]

Consider t'[e'/x][e/y]. Using Lemma (Commuting-Substitution):

(17) t'[e'/x][e/y] = t'[e/y][e'[e/y]/x]

Since y is fresh, it does not occur free in e'. Thus, we have the proof.


Case [T-Return]:    e = M.return t' e    C = M t' (M.return_wp t' e)
--------------------------------------------------------------------

From premises:

(6) S; G, x:t, G' |- t' : Type0
(7) S; G, x:t, G' |- e  : Tot t'

Applying I.H. on (6) and (7), and then applying [T-Return] again we have the proof.


Case [T-Bind]:    e = M.bind t1 t2 wp1 e1 wp2 x.e2    C = M t2 (M.bind_wp t1 t2 wp1 wp2)
-----------------------------------------------------------------------------------------

Similar to [T-Return].


Case [T-Run]:    e = run e    C = Tot t'
-----------------------------------------

From premises:

(6) S; G, x:t, G' |- e : Pure t' wp
(7) S; G, x:t, G' |= exists p. wp p

Using I.H. (1) on (6) and (5) on (7), and then applying [T-Run] again, we have the proof.


Case [T-Reify] [T-Reflect] [T-Lift]: Application of I.H. on premises.
-----------------------------------------------------------------------


Case [T-Action]:    e = M.a_i es    C = M t_i wp[es/xs]
--------------------------------------------------------

From premises:

(6) ts_i effect-free
(7) S(M a x) = t a x { ... a_i (xs_i:ts_i) : t_i = e, wp ... }
(8) S; G, x:t, G' |- es : ts_i

Using I.H. on (8) we get:

(9)S; G, G'[e'/x] |- es[e'/x] : ts_i    since x is not free in ts_i

Applying [T-Action] with (6), (7), and (9), we get:

(10) S; G, G'[e'/x] |- M.a_i es[e'/x] : M t_i (wp[es[e'/x]/xs])

We need to prove: S; G, G'[e'/x] |- M.a_i es[e'/x] : M t_i (wp[es/xs])[e'/x]    again, x is not free in t_i

Consider (wp[es/xs])[e'/x]. Using Lemma (Commuting-Substitution),

(11) (wp[es/xs])[e'/x] = (wp[e'/x])[es[e'/x]/xs]

And since x is not free in wp,

(12) (wp[e'/x])[es[e'/x]/xs] = wp[es[e'/x]/xs]

Using (10) and (12), we have the proof.


Case [T-Sub]:
-------------

From premises:

(6) S; G, x:t, G' |- e : C'
(7) S; G, x:t, G' |- C' <: C

Applying I.H. (1) on (6) and (3) on (7), we get the proof.


Qed.

(2)

Case [C-Tot]:    C = Tot t'
---------------------------

From premise:

(6) S; G, x:t, G' |- t' : Type_i

Apply I.H. (1) on (6), and then rule [C-Tot] to get the proof.


Case [C-M]: Similar to [C-Tot].
-------------------------------


Qed.

(3)

Case [S-CompPure]:    C = Pure t' wp'    C' = Pure t'' wp''
------------------------------------------------------------

From premises:

(6) S; G, x:t, G' |- Pure t'' wp'' : Type_i
(7) S; G, x:t, G' |- t' <: t''
(8) S; G, x:t, G' |= forall p:(t -> Type0). wp'' p ==> wp' p

Apply I.H. on (6), (7), and (8), and then apply rule [S-CompPure] to get the proof.


Case [S-CompF] [S-TotTot]: Similar to [S-CompPure].
----------------------------------------------------


Qed.

(4)

Case [Sub-Conv]:
-----------------

From the premises:

(6) S; G, x:t, G' |- t'' : Type_i
(7) t' ~>* t'' \/ t'' ~>* t'

Apply I.H. (1) on (6), Lemma (Reduction-substitutive*) on (7), and rule [Sub-Conv] to get get the proof.


Case [Sub-RefineL]:    t' = y:t1{t2}    t'' = t1
-------------------------------------------------

Using [Sub-RefineL] on substituted types we get the proof.


Case [Sub-RefineR]:    t' = t1    t'' = y:t1'{t2}
--------------------------------------------------

From premises

(6) S; G, x:t, G'       |- t1 <: t1'
(6) S; G, x:t, G', y:t1 |= t2

Applying I.H. on (6) and (7) and using [Sub-RefineR] on the substituted types we get the proof.


Case [Sub-Fun]:    t' = y:t' -> C'    t'' = y:t'' -> C''
------------------------------------------------------

From the premises:

(6) S; G, x:t, G'        |- y:t'' -> C'' : Type_i
(7) S; G, x:t, G'        |- t'' <: t'
(8) S; G, x:t, G', y:t'' |- C' <: C''

Use I.H. on (6), (7), and (8), and then use rule [Sub-Fun] to get the proof.


Case [Sub-Trans] [Sub-Prod] [Sub-Sum]: Immediate applications of I.H.
----------------------------------------------------------------------


Qed.

(5)

Case [V-Assume]:
----------------

From premise:

(6) S; G, x:t, G' |- e' : Tot t'

Use I.H. (1) on (6) and apply [V-Assume] again to get the proof.


Case [V-Refine]:    t' = t2[e/y]
---------------------------------

From premise:

(6) S; G, x:t, G' |- e : y:t1{t2}

Using I.H. on (6), we get:

(7) S; G, G'[e'/x] |- e[e'/x] : y:t1[e'/x]{t2[e'/x]}

Applying [V-Refine] on (7):

(8) S; G, G'[e'/x] |- t2[e'/x][e[e'/x]/y]

Using Lemma (Commuting-Substitution) we have t2[e'/x][e[e'/x]/y] = t1[e/y][e'/x] and we get the proof.


Case [V-Bind] [V-EqRed] [V-EqRefl] [V-EqSym] [V-EqTrans] [V-ExMiddle] [V-SumInd] [V-EqP] [V-AndIntro] [V-AndElim1] [V-AndElim2] [V-foralli]: Immediate applications of I.H.
-----------------------------------------------------------------------------------------------------


Case [V-foralle]:    t' = phi[e/y]
-----------------------------------

From premises:

(6) S; G, x:t, G' |= forall (y:t'). phi
(7) S; G, x:t, G' |- e : Tot t'

Using I.H. on (6) and (7):

(8) S; G, G'[e'/x] |= forall (y:t'[e'/x]). phi[e'/x]
(9) S; G, G'[e'/x] |= e[e'/x] : Tot t'[e'/x]

Using [V-foralle] with (8) and (9):

(10) S; G, G'[e'/x] |= phi[e'/x][e[e'/x]/y]

Using Lemma (Commuting-Substitution), we get phi[e'/x][e[e'/x]/y] = phi[e/y][e'/x], which we can substitute in (10) to get the proof.


Case [V-Expl]: Immediate from I.H.
------------------------------------


Qed.


-------------------------
Lemma: Derived-judgments
-------------------------

(1) S; G |- e : C      ==> |- S; G /\ S; G |- C : Type_i

(2) S; G |- C : Type_i ==> |- S; G

(3) S; G |- C <: C'    ==> |- S; G /\ S; G |- C' : Type_i   //see if we need property of C

(4) S; G |- t <: t'    ==> |- S; G /\ S; G |- t' : Type_i   //see if we need property of t

(5) S; G |= t          ==> |- S; G /\ S; G |- t : Type_i


Proof: By mutual induction on the typing derivation of the premises. Case analysis on the last rule used.

(1):

Case [T-Var]:    e = x    C = Tot t where G = G1, x:t, G2
---------------------------------------------------------

|- S; G follows from the premise of [T-Var].
S; G |- C : Type_i follows from [C-Tot] and |- S; G.


Case [T-Refine]:    e = x:t1{t2}    C = Type_i
-----------------------------------------------

Applying I.H. on the first premise we get |- S; G.

Use typing of constant Type_i to get the proof.


Case [T-RefineI]: Applying I.H. on premises gives us the proof.
----------------------------------------------------------------


Case [T-Const]:    e = c    C = Tot (T_c)
------------------------------------------

|- S; G follows from the premise of [T-Const]
S; G |- C : Type_i follows from inspection of types of constants.


Case [T-Arr]:    e = x:t -> C'    C = Type_{i, i'}    
--------------------------------------------------

From premises:

(6) S; G |- t : Type_i
(7) S; G, x:t |- C' : Type_i' 

|- S; G follows from I.H. on (6).
S; G |- C : Type_j follows with typing of constant Type_{i, i'}.


Case [T-Abs]:    e = fun (x:t) -> e'    C = x:t -> C'
-----------------------------------------------------

From premises:

(6) S; G |- t : Type_i
(7) S; G, x:t |- e : C'    

|- S; G follows from I.H. on (6).

Using I.H. on (7), we get:

(8) S; G, x:t |- C' : Type_j

To derive S; G |- C : Type_i, use [T-Arr] with (6) and (8).


Case [T-App]:    e = e1 e2    C = C'[e2/x]
-------------------------------------------

From premises:

(6) S; G |- e1 : Tot (x:t -> C')
(7) S; G |- e2 : Tot t

|- S; G follows from I.H. (1) on (6). Also, with I.H. (1) on (6):

(8) S; G |- Tot (x:t -> C') : Type_i

The only rule that's possible for (8) is [C-Tot], inverting that:

(9) S; G |- x:t -> C' : Type_i

Inverting [T-Arr] on (9):  (here [T-Sub] is also possible, so we should prove this as a separate lemma)

(10) S; G, x:t |- C' : Type_j for some j

Apply Lemma (Substitution) with (7) and (10) to get S; G |- C'[e2/x] : Type_j, which completes the proof.


Case [T-Case]:    e = case (e as y) x.e1 x.e2 returns t    C = M (t[e/y]) (case (e as _) \x.wp1 \x.wp2 return M.t_wp t[e/y])
-----------------------------------------------------------------------------------------------------

From the premises:

(6) S; G              |- e : sum t1 t2
(7) S; G, y:sum t1 t2 |- t : Type0
(8) S; G, x:t1        |- e1 : M (t[Inl x/y]) wp1
(9) S; G, x:t2        |- e2 : M (t[Inr x/y]) wp2

|- S; G follows from I.H. (1) on (6).

We need to prove: S; G |- M (t[e/y]) (case (e as _) \x.wp1 \x.wp2 return M.t_wp t[e/y]) : Type_i

We will apply rule [C-M], but first we need to prove its premises.

For wp, we need to prove: S; G |- (case (e as _) \x.wp1 \x.wp2 return M.t_wp t[e/y]) : M.t_wp (t[e/y])

Consider (8). Apply I.H. (1) on (8) to get:

(10) S; G, x:t1 |- M (t[Inl x/y]) wp1 : Type_j

Invert [C-M] on (10) to get:

(11) S; G, x:t1 |- wp1 : M.t_wp (t[Inl x/y])

Similarly, considering (9), we get:

(12) S; G, x:t2 |- wp2 : M.t_wp (t[Inr x/y])

Using Lemma (Substitution) with (6) and (7):

(13) S; G |- t[e/y] : Type0

Since M.t_wp: Type0 -> Type1, we get:

(14) S; G |- M.t_wp t[e/y] : Type1

Apply [T-CaseTot] with (6), (14), (11), and (12), to get:

(15) S; G |- (case (e as _) \x.wp1 \x.wp2 return M.t_wp t[e/y]) : M.t_wp (t[e/y])

Finally, apply [C-M] with (13) and (15) to get the proof.


Case [T-CaseTot]:    e = case (e as y) x.e1 x.e2 returns t    C = Tot t[e/y]
-----------------------------------------------------------------------------

From premises:

(6) S; G              |- e  : sum t1 t2
(7) S; G, y:sum t1 t2 |- t  : Type_i
(8) S; G, x:t1        |- e1 : Tot (t[Inl x/y])
(9) S; G, x:t2        |- e2 : Tot (t[Inr x/y])

Using I.H. (1) on (6), we get |- S; G

Using Lemma (Substitution) on (6) and (7):

(10) S; G |- t[e/y] : Type_i

Use [C-Tot] with (10) to get the rest of the proof.


Case [T-Return]:    e = M.return t e    C = M t (M.return_wp t e)
------------------------------------------------------------------

From premises:

(6) S; G |- t : Type0
(7) S; G |- e : Tot t

Using I.H. (1) on (6), we get |- S; G.

Since M.return_wp : a:Type0 -> a -> Tot (M.t_wp a), we have:

(8) S |- M.return_wp t e : Tot (M.t_wp a)

Apply [C-M] with (6) and (7) to get the proof.


Case [T-Bind]:    e = M.bind t1 t2 wp1 e1 wp2 x.e2    C = M t2 (M.bind_wp t1 t2 wp1 wp2)
-----------------------------------------------------------------------------------------

From premises:

(6)  S; G       |- t1  : Type0
(7)  S; G       |- t2  : Type0
(8)  S; G       |- wp1 : M.t_wp t1
(9)  S; G       |- e1  : M t wp1
(10) S; G       |- wp2 : x:t1 -> M.t_wp t2
(11) S; G, x:t1 |- e2  : M t2 (wp2 x)

Using I.H. (1) on (6), we get |- S; G.

Since M.bind_wp : a:Type0 -> b:Type0 -> t_wp a -> (a -> t_wp b) -> t_wp b, we get:

(12) S; G |- M.bind_wp t1 t2 wp1 wp2 : M.t_wp t2

Using I.H. (1) on (9):

(13) S; G |- M t wp1 : Type_i

Using I.H. (1) on (11):

(15) S; G |- x:t1 -> M t2 (wp2 x) : Type_j

Inverting [T-Arr], note that T-Sub would also give us the following:

(16) S; G, x:t1 |- M t2 (wp2 x) : Type_j'

Apply [C-M] with (7), (12) to get the proof.


Case [T-Run]:    e = run e    C = Tot t
----------------------------------------

From premises:

(6) S; G |- e : Pure t wp
(7) S; G |= exists p. wp p

Using I.H. (1) on (6), we get |- S; G. Also, we get:

(8) S; G |- Pure t wp : Type_i

Inverting [C-M]:

(9) S; G |- t : Type0

Use [C-Tot] with (9) to get the proof.


Case [T-Reify]:    e = reify e    C = Tot (F.t t' wp)
------------------------------------------------------

From premise:

(6) S; G |- e : F t' wp

Using I.H. (1) on (6), we get |- S; G, and also:

(7) S; G |- F t' wp : Type_i

Inverting [C-M] on (7):

(8) S; G |- t' : Type0
(9) S; G |- wp : Tot (F.t_wp t')

Since F.t : a:Type0 -> t_wp a -> Type0, we get:

(10) S; G |- F.t t' wp : Type0

Use [C-Tot] with (10) to get the proof.


Case [T-Reflect]:    e = reflect e    C = F t' wp
--------------------------------------------------

From premise:

(6)  S; G |- e : Tot (F.t t' wp)

Using I.H. (1) on (6), we get |- S; G, and:

(7) S; G |- Tot (F.t t' wp) : Type_i

Inverting [C-Tot] on (7):

(8) S; G |- F.t t' wp : Type_i

Since F.t : a:Type0 -> t_wp a -> Type0, we get:

(9)  S; G |- t' : Type0
(10) S; G |- wp : F.t_wp t'

Apply [C-M] with (9) and (10) to get the proof.


Case [T-Lift]:    e = M.lift_M' t wp e    C = M' t (M.lift_M'_wp t wp)
----------------------------------------------------------------------

From premises:

(6) S; G |- e : M t wp

Using I.H. (1) on (6), we get |- S; G, and:

(7) S; G |- M t wp : Type_i

Inverting [C-M] on (7):

(8)  S; G |- t  : Type0
(9)  S; G |- wp : M.t_wp t

Since M.lift_M'_wp: a:Type0 -> M.t_wp a -> Tot (M'.t_wp a), we get:

(11) S; G |- M.lift_M'_wp t wp : Tot (M'.t_wp a)

Apply [C-M] with (8) and (11) above to get the proof.


Case [T-Action]:    e = M.a_i es    C = M t_i[es/xs_i] wp[es/xs_i]
------------------------------------------------------------------

From premises:

(6) S(M a x) = t a x { ... a_i (xs_i:ts_i) : t_i = e, wp ... }
(7) S; G |- es : ts_i

Using I.H. (1) on (7), we get |- S; G.

From signature typing:

(8)  S; G, xs_i:ts_i |- t_i : Type0
(9)  S; G, xs_i:ts_i |- wp  : M.t_wp t_i

Using Lemma (Substitution) with (7), we can derive from (8), (9), and (9'):

(10) S; G |- t_i[es/xs_i] : Type0
(11) S; G |- wp[es/xs_i]  : M.t_wp (t_i[es/xs_i])

Apply [C-M] to get the proof.


Case [T-Sub]:
--------------

From premises:

(6) S; G |- e : C'
(7) S; G |- C' <: C

Using I.H. (1) on (6), we get |- S; G.

Apply I.H. (3) on (7) to get the proof.


Qed.

(2)

Case [C-Tot]:    C = Tot t
---------------------------

From premise:

(6) S; G |- t : Type_i

Apply I.H. (1) on (6) to get |- S; G.


Case [C-M]: Similar. Apply I.H. to first premise.
--------------------------------------------------


Qed.

(3)

Case [S-CompPure]:    C = Pure t' wp'    C' = Pure t wp
---------------------------------------------------------

From premises:

(6) S; G |- Pure t wp : Type_i
(7) S; G |- t' <: t
(8) S; G |= forall p. wp p ==> wp' p

Apply I.H. (4) on (7) to get |- S; G.

Proof follows from (6).


Case [S-CompF] [S-TotTot]: Similar from I.H.
---------------------------------------------


Qed.


(4)

Case [Sub-Conv]: Applying I.H. on premise and using the premise itself, we get the proof.
------------------------------------------------------------------------------------------


Case [Sub-RefineL]:
--------------------

Applying I.H. on the premise we get |- S; G.

Invert [T-Refine] on the premise to get the proof. (Note that with [T-Sub] we get the same result, as Type_i is a subtype of only itself.)


Case [Sub-RefineR]:    t = t1    t' = x:t1'{t2}
-----------------------------------------------

From premises:

(6) S; G       |- t1 <: t1'
(7) S; G, x:t1 |= t2

Applying I.H. on the premises and using [T-Refine] after that we get the proof.


Case [Sub-Fun]: Similar to [Sub-Conv].
--------------------------------------


Case [Sub-Trans]: Apply I.H. we get the proof.
-----------------------------------------------


Case [Sub-Prod] [Sub-Sum]: Apply I.H. and then using typing of constants prod and sum.
---------------------------------------------------------------------------------------


Qed.


(5)

Case [V-Assume]:
----------------

From premise:

(6) S; G |- e : Tot t

Using I.H. (1) on (6) and then inverting [C-Tot], we get the proof.


Case [V-Refine]:
-----------------

Applying I.H. on the premise we get |- S; G, and:

(6) S; G |- x:t1{t2} : Type_i

Inverting rule [T-Refine] on (6) we get:

(7) S; G, x:t1 |- t2 : Type_j

Using rule [Sub-RefineL] with (6) to get:

(8) S; G |- x:t1{t2} <: t1

Using rule [S-TotTot] with (8) to get:

(9) S; G |- Tot (x:t1{t2}) <: Tot t1

Using rule [T-Sub] with premise and (9):

(10) S; G |- e : Tot t1

Using Lemma (Substitution) with (10) and (7) we get the proof.


Case [V-Bind]:
---------------

From premises:

(6) S; G |= a
(7) S; G, x:a |= b
(8) x not free in b

Using I.H. (5) on (6), we get |- S; G.

Also from I.H. (5) on (6), we get:

(9) S; G, x:a |- b : Type_i

Using (8), we get the proof.


Case [V-EqRed]:    t = eq t e e'
---------------------------------

Applying I.H. on premises, we get |- S; G and rest follows from typing of eq.


Case [V-EqRefl] [V-EqSym] [V-EqTrans]: Applying I.H. gives us the proof.
-------------------------------------------------------------------------

Case [V-ExMiddle]: Using I.H. we get |- S; G and using constant typing to type ((a ==> false) ==> false) ==> a gives us the proof.
---------------------------------------------------------------------------------------

Case [V-SumInd]:
-----------------

From premises:

(6) S; G |- P : a+b -> Type0

Using I.H. (1) on (6) we get |- S; G, and:

(7) S; G |- a+b -> Type0 : Type_i

Invert [T-Arr] on (7):

(8) S; G |- a+b : Type_j

Using typing of constant forall, we can derive the typing of forall (x:a+b). P x and get the proof.


Case [V-EqP]:
--------------

From premises:

(6) S; G |= eq t a b
(7) S; G |- P : t -> t'

Using I.H. on (6) we get |- S; G, and:

(8) S; G |- eq t a b : Type_i

Inverting typing of constant eq:

(9)  S; G |- t : Type_j
(10) S; G |- a : t
(11) S; G |- b : t

Using constant typing for eq, we get the proof.


Case [V-AndIntro] [V-AndElim1] [V-AndElim2]: Using I.H. and typing for constant and.
-------------------------------------------------------------------------------------


Case [V-foralli]:
------------------

From premise:

(6) S; G, x:t |= phi

Using I.H. on (6) we get:

(7) |- S; G, x:t
(8) S; G, x:t |- phi : Type_i

From (7), we can derive:

(9)  |- S; G
(10) S; G |- t : Type_j

Using typing of constant forall, we have the proof.


Case [V-foralle]:
-----------------

From premises:

(6) S; G |= forall t (\x. phi)
(7) S; G |- e : Tot t

Using I.H. on (7), we get |- S; G.

Inverting typing of constant forall on (6):

(8) S; G, x:t |- phi : Type0

Using Lemma (Substitution) on (7) and (8), we have the proof.


Case [V-Expl]: Immediate from the premise.
-------------------------------------------


Qed.


-------------------------------
Lemma: Reflexivity-of-sub-comp
-------------------------------

S; G |- C <: C


-------------------------------
Lemma: Transitivity-of-sub-comp
-------------------------------

If

(1) S; G |- C1 <: C2
(2) S; G |- C2 <: C3

then

(a) S; G <: C1 <: C2


--------------------------
Lemma: Strengthen-binding
--------------------------

S; G |- t' : Type_i /\ S; G |- t' <: t

==>

(1) S; G, x:t, G' |- e : C      ==> S; G, x:t', G' |- e : C

(2) S; G, x:t, G' |- C : Type_i ==> S; G, x:t', G' |- C : Type_i

(3) S; G, x:t, G' |- C <: C'    ==> S; G, x:t', G' |- C <: C'

(4) S; G, x:t, G' |- t <: t'    ==> S; G, x:t', G' |- t <: t'

(5) S; G, x:t, G' |= t          ==> S; G, x:t', G' |= t


--------------------------------
Lemma: Inversion-of-sub-refiner
--------------------------------

If

(1) S; G      |- y:(x:t -> C){y = fun x:t -> e1} <: x:t1 -> C1

then

(a) S; G       |- t1 <: t
(b) S; G, x:t1 |- C  <: C1


---------------------------
Lemma: Ret-Pure-is-weakest
---------------------------

forall S, G, t, e, wp.

(1) S; G |- Pure.return t e : Pure t' wp'

==>

(a) S; G |- t : Type0
(b) S; G |- e : Tot t
(c) S; G |- t <: t'
(d) S; G |= forall p. wp' p ==> (Pure.return_wp t e) p  //note p:(t' -> Type0)

Proof: By induction on derivation of (1), case analysis on the last rule.

Case [T-Return]:
-----------------

From conclusion of [T-Return]:

(2) t' = t and wp = Pure.return_wp t e

From premises:

(3) S; G |- t : Type0
(4) S; G |- e : Tot t

(a) and (b) follow from (3) and (4).
(c) follows from [T-SubConv] (zero steps).
(d) is of the form S; G |= a ==> a, so we get the proof.


Case [T-Sub]:
--------------

From premises:

(2) S; G |- Pure.return t e : C
(3) S; G |- C <: Pure t' wp'

Inverting [S-CompPure] on (3):

(4) C = Pure t'' wp''
(5) S; G |- t'' <: t'
(6) S; G |= forall p:(t' -> Type0). wp' p ==> wp'' p

Applying I.H. on (2):

(7)  S; G |- t : Type0
(8)  S; G |- e : Tot t
(9)  S; G |- t <: t''
(10) S; G |= forall p. wp'' p ==> (Pure.return_wp t e) p

(a) and (b) follow from (7) and (8).

(c) follows from using [Sub-Trans] with (9) and (5).

(d) follows from (6) and (10), basically S; G |= a ==> b and S; G |= b ==> c implies S; G |= a ==> c.

We get the proof.


Qed.

-------------------------------
Lemma: Inversion-of-Pure-bind
-------------------------------

(1) S; G |- Pure.bind t1 t2 wp1 e1 wp2 x.e2 : Pure t wp

==>

(a) S; G       |- t1  : Type0
(b) S; G       |- t2  : Type0
(c) S; G       |- wp1 : Pure.t_wp t1
(d) S; G       |- e1  : Pure t1 wp1
(e) S; G       |- wp2 : x:t1 -> Pure.t_wp t2
(f) S; G, x:t1 |- e2  : Pure t2 (wp2 x)
(g) S; G       |- t2  <: t
(h) S; G       |= forall post. wp post ==> (Pure.bind_wp t1 t2 wp1 wp2) post //note post:t -> Type0


Proof: By induction on the derivation of (1), case analysis on the last rule used.


Case [T-Bind]:
---------------

From the conclusion of the rule:

(2) t = t2
(3) wp = Pure.bind_wp t1 t2 wp1 wp2

(a) through (f) follow directly from the premises.
(g) follows from rule [Sub-Conv].
(h) is of the form S; G |= a ==> a which follows.

We get the proof.


Case [T-Sub]:
--------------

From premises:

(2) S; G |- Pure.bind t1 t2 wp1 e1 wp2 x.e2 : C
(3) S; G |- C <: Pure t wp

Inverting [S-CompPure] on (3):

(4) C = Pure t' wp'
(5) S; G |- t' <: t
(6) S; G |= forall post(t -> Type0). wp post ==> wp' post

Applying I.H. on (2):

(7)  S; G       |- t1  : Type0
(8)  S; G       |- t2  : Type0
(9)  S; G       |- wp1 : Pure.t_wp t1
(10) S; G       |- e1  : Pure t1 wp1
(11) S; G       |- wp2 : x:t1 -> Pure.t_wp t2
(12) S; G, x:t1 |- e2  : Pure t2 (wp2 x)
(13) S; G       |- t2  <: t'
(14) S; G       |= forall post. wp' post ==> (Pure.bind_wp t1 t2 wp1 wp2) post

(a) through (f) follow from (7) - (12).
(g) follows from using [Sub-Trans] with (13) and (5).
(h) follows from (14) and (6), basically of the form S; G |= a ==> b, S; G |= b ==> c, and derive S; G |= a ==> c.

We get the proof.


Qed.


---------------------------
Lemma: Inversion-of-M-case
---------------------------

(1) S; G |- case (e as y) x.e1 x.e2 returns t : M t' wp'

==>

(a) S; G              |- e  : sum t1 t2
(b) S; G, y:sum t1 t2 |- t  : Type0
(c) S; G, x:t1        |- e1 : M t[Inl x/y] wp1
(d) S; G, x:t2        |- e2 : M t[Inr x/y] wp2

If M = Pure then:

(e1) S; G              |- t[e/y] <: t'
(f1) S; G              |= forall post. wp' post ==> (case (e as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t[e/y]) post //post:t' -> Type0

else:

(e2) S; G |- M.t t[e/y] (case (e as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t[e/y]) <: M.t t' wp'


Proof: By induction on derivation of (1), with case analysis on the last rule used.


Case [T-Case]:    t' = t[e/y]    wp' = case (e as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t[e/y]
---------------------------------------------------------------------------------------------------------

From premises:

(2) S; G              |- e  : sum t1 t2
(3) S; G, y:sum t1 t2 |- t  : Type0
(4) S; G, x:t1        |- e1 : Pure t[Inl x/y] wp1
(5) S; G, x:t2        |- e2 : Pure t[Inr x/y] wp2

(a) - (d) follow from (2) - (5).

If M = Pure:

(e1) follows from rule [Sub-Conv].
(f1) follows from S; G |= a ==> a.

Else:

(e2) follows from rule [Sub-Conv]. We get the proof.


Case [T-Sub]:
-------------

(2) S; G |- case (e as y) x.e1 x.e2 returns t : C''
(3) S; G |- C'' <: M t' wp'

If M = Pure:

Inverting rule [S-CompPure] on (3):

(4) C'' = Pure t'' wp''
(5) S; G |- Pure t' wp' : Type_i
(6) S; G |- t'' <: t'
(7) S; G |= forall p:(t' -> Type0). wp' p ==> wp'' p

Applying I.H. on (2), we get:

(8)  S; G              |- e  : sum t1 t2
(9)  S; G, y:sum t1 t2 |- t  : Type0
(10) S; G, x:t1        |- e1 : Pure t[Inl x/y] wp1
(11) S; G, x:t2        |- e2 : Pure t[Inr x/y] wp2
(12) S; G              |- t[e/y] <: t''
(13) S; G              |= forall post. wp'' post ==> (case (e as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t[e/y]) post //post:t'' -> Type0

(a) - (d) follow from (8) - (11).
(e) follows from rule [Sub-Trans] on (12) and (6).
(f) follows from (7) and (13), basically of the form S; G |= a ==> b and S; G |= b ==> c, and derive S; G |= a ==> c.

Else for an arbitrary M:

Inverting rule [S-CompF]:

(4) C'' = M t'' wp''
(5) S; G |- M t' wp' : Type_i
(6) S; G |- M.t t'' wp'' <: M.t t' wp'


Applying I.H. on (2):

(7)  S; G              |- e  : sum t1 t2
(8)  S; G, y:sum t1 t2 |- t  : Type0
(9)  S; G, x:t1        |- e1 : M t[Inl x/y] wp1
(10) S; G, x:t2        |- e2 : M t[Inr x/y] wp2
(11) S; G              |- M.t t[e/y] (case (e as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t[e/y]) <: M.t t'' wp''


(a) - (d) follow from (7) - (10).
(e) follows from [Sub-Trans] on (11) and (6).

We get the proof.


Qed.


-----------------------------
Lemma: Inversion-of-Tot-case
-----------------------------

(1) S; G |- case (e as y) x.e1 x.e2 returns t : Tot t'

==>

(a) S; G              |- e : sum t1 t2
(b) S; G, y:sum t1 t2 |- t : Type0
(c) S; G, x:t1        |- e1 : Tot (t[inl x/y])
(d) S; G, x:t2        |- e2 : Tot (t[inr x/y])
(e) S; G              |- z:t[e/y]{eq z (case (e as y) x.e1 x.e2 returns t)} <: t'


Proof: Similar to Lemma (Inversion-of-Tot-app).


------------------------
Lemma: Inversion-of-run
------------------------

(1) S; G |- run e : C

==>

(a) C = Tot t'
(b) S; G |- e : Pure t wp
(c) S; G |= exists p. wp p
(d) S; G |- x:Tot t{eq x (run e)} <: Tot t'


Proof: Similar to Lemma (Inversion-of-Tot-app).


--------------------------
Lemma: Inversion-of-reify
--------------------------

(1) S; G |- reify e : C

==>

(a) C = Tot t
(b) S; G |- e : F t' wp
(c) S; G |- y:(F.t t' wp){eq (F.t t' wp) y (reify e)} <: t


Proof: Similar to Lemma (Inversion-of-Tot-app).


-----------------------------
Lemma: Inversion-of-F-return
-----------------------------

(1) S; G |- F.return t e : F t' wp

==>

(a) S; G |- t : Type0
(b) S; G |- e : Tot t
(c) S; G |- F t (F.return_wp t e) <: F t' wp


Proof: By induction on derivation of (1), case analysis on the last rule.

Only possible cases are:

[T-Return]: The proof is trivial since t' = t and wp = F.return_wp t e.

[T-Sub]: Apply I.H. on the premise and then use Lemma (Transitivity-of-sub-comp).


Qed.


---------------------------
Lemma: Inversion-of-F-bind
---------------------------

(1) S; G |- F.bind t1 t2 wp1 e1 wp2 x.e2 : F t wp

==>

(a) S; G       |- t1  : Type0
(b) S; G       |- t2  : Type0
(c) S; G       |- wp1 : F.t_wp t1
(d) S; G       |- e1  : F t1 wp1
(e) S; G       |- wp2 : x:t1 -> F.t_wp t2
(f) S; G, x:t1 |- e2  : F t2 (wp2 x)
(g) S; G       |- F t2 (F.bind_wp t1 t2 wp1 wp2) <: F t wp


Proof: By induction on derivation of (1), case analysis on the last used.

Only possible cases are:

[T-Bind]: The proof is trivial since t = t2 and wp = F.bind_wp t1 t2 wp1 wp2.

[T-Sub]: Apply I.H. on the premise and then use Lemma (Transitivity-of-sub-comp).


Qed.


-----------------------------
Lemma: Inversion-of-F-action
-----------------------------

(1) S; G |- F.a_i es : F t wp

==>

(a) S (F a x) = _ with { ... a_i (xs_i:ts_i) :t_i = e_i, wp_i ... }
(b) S; G            |- ts_i : Type0
(c) S; G, xs_i:ts_i |- t_i  : Type0
(d) S; G, xs_i:ts_i |- wp_i : F.t_wp t_i
(e) S; G, xs_i:ts_i |- e_i  : F.t t_i wp_i
(f) S; G            |- es_i : ts_i
(g) S; G            |- F t_i[es/xs] wp_i[es/xs] <: F t wp


Proof: By induction on derivation of (1), case analysis on the last rule used.

(a) - (f) follow from signature typing.

Only possible cases are:

[T-Action]: The proof is trivial since t = t_i[es/xs] and wp = wp_i[es/xs].

[T-Sub]: Apply I.H. on the premise and then use Lemma (Transitivity-of-sub-comp).


Qed.


---------------------------
Lemma: Inversion-of-M-lift
---------------------------

(1) S; G |- M.lift_M' t1 wp1 e1 : C

==>

(a) C = M' t wp
(b) S (M.lift_M') = e_l, wp_l
(c) S; G |- wp_l : a:Type0 -> M.t_wp a -> Tot (M'.t_wp a)
(d) S; G |- e_l  : a:Type0 -> x:M.t_wp a -> M.t a x -> M'.t a (wp_l a x)
(e) S; G |- e1   : M t1 wp1
(f) S; G |- M' t1 (wp_l t1 wp1) <: M' t wp


Proof: By induction on derivation of (1), case analysis on the last rule used.

((b) - (d) follow from signature typing.)

Only possible cases are:

[T-Lift]: The proof is trivial since t = t1 and wp = wp_l t wp.

[T-Sub]: Apply I.H. on the premise, and then use Lemma (Transitivity-of-sub-comp).


Qed.


----------------------------
Lemma: Inversion-of-reflect
----------------------------

(1) S; G |- reflect e : C

==>

(a) S; G |- e : Tot (F.t t1 wp1)
(b) S; G |- F t1 wp1 <: C


Proof: By induction on derivation of (1), case analysis on the last rule used.

Only two cases are possible:

[T-Reflect]: The proof is trivial since C = F t1 wp1

[T-Sub] Apply I.H. on the premise, and then use Lemma (Transitivity-of-sub-comp).


--------------------------
Lemma: Inversion-of-M-app
--------------------------

If

(1) S; G |- e1 e2 : M t wp

then

(a) S; G |- e1 : x:t1 -> C1
(b) S; G |- e2 : t1
(c) S; G |- e1 e2 : C1[e2/x]
(d) S; G |- C1[e2/x] <: M t wp


Proof: By induction on derivation of (1), case analysis on the last rule.


Case [T-App]:
--------------

From premises and conclusion:

(2) S; G |- e1 : x:t1 -> C1
(3) S; G |- e2 : t1
(4) M t wp = C1[e2/x]

(a) and (b) follow from (2) and (3).
(c) follows from (1) and (4).
(d) follows from Lemma (Reflexivity-of-sub-comp). We get the proof.


Case [T-Sub]:
--------------

From premises:

(2) S; G |- e1 e2 : C'
(3) S; G |- C' <: M t wp

Inverting rule [S-CompPure] or [S-CompF] on (3), we get that:

(4) C' = M t' wp'

Applying I.H. on (2):

(5) S; G |- e1 : x:t1 -> C1
(6) S; G |- e2 : t1
(7) S; G |- e1 e2 : C1[e2/x]
(8) S; G |- C1[e2/x] <: M t' wp'

(a) - (c) follow from (5) - (7).

(d) follows from Lemma (Transitivity-of-sub-comp) with (8) and (3). We get the proof.


Qed.


----------------------------
Lemma: Inversion-of-Tot-app
----------------------------

If

(1) S; G |- e1 e2 : Tot t

then

(a) S; G             |- e1 : x:t1 -> Tot t'
(b) S; G             |- e2 : t1
(c) S; G             |- e1 e2 : Tot t'[e2/x]
(d) S; G, y:t'[e2/x] |- eq t'[e2/x] y (e1 e2) : Type_i
(e) S; G             |- y:t'[e2/x]{eq t'[e2/x] y (e1 e2)} <: t


Proof: By induction on derivation of (1), case analysis on the last rule used.


Case [T-App]:
--------------

From premises and conclusion:

(2) S; G |- e1 : x:t1 -> C1
(3) S; G |- e2 : t1
(4) Tot t = C1[e2/x]

Matching the head symbol in (4), we get:

(5) C1 = Tot t'
(6) t'[e2/x] = t

(a) and (b) follow from (2) and (3).
(c) follows by rule [T-App] on (2) and (3).
(d) follows from the typing of the constant eq, typing of t'[e2/x] follows from Lemma (Derived-judgments) on (1).
(e) follows from rule [Sub-RefineL] using (d) to get the premise. We get the proof.


Case [T-Sub]:
-------------

From premises:

(2) S; G |- e1 e2 : C
(3) S; G |- C <: Tot t

Inverting rule [S-TotTot] on (3), we get:

(4) C = Tot t''
(5) S; G |- t'' <: t

Using I.H. on (2):

(6)  S; G             |- e1 : x:t1 -> Tot t'
(7)  S; G             |- e2 : t1
(8)  S; G             |- e1 e2 : Tot t'[e2/x]
(9)  S; G, y:t'[e2/x] |- eq t'[e2/x] y (e1 e2) : Type_i
(10) S; G             |- y:t'[e2/x]{eq t'[e2/x] y (e1 e2)} <: t''

(a) - (d) follow from (4) - (7).
(e) follows from using rule [Sub-Trans] with (10) and (5). We get the proof.


Case [T-RefineI]:
------------------

From premises and conclusion of the rule:

(2) t = z:t1'{t2'}
(3) S; G        |- e1 e2 : Tot t1'
(4) S; G, z:t1' |- t2' : Type_j
(5) S; G        |= t2'[e1 e2/z]

Applying I.H. on (3):

(6)  S; G             |- e1 : x:t1 -> Tot t'
(7)  S; G             |- e2 : t1
(8)  S; G             |- e1 e2 : Tot t'[e2/x]
(9)  S; G, y:t'[e2/x] |- eq t'[e2/x] y (e1 e2) : Type_i
(10) S; G             |- y:t'[e2/x]{eq t'[e2/x] y (e1 e2)} <: t1'

(a) - (d) follow from (6) - (9).

Let's try to prove S; G, z:(y:t'[e2/x]{eq t'[e2/x] y (e1 e2)}) |= t2'

Informally:

S; G, z:(y:t'[e2/x]{eq t'[e2/x] y (e1 e2)}) |- z : y:t'[e2/x]{eq t'[e2/x] y (e1 e2)}
------------------------------------------------------------------------------------- [V-Refine]
S; G, z:(y:t'[e2/x]{eq t'[e2/x] y (e1 e2)}) |- eq t'[e2/x] z (e1 e2)    S; G, z:(y:t'[e2/x]{eq t'[e2/x] y (e1 e2)}) |= P (e1 e2)    (Choose P = fun z' -> t2'[z'/z] and use (5) with weakening)
-------------------------------------------------------------------------------------- [V-EqP]
(11) S; G, z:(y:t'[e2/x]{eq t'[e2/x] y (e1 e2)}) |= t2'

Using rule [Sub-RefineR] with (10) and (11), we get the proof.

(Note that to reason about typing of P above, we need Lemma (Strengthen-binding)).


Qed.


------------------------
Lemma: Inversion-of-fun
------------------------

If

(1) S; G |- fun x:t -> e : C1

then

(a) C = Tot t'
(b) S; G      |- t : Type_i
(c) S; G, x:t |- e : C
(d) S; G      |- y:(x:t -> C){eq y (fun x:t -> e)} <: t'


Proof: By induction on derivation of (1), case analysis on the last rule used.


Case [T-Abs] [T-Sub]: Similar to Lemma (Inversion-of-Tot-app).
--------------------------------------------------------------

Case [T-Refine]:
-----------------

From premises and conclusion:

(2) C1 = y:t1'{t2'}
(3) S; G        |- fun x:t -> e : Tot t1'
(4) S; G, y:t1' |- t2' : Type_j
(5) S; G        |= t2'[fun x:t -> e/y]

Using I.H. on (3):

(6) S; G      |- t : Type_i
(7) S; G, x:t |- e : C
(8) S; G      |- y:(x:t -> C){y = fun x:t -> e} <: t1'

Similar to Lemma (Inversion-of-Tot-app), we can prove:

(9) S; G, z:(y:(x:t -> C){eq (x:t -> C) y (fun x:t -> e)}) |= t2'

Using rule [Sub-RefineR] with (8) and (9, we get the proof.


Qed.


-----------------------
Lemma: Progress-of-Tot
-----------------------

forall e, t.

(1) . |- e : Tot t

==>
Either

(a1) e is a value

Or

(a2) exists e'.  e ~> e'


-------------------------
Lemma: Progress-of-Pure
-------------------------

forall e, t, wp, p.

(1) . |- e : Pure t wp
(2) . |= wp p

==>

Either

(a1) e = Pure.return t' v

Or

(a2) exists e'. e ~> e'


--------------------------------
Lemma: Preservation-for-context
--------------------------------

(1) S |- e ~> e'
(2) S; G |- E<e> : C'

==>

(a) S; G |- E<e'> : C'


Proof: By structural induction on E.
-------------------------------------


Case E = E1 e1
----------------


From (4):

(5) S; G |- E1<e> e1 : C'


Case when C' = M' t' wp'

From Lemma (Inversion-of-M-app) on (5):

(6) S; G |- E1<e> : x:t1 -> C1
(7) S; G |- e1 : t1
(8) S; G |- E1<e> e1 : C1[e1/x]
(9) S; G |- C1[e1/x] <: M' t' wp'

Using I.H. with (1) and (6) (E1 is smaller than E):

(10) S; G |- E1<e'> : x:t1 -> C1

Using rule [T-App] with (10) and (7):

(11) S; G |- E1<e'> e1 : C1[e1/x]

Using rule [T-Sub] with (11) and (9), we get the proof.

Other cases should be similar with the use of corresponding inversion lemmas.


--------------------
Lemma: Preservation
--------------------

(1) S; G |- e : C_e
(2) e ~> e'

==>

(a) S; G |- e' : C_e

Proof: By induction on derivation of (2), with case analysis on the last rule used.


Case [Context]: e = E<e1>    e' = E<e1'>    e ~> e'
---------------------------------------------------

Immediate from Lemma (Preservation-for-context).


Case [Beta]: e = (fun x:t -> e1) e2    e' = e1[e2/x]
-----------------------------------------------------

We consider two cases, when C_e = M t wp and when C_e = Tot t

        When C_e = M t wp
        ==================

Using Lemma (Inversion-of-M-app) on (1):

(4) S; G |- fun x:t -> e1 : x:t1 -> C1
(5) S; G |- e2 : t1
(6) S; G |- (fun x:t -> t1) e2 : C1[e2/x]
(7) S; G |- C1[e2/x] <: M t wp

Using Lemma (Inversion-of-fun) on (4):

(8)  S; G      |- t  : Type_i
(9)  S; G, x:t |- e1 : C
(10) S; G      |- y:(x:t -> C){eq y (fun x:t -> e1)} <: x:t1 -> C1

Using Lemma (Inversion-of-sub-refiner):

(11) S; G       |- t1 <: t
(12) S; G, x:t1 |- C  <: C1

Using rule [S-TotTot] with (11):

(13) S; G |- Tot t1 <: Tot t

Using rule [T-Sub] with (5) and (13):

(14) S; G |- e2 : t

Using Lemma (Substitution) with (9) and (14):

(15) S; G |- e1[e2/x] : C[e2/x]

Using Lemma (Substitution) with (5) and (12):

(16) S; G |- C[e2/x] <: C1[e2/x]

Using Lemma (Transitivity-of-sub-comp) with (16) and (7), we get the proof.


        When C_e = Tot t
        =================

Using Lemma (Inversion-of-Tot-app) on (1):

(3) S; G             |- fun x:t -> e1 : x:t1 -> Tot t'
(4) S; G             |- e2 : t1
(5) S; G             |- (fun x:t -> e1) e2 : Tot t'[e2/x]
(6) S; G, y:t'[e2/x] |- eq t'[e2/x] y ((fun x:t -> e1) e2) : Type_i
(7) S; G             |- y:t'[e2/x]{eq t'[e2/x] y ((fun x:t -> e1) e2)} <: t

Using Lemma (Inversion-of-fun) on (3):

(8)  S; G      |- t : Type_i
(9)  S; G, x:t |- e1 : C
(10) S; G      |- y:(x:t -> C){eq y (fun x:t -> e1)} <: x:t1 -> Tot t'

Using Lemma (Inversion-of-sub-refiner) on (10):

(11) S; G       |- t1 <: t
(12) S; G, x:t1 |- C <: Tot t'

Inverting [S-TotTot] on (12):

(13) C = Tot t''
(14) S; G, x:t1 |- t'' <: t'

Using Lemma (Strengthen-binding) on (9) and (11):

(15) S; G, x:t1 |- e1 : Tot t''

Using rule [Sub-Trans] with (14) and (15):

(16) S; G, x:t1 |- e1 : t'

Using Lemma (Substitution) with (4) and (16):

(17) S; G |- e1[e2/x] : t'[e2/x]

Let's try to show: S; G |= (eq t'[e2/x] y ((fun x:t -> e1) e2))[e1[e2/x]/y]. From [V-EqRed]:

(18) S; G |= (eq t'[e2/x] y ((fun x:t -> e1) e2))[e1[e2/x]/y]

Using rule [T-RefineI] with (17) and (18):

(19) S; G |- e1[e2/x] : y:t'[e2/x]{eq t'[e2/x] y ((fun x:t -> e1) e2)}

Using rule [Sub-Trans] with (18) and (19), we get the proof.


Case [Proj-L]:    e = fst t1 t2 e1 e2    e' = e1
--------------------------------------------------

Inverting typing of constant fst:

(3) S; G |- t1 : Type0
(4) S; G |- t2 : Type0
(5) S; G |- e1 : t1
(6) S; G |- e2 : t2

We get the proof.


Case [Proj-R]: Analogous to [Proj-L].
-------------------------------------


Case [Case-L]:    e = case (inl e_case as y) x.e1 x.e2 returns t''    e' = e1[e_case/x]
----------------------------------------------------------------------------------------

We consider two cases, when C_e = M t wp and when C_e = Tot t

        When C_e = M t wp
        ==================	

Using Lemma (Inversion-of-M-case) on (1):

When M = Pure:

(4) S; G              |- inl e_case        : sum t1 t2
(5) S; G, y:sum t1 t2 |- t''               : Type0
(6) S; G, x:t1        |- e1                : Pure t''[inl x/y] wp1
(7) S; G, x:t2        |- e2                : Pure t''[inr x/y] wp2
(8) S; G              |- t''[inl e_case/y] <: t
(9) S; G              |= forall post. wp post ==> (case (inl e_case as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t''[inl e_case/y]) post //post:t -> Type0

Using rule [Case-L], we get:

(10) S |- (case (inl e_case as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t''[inl e_case/y]) post ~> wp1[e_case/x] post

Using rule [Context], we get:

(11) S |- forall post. wp post ==> (case (inl e_case as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t''[inl e_case/y]) post ~> forall post. wp post ==> wp1[e_case/x] post

Using rule [V-EqRed]:

(12) S; G |- eq Type0 (forall post. wp post ==> (case (inl e_case as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t''[inl e_case/y]) post) (forall post. wp post ==> wp1[e_case/x] post)

Using rule [V-Eq*] with (9) and (12):

(13) S; G |= forall post. wp post ==> wp1[e_case/x] post //post:t -> Type0

Inverting typing of constant inl on (4):

(14) S; G |- e_case : t1

Using Lemma (Substitution) with (6) and (14):

(15) S; G |- e1[e_case/x] : Pure t''[inl x/y][e_case/x] wp1[e_case/x]

Using Lemma (Commuting-Substitution):

(16) t''[inl x/y][e_case/x] = t''[e_case/x][inl x[e_case/x]/y]

Since x does not occur free in t'' (from 5):

(17) t''[inl x/y][e_case/x] = t''[inl e_case/y]

Hence (15) can be written as:

(18) S; G |- e1[v/x] : Pure t''[inl e_case/y] wp1[e_case/x]

Using Lemma (Derived-judgments) on (1):

(19) S; G |- Pure t wp : Type_i

Using rule [S-CompPure] with (19), (8), and (13):

(20) S; G |- Pure t''[inl e_case/y] wp1[v/x] <: Pure t wp

Using rule [T-Sub] with (18) and (20), we get the proof.


Else for an arbitrary M:

(4) S; G              |- inl e_case        : sum t1 t2
(5) S; G, y:sum t1 t2 |- t''               : Type0
(6) S; G, x:t1        |- e1                : M t''[inl x/y] wp1
(7) S; G, x:t2        |- e2                : M t''[inr x/y] wp2
(8) S; G              |= M.t t''[inl e_case/y] (case (inl e_case as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t''[inl e_case/y]) <: M.t t wp

We have to prove: S; G |- e1[e_case/x] : M t wp.

Inverting typing of constant inl on (4):

(9) S; G |- e_case : t1

Using Lemma (Substitution) on (9) and (6):

(10) S; G |- e1[e_case/x] : M t''[inl x/y][e_case/x] wp1[e_case/x]

Using Lemma (Commuting-Substitution):

(11) t''[inl x/y][e_case/x] = t''[e_case/x][inl x[e_case/x]/y]

Since x does not occur free in t'' (from 5):

(12) t''[inl x/y][e_case/x] = t''[inl e_case/y]

Hence (10) can be written as:

(13) S; G |- e1[v/x] : M t''[inl e_case/y] wp1[e_case/x]

So, our goal is now to prove, S; G |- M t''[inl e_case/y] wp1[e_case/x] <: M t wp.

We have, by strong reduction [Case-L] in the second argument:

(14) M.t t''[inl e_case/y] (case (inl e_case as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t''[inl e_case/y]) ~> M.t t''[inl e_case/y] wp1[e_case/x]

Using rule [Sub-Conv]:

(15) S; G |- M.t t''[inl e_case/y] wp1[e_case/x] <: M.t t''[inl e_case/y] (case (inl e_case as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t''[inl e_case/y])

(We need to argue about typability of M.t t''[inl e_case/y] (case (inl e_case as _) (fun x -> wp1) (fun x -> wp2) returns M.t_wp t''[inl e_case/y])

Using rule [Sub-Trans] on (15) and (8), we get:

(16) S; G |- M.t t''[inl e_case/y] wp1[e_case/x] <: M.t t wp

Using rule [T-Sub] with (13) and (16), we get the proof.


        When C_e = Tot t
        =================

Using Lemma (Inversion-of-Tot-case) on (1):

(3) S; G              |- inl e_case  : sum t1 t2
(4) S; G, y:sum t1 t2 |- t''         : Type0
(5) S; G, x:t1        |- e1          : Tot t''[inl x/y]
(6) S; G, x:t2        |- e2          : Tot t''[inr x/y]
(7) S; G              |- z:t''[inl v/y]{eq z (case (inl e_case as _) x.e1 x.e2 returns t'')} <: t

Inverting typing of constant inl on (3):

(8) S; G |- e_case : t1

Using Lemma (Substitution) with (8) and (5):

(9) S; G |- e1[e_case/x] : Tot t''[inl e_case/y]

Using [V-EqRed] we can prove:

(10) S; G |= {eq z (case (inl e_case as _) x.e1 x.e2 returns t'')}[e1[inl e_case/x]/z]

Using rule [T-RefineI] with (9) and (10), and then using rule [Sub-Trans] with the conclusion and (7), we get the proof.


Case [Case-R]: Analogous to [Case-L]
-------------------------------------


Case [Reify-Reflect]:    e = reify (reflect e1)    e' = e1
-----------------------------------------------------------

Using Lemma (Inversion-of-reify) on (1):

(3) S; G |- reflect e1 : F t' wp'
(4) S; G |- y:(F.t t' wp'){eq (F.t t' wp') y (reify (reflect e1))} <: t

Using Lemma (Inversion-of-reflect) pn (3):

(5) S; G |- e1 : Tot (F.t t1 wp1)
(6) S; G |- F t1 wp1 <: F t' wp'

Inverting rule [S-CompF] on (6):

(7) S; G |- F.t t1 wp1 <: F.t t' wp'

Using rule [T-Sub] with (5) and (7):

(8) S; G |- e1 : F.t t' wp'

Similar to case [T-App], using rule [V-EqRed], we can show:

(11) S; G |= (eq (F.t t' wp') y (reify (reflect e1)))[e1/y]

Using rule [T-RefineI] with (8) and (11), and then usinf rule [T-Sub] with the conclusion and (4), we get the proof.


Case [Run-PureRet]:    e = run (Pure.return t1 e1)    e' = e1
--------------------------------------------------------------

Using Lemma (Inversion-of-run) on (1):

(3) S; G |- Pure.return t1 e1 : Pure t2 wp
(4) S; G |= exists p. wp p
(5) S; G |- x:Tot t1{eq x (run (Pure.return t1 e1))} <: Tot t

Using Lemma (Ret-Pure-is-weakest) on (3):

(6) S; G |- t1 : Type0
(7) S; G |- e1 : Tot t1
(8) S; G |- t1 <: t2
(9) S; G |= forall p. wp p ==> (Pure.return_wp t1 e1) p

Using [V-EqRed] we get:

(10) S; G |= (eq x (run (Pure.return t1 e1)))[e1/x]

Using rule [T-RefineI] with (7) and (10):

(11) S; G |- e1 : x:Tot t1{eq x (run (Pure.return t1 e1))}

Using rule [Sub-Trans] with (11) and (5), we get the proof.


Case [Reify-Ret]:    e = reify (F.return t' e)    e' = F.return_e t' e
-----------------------------------------------------------------------

Using Lemma (Inversion-of-reify) on (1):

(3) S; G |- F.return t' e : F t'' wp
(4) S; G |- y:(F.t t'' wp){eq (F.t t'' wp) y (reify (F.return t' e))} <: t

Using Lemma (Inversion-of-F-return) on (3):

(5) S; G |- t' : Type0
(6) S; G |- e  : Tot t'
(7) S; G |- F t' (F.return_wp t' e) <: F t'' wp

Using typing of F.return_e from the signature (with (5) and (6)):

(8) S; G |- F.return_e t' e : F.t t' (F.return_wp t' e)

Inverting rule [S-CompF] on (7):

(9) S; G |- F.t t' (F.return_wp t' e) <: F.t t'' wp

Using rule [T-Sub] with (8) and (9):

(10) S; G |- F.return_e t' e : F.t t'' wp

Similar to case [T-App], using rule [V-EqRed], we can show:

(11) S; G |= (eq (F.t t'' wp) y (reify (F.return t' e)))[F.return_t t' e/y]

Using rule [T-RefineI] with (10) and (11):

(12) S; G |- F.return_e t' e : (y:(F.t t'' wp){eq (F.t t'' wp) y (reify (F.return t' e))})

Using rule [T-Sub] with (12) and (4), we get the proof.


Case [PureBind]:    e = Pure.bind t1 t2 wp1 (Pure.return t1' e1) wp2 x.e2    e' = e2[e1/x]
-------------------------------------------------------------------------------------------

Using Lemma (Inversion-of-Pure-bind) on (1):

(4)  S; G       |- t1          : Type0
(5)  S; G       |- t2          : Type0
(6)  S; G       |- wp1         : Pure.t_wp t1
(7)  S; G       |- Pure t1' e1 : Pure t1 wp1
(8)  S; G       |- wp2         : x:t1 -> Pure.t_wp t2
(9)  S; G, x:t1 |- e2          : Pure t2 (wp2 x)
(10) S; G       |- t2  <: t
(11) S; G       |= forall post. wp post ==> (Pure.bind_wp t1 t2 wp1 wp2) post //note post:t -> Type0

We can show that Pure.bind_wp t1 t2 wp1 wp2 is well-typed (using (4), (5), (6), and (8)), and also (t -> Type0) <: (t2 -> Type0) using (10), and  (Pure.bind_wp t1 t2 wp1 wp2) post ~> wp1 (fun x:t1 -> (wp2 x) post).

Since we have strong reduction, we can also show that:

(11') forall post. wp post ==> (Pure.bind_wp t1 t2 wp1 wp2) post  ~> forall post. wp post ==> wp1 (fun x:t1 -> (wp2 x) post).

Using [V-EqRed] with (11) and (11') with t as Type0:

(11'') S; G |- eq Type0 (forall post. wp post ==> (Pure.bind_wp t1 t2 wp1 wp2) post) (forall post. wp post ==> wp1 (fun x:t1 -> (wp2 x) post))

Using [V-Eq*] with (11'') and (11):

(12) S; G |= forall post. wp post ==> wp1 (fun x:t1 -> (wp2 x) post)  //note post:t -> Type0

Using Lemma (Ret-Pure-is-weakest) on (7):

(13) S; G |= forall post. wp1 post ==> (Pure.return_wp t1' e1) post //note post:t1 -> Type0


Consider a context S; G, post:t -> Type0. We can show that:

(14) S; G, post:t -> Type0 |- (fun x:t1 -> (wp2 x) post) : t1 -> Type0

Use [V-foralle] with (13) and (14) after applying Lemma (Weakening) to (13):

(15): S; G, post:t -> Type0 |= wp1 (fun x:t1 -> (wp2 x) post) ==> (wp2 e1) post

Using [V-foralli] with (15), and then [V-MP] with (12) to get:

(16) S; G |= forall post. wp post ==> (wp2 e1) post //note post:t -> Type0

Using Lemma (Ret-Pure-is-weakest) on (7) we also get:

(17) S; G |- e1  : Tot t1'
(18) S; G |- t1' <: t1

Using rule [S-TotTot] on (18), and then rule [T-Sub] with (17) to get:

(19) S; G |- e1 : Tot t1

Using Lemma (Substitution) with (9) and (19):

(20) S; G |- e2[e1/x] : Pure t2 (wp2 e1)

We will be done if we can show that S; G |- Pure t2 (wp2 e1) <: Pure t wp

Using Lemma (Derived-judgments) on (1), we get:

(21) S; G |- Pure t wp : Type_i

Apply rule [S-CompPure] with (21), (10), and (16), and we get the proof.


Case [Reify-Bind]:    e = reify (F.bind t1 t2 wp1 e1 wp2 x.e2)    e' = F.bind_e t1 t2 wp1 (reify e1) wp2 x.(reify e2)
------------------------------------------------------------------------------------------------

Using Lemma (Inversion-of-reify) on (1):

(3) S; G |- F.bind t1 t2 wp1 e1 wp2 x.e2 : F t' wp
(4) S; G |- y:(F.t t' wp){eq (F.t t' wp) y (reify (F.bind t1 t2 wp1 e1 wp2 x.wp2))} <: t

Using Lemma (Inversion-of-F-bind) on (3):

(5)  S; G       |- t1  : Type0
(6)  S; G       |- t2  : Type0
(7)  S; G       |- wp1 : F.t_wp t1
(8)  S; G       |- e1  : F t1 wp1
(9)  S; G       |- wp2 : x:t1 -> F.t_wp t2
(10) S; G, x:t1 |- e2  : F t2 (wp2 x)
(11) S; G       |- F t2 (F.bind_wp t1 t2 wp1 wp2) <: F t' wp

Using typing of F.bind_e with (5) - (10):

(12) S; G |- F.bind_e t1 t2 wp1 (reify e1) wp2 x.(reify e2) : F.t t2 (F.bind_wp t1 t2 wp1 wp2)

(Note that using (10) and then rule [T-Abs], we can derive: S; G |- fun x:t1 -> e2 : x:t1 -> Tot (F.t t2 (wp2 x))

Inverting rule [Sub-CompF] on (11) and applying [T-Sub] with the conclusion and (12):

(13) S; G |- F.bind_e t1 t2 wp1 (reify e1) wp2 x.(reify e2) : F.t t' wp

Similar to case [T-App], using rule [V-EqRed], we can show:

(14) S; G |= (eq (F.t t' wp) y (reify (F.bind t1 t2 wp1 e1 wp2 x.wp2)))[F.bind_e t1 t2 wp1 (reify e1) wp2 x.(reify e2)/y]

Using rule [T-RefineI] with (13) and (14), we get the proof.


Case [Reify-Action]:    e = reify (M.a_i es)    e' = e_i[es/xs]
----------------------------------------------------------------

Using Lemma (Inversion-of-reify) on (1):

(3) S; G |- F.a_i es : F t' wp
(4) S; G |- y:(F.t t' wp){eq (F.t t' wp) y (reify (M.a_i es))} <: t

Using Lemma (Inversion-of-F-action):

(5)  S (F a x) = _ with { ... a_i (xs_i:ts_i) :t_i = e_i, wp_i ... }
(6)  S; G            |- ts_i : Type0
(7)  S; G, xs_i:ts_i |- t_i  : Type0
(8)  S; G, xs_i:ts_i |- wp_i : F.t_wp t_i
(9)  S; G, xs_i:ts_i |- e_i  : F.t t_i wp_i
(10) S; G            |- es_i : ts_i
(11) S; G            |- F t_i[es/xs] wp_i[es/xs] <: F t' wp

Using Lemma (Substitution) with (10) and (9):

(12) S; G |- e_i[es/xs] : F.t t_i[es/xs] wp_i[es/xs]

Inverting rule [S-CompF] on (11) and using rule [T-Sub] with the conclusion and (12):

(13) S; G |- e_i[es/xs] : F.t t' wp

Similar to case [T-App], using rule [V-EqRed], we can show:

(14) S; G |= (eq (F.t t' wp) y (reify (M.a_i es)))[e_i[es/xs]/y]

Using rule [T-RefineI] with (13) and (14), and then using [T-Sub] with the conclusion and (4), we get the proof.


Case [Reify-Lift]:    e = reify (M.lift_M' t1 wp1 e1)    e' = e_l t1 wp1 (reify e1)
------------------------------------------------------------------------------------

Using Lemma (Inversion-of-reify) on (1):

(3) S; G |- M.lift_M' t1 wp1 e1 : F t' wp'
(4) S; G |- y:(F.t t' wp'){eq (F.t t' wp') y (reify (M.lift_M' t1 wp1 e1))} <: t

Using Lemma (Inversion-of-M-lift) on (3), and rewriting (3) and (4) too:

(5)  S; G |- M.lift_M' t1 wp1 e1 : M' t' wp'
(6)  S; G |- y:(M.t t' wp'){eq (M.t t' wp') y (reify (M.lift_M' t1 wp1 e1))} <: t
(7)  S (M.lift_M') = e_l, wp_l
(8)  S; G |- wp_l : a:Type0 -> M.t_wp a -> Tot (M'.t_wp a)
(9)  S; G |- e_l  : a:Type0 -> x:M.t_wp a -> M.t a x -> M'.t a (wp_l a x)
(10) S; G |- e1   : M t1 wp1
(11) S; G |- M' t1 (wp_l t1 wp1) <: M' t' wp'

Using Lemma (Derived-judgments) on (10) and then inverting rule [C-M], we get:

(12) S; G |- t1  : type0
(13) S; G |- wp1 : M.t_wp t1

Using rule [T-Reify] with (10) we get:

(14) S; G |- reify c : M.t t1 wp1

Using rule [T-App] with (9), (12), (13), and (14), we get:

(15) S; G |- e_l t1 wp1 (reify e1) : M'.t t1 (wp_l t1 wp1)

Inverting rule [S-CompF] on (11), and then using rule [T-Sub] with the conclusion and (15):

(16) S; G |- e_l t1 wp1 (reify e1) : M'.t t' wp'

Similar to case [T-App], using rule [V-EqRed], we can show:

(17) S; G |= (eq (M.t t' wp') y (reify (M.lift_M' t1 wp1 e1)))[e_l t1 wp1 (reify e1)/y]

Using rule [T-RefineI] with (16) and (17), and then using rule [T-Sub] with the conclusion and (6), we get the proof.


Qed.


--------------------------------------
Lemma: Single-step-correctness-of-Pure
--------------------------------------

(1) S; . |- e : Pure t wp
(2) S; . |- p : t -> Type0
(3) S; . |= wp p

==>

(a) run e ~> e'

s.t. Either

(b1) e' = v
(c1) S; . |= p v

Or

(b2) e' = run e''
(c2) S; . |- e'' : Pure t wp


Proof:

Using Lemma (Progress-of-Pure) with (1) we get two cases:

(4.1) e = Pure.return t' v

(a)  follows using rule [Run-PureRet].
(b1) follows from RHS of [Run-PureRet].

Using Lemma (Ret-Pure-is-weakest) on (1), with e = Pure.return t' v:

(5.1) S; . |= forall post. wp post ==> (Pure.return_wp t v) post

Using rule [V-foralle] with (2) and (5.1) (also simplifying RHS of implication in (5.1)):

(6.1) S; . |= wp p ==> p v

Using rule [V-MP] with (3) and (6.1), we get the proof.

Second case of Lemma (Progress-of-Pure) with (1) gives us:

(4.2) e ~> e1

Using Lemma (Preservation) with (1) and (4.2):

(5.2) S; . |- e1 : Pure t wp

Choose e'' = e1

(a)  follows from [Context] with E = run E, and (4.2).
(b2) follows from proof of (a).
(c2) follows from (5.2).


Qed.


------------------------------------
Theorem: Total Correctness for Pure
------------------------------------

(1) S; . |- e : Pure t wp
(2) S; . |- p : t -> Type0
(2) S; . |= wp p

==> exists v.

(a) run e ~>+ v
(b) . |= p v


Proof:

(a) follows from the normalization of the Pure monad.

For (b) we do an induction on the number of steps n in run e ~>+ v.

Base case: run e ~> v
----------------------

Using Lemma (Single-step-correctness-of-Pure) we get (b).

Induction case:    run e ~> e' ~>n v
-------------------------------------

Using Lemma (Single-step-correctness-of-Pure):

(4) e' = run e''
(5) S; . |- e'' : Pure t wp

Using I.H. on n, we get the proof.


Qed.