Chapter 8 Proofs

ch8.slf

package tapl;

terminals true false if then else value steporvalue Bool Nat subterm succ nv

syntax

t ::= true |
      false |
      if t then t else t |
      0 |
      succ t

T ::= Bool |
      Nat

/********** EVALUATION ************/

// a judgement is a statement whose derivation is justified
// by a tree of rules labeled by inference rules
judgment eval: t -> t

// a judgement is followed by a series of inference rules
// that define the judgment's semantics

----------------------------- e-iftrue
if true then t2 else t3 -> t2


------------------------------ e-iffalse
if false then t2 else t3 -> t3


t1 -> t1'
----------------------------------------------- e-if
if t1 then t2 else t3 -> if t1' then t2 else t3


t -> t'
----------------- e-succ
succ t -> succ t'

/******************************/
/********** TYPING ************/
/******************************/

judgment typing: t : T


----------- t-true
true : Bool


------------ t-false
false : Bool

------- t-zero
0 : Nat

t : Nat
------------ t-succ
succ t : Nat

t1 : Bool
t2 : T
t3 : T
------------------------- t-if
if t1 then t2 else t3 : T

/********** VALUES ************/

judgment values: t value


---------- v-true
true value


----------- v-false
false value

t nv
------- v-num
t value

judgment numvalues: t nv

---- nv-zero
0 nv

t nv
--------- nv-succ
succ t nv

/*************************************/
/********** STEP OR VALUE ************/
/*************************************/

judgment steporvalue: t steporvalue

t value
------------- sv-values
t steporvalue

t -> t'
------------- sv-step
t steporvalue

/********** SUBTERMS **********/

judgment subterm: t subterm t

-------------------------- st-if-t1
t1 subterm if t1 then t2 else t3

-------------------------- st-if-t2
t2 subterm if t1 then t2 else t3

-------------------------- st-if-t3
t3 subterm if t1 then t2 else t3

/********** CANONICAL FORMS ************/

judgment canonical-forms: t value : T


----------------- canonical-true
true value : Bool


------------------ canonical-false
false value : Bool

t nv
------------- canonical-nv
t value : Nat

lemma canonical-forms:
  forall d1: t : T
  forall d2: t value
  exists t value : T.

  _: t value : T by case analysis on d2:
    case rule
      ------------- v-true
      _: true value
    is
      _ : true value : T by case analysis on d1:
        case rule
          -------------- t-true
          _: true : Bool
        is
          _: true value : Bool by rule canonical-true
        end case
      end case analysis
    end case

    case rule
      -------------- v-false
      _: false value
    is
      _ : false value : T by case analysis on d1:
        case rule
          --------------- t-false
          _: false : Bool
        is
          _: false value : Bool by rule canonical-false
        end case
      end case analysis
    end case

    case rule
      dnv: t nv
      --------- v-num
      _: t value
    is
      _: t value : T by case analysis on dnv:
        case rule
          -------- nv-zero
          dn: 0 nv
        is
          _ : 0 value : T by case analysis on d1:
            case rule
              ---------- t-zero
              _: 0 : Nat
            is
              _: 0 value : Nat by rule canonical-nv on dn
            end case
          end case analysis
        end case

        case rule
          dv: t' nv
          ------------- nv-succ
          dc: succ t' nv
        is
          _ : (succ t') value : T by case analysis on d1:
            case rule
              d5: t' : Nat
              ---------------- t-succ
              _: succ t' : Nat
            is
              _: (succ t') value : Nat by rule canonical-nv on dc
            end case
          end case analysis
        end case
      end case analysis
    end case
  end case analysis
end lemma

/************ SUBTERM WELL-TYPED ************/

theorem well_typed_subterms:
  forall d1: t : T
  forall d2: t' subterm t
  exists t': T'.

  _: t': T' by induction on d2:
    case rule
      ----------------------------------- st-if-t1
      _: t1 subterm if t1 then t2 else t3
    is
      _: t': T' by case analysis on d1:
        case rule
          dt: t1 : Bool
          _: t2 : T
          _: t3 : T
          ---------------------------- t-if
          _: if t1 then t2 else t3 : T
        is
          _: t1: Bool by dt
        end case
      end case analysis
    end case

    case rule
      ----------------------------------- st-if-t2
      _: t2 subterm if t1 then t2 else t3
    is
      _: t': T' by case analysis on d1:
        case rule
          _: t1 : Bool
          dt: t2 : T
          _: t3 : T
          ---------------------------- t-if
          _: if t1 then t2 else t3 : T
        is
          _: t2: T by dt
        end case
      end case analysis
    end case

    case rule
      ----------------------------------- st-if-t3
      _: t3 subterm if t1 then t2 else t3
    is
      _: t': T' by case analysis on d1:
        case rule
          _: t1 : Bool
          _: t2 : T
          dt: t3 : T
          ---------------------------- t-if
          _: if t1 then t2 else t3 : T
        is
          _: t3: T by dt
        end case
      end case analysis
    end case
  end induction
end theorem

/************ PROGRESS ************/

theorem progress:
  forall d1: t : T
  exists t steporvalue.

  d2: t steporvalue by induction on d1:
    case rule
      -------------- t-true
      _: true : Bool
    is
      d3: t value by rule v-true
      d4: t steporvalue by rule sv-values on d3
    end case

    case rule
      --------------- t-false
      _: false : Bool
    is
      d3: t value by rule v-false
      d4: t steporvalue by rule sv-values on d3
    end case

    case rule
      ---------- t-zero
      _: 0 : Nat
    is
      d3: 0 nv by rule nv-zero
      d4: 0 value by rule v-num on d3
      d5: 0 steporvalue by rule sv-values on d4
    end case

    case rule
      dt: t' : Nat
      -------------- t-succ
      _: succ t' : Nat
    is
      d3: t' steporvalue by induction hypothesis on dt
      _: t steporvalue by case analysis on d3:
        case rule
          dv: t' value
          ----------------- sv-values
          _: t' steporvalue
        is
          d4: t' value : Nat by lemma canonical-forms on dt,dv
          _: t steporvalue by case analysis on d4:
            case rule
              dn: t' nv
              ----------------- canonical-nv
              _: t' value : Nat
            is
              d5: succ t' nv by rule nv-succ on dn
              d6: succ t' value by rule v-num on d5
              _: succ t' steporvalue by rule sv-values on d6
            end case
          end case analysis
        end case


        case rule
          de: t' -> t''
          ----------------- sv-step
          _: t' steporvalue
        is
          d5: succ t' -> succ t'' by rule e-succ on de
          d6: t steporvalue by rule sv-step on d5
        end case
      end case analysis
    end case

    case rule
      dip1: t1 : Bool
      _: t2 : T
      _: t3 : T
      ---------------------------- t-if
      _: if t1 then t2 else t3 : T
    is
      d3: t1 steporvalue by induction hypothesis on dip1
      d4: t steporvalue by case analysis on d3:
        case rule
          dsvp: t' value
          ----------------- sv-values
          _: t' steporvalue
        is
          d5: t' value : Bool by lemma canonical-forms on dip1,dsvp
          d6: t steporvalue by case analysis on d5:
            case rule
              -------------------- canonical-true
              _: true value : Bool
            is
              d7: if t' then t2 else t3 -> t2 by rule e-iftrue
              d8: t steporvalue by rule sv-step on d7
            end case

            case rule
              --------------------- canonical-false
              _: false value : Bool
            is
              d7: if false then t2 else t3 -> t3 by rule e-iffalse
              d8: if false then t2 else t3 steporvalue by rule sv-step on d7
            end case
          end case analysis
        end case

        case rule
          dsp: t' -> t''
          ----------------- sv-step
          _: t' steporvalue
        is
          d5: if t1 then t2 else t3 -> if t'' then t2 else t3 by rule e-if on dsp
          d6: t steporvalue by rule sv-step on d5
        end case
      end case analysis
    end case
  end induction
end theorem


/************ PRESERVATION ************/

theorem preservation:
  forall d1: t : T
  forall d2: t -> t'
  exists t' : T.

  _: t' : T by induction on d1:
    case rule
      -------------- t-true
      _: true : Bool
    is
      d3: t' : Bool by case analysis on d2:
      end case analysis
    end case

    case rule
      --------------- t-false
      _: false : Bool
    is
      d3: t' : Bool by case analysis on d2:
      end case analysis
    end case

    case rule
      ---------- t-zero
      _: 0 : Nat
    is
      d3: t' : Nat by case analysis on d2:
      end case analysis
    end case

    case rule
      dt: t2 : Nat
      ---------------- t-succ
      _: succ t2 : Nat
    is
      _: t' : Nat by case analysis on d2:
        case rule
          de: t2 -> t3
          --------------------- e-succ
          _: succ t2 -> succ t3
        is
          d4: t3 : Nat by induction hypothesis on dt,de
          _: succ t3 : Nat by rule t-succ on d4
        end case
      end case analysis
    end case

    case rule
      dt: t1 : Bool
      dt2: t2 : T
      dt3: t3 : T
      ---------------------------- t-if
      _: if t1 then t2 else t3 : T
    is
      _: t' : T by case analysis on d2:
        case rule
          -------------------------------- e-iftrue
          _: if true then t2 else t3 -> t2
        is
          _: t2 : T by dt2
        end case

        case rule
          --------------------------------- e-iffalse
          _: if false then t2 else t3 -> t3
        is
          _: t3 : T by dt3
        end case
        
        case rule
          de: t1 -> t1'
          -------------------------------------------------- e-if
          _: if t1 then t2 else t3 -> if t1' then t2 else t3
        is
          d5: t1' : Bool by induction hypothesis on dt,de
          _: if t1' then t2 else t3 : T by rule t-if on d5,dt2,dt3
        end case
      end case analysis
    end case
  end induction
end theorem