homework6-internal-error.slf

package edu.northeastern.cs7480;

terminals true false if then else value
          Bool in fn


syntax

t ::= true 
  | false
  | if t then t else t
  | fn x:T => t[x]
  | x
  | t t

T ::= Bool
  | T -> T

G ::= *
      | G, x : T



judgment equality: t == t

------ eq
t == t


judgment typeequality: T == T

------ type-eq
T == T


judgment isavalue: t value


-------------------- val-fn
fn x:T => t[x] value

--------------- val-true
true value

---------------- val-false
false value


judgment eval: t -> t

----------------------------- E-IfTrue
if true then t1 else t2 -> t1

------------------------------ E-IfFalse
if false then t1 else t2 -> t2

t1 -> t1'
----------------------------------------------- E-If
if t1 then t2 else t3 -> if t1' then t2 else t3

t1 -> t1'
--------------- E-App1
t1 t2 -> t1' t2

t1 value
t2 -> t2'
--------------- E-App2
t1 t2 -> t1 t2'

t2 value
------------------------------ E-AppAbs
(fn x:T => t1[x]) t2 -> t1[t2]



judgment isvar: t : T in G
assumes G

----------------------- var
x : T in (G, x : T)


judgment type: G |- t : T
assumes G

-------------------- T-True
G |- true : Bool

--------------------- T-False
G |- false : Bool

G |- t1 : Bool
G |- t2 : T
G |- t3 : T
---------------------------------- T-If
G |- if t1 then t2 else t3 : T

t : T in G
-------------- T-Var
G |- t : T

G, x : T1 |- t[x] : T2
------------------------------------- T-Abs
G |- (fn x:T1 => t[x]) : T1 -> T2

G |- t1 : T2 -> T1
G |- t2 : T2
----------------------- T-App
G |- t1 t2 : T1

theorem typing-unique :
    assumes G
    forall d1: G |- t : T1
    forall d2: G |- t : T2
    exists T1 == T2 .
    proof by induction on d1:
        case rule
            -------------------------- T-True
            _: G |- true : Bool
        is
            proof by unproved 
        end case

        case rule
            --------------------------- T-False
            _: G |- false : Bool
        is
            proof by unproved 
        end case

        case rule
            _: G |- t0 : Bool
            p: G |- t1 : T1
            _: G |- t2 : T1
            ---------------------------------------- T-If
            _: G |- (if t0 then t1 else t2) : T1
        is
            proof by unproved 
        end case

        case rule
            p: t : T1 in G
            -------------------- T-Var
            _: G |- t : T1
        is
            proof by case analysis on d2:
                case rule
                    -------------------------- T-True
                    _: G |- true : Bool
                is
                    proof by unproved 
                end case

                case rule
                    --------------------------- T-False
                    _: G |- false : Bool
                is
                    proof by unproved 
                end case

                case rule
                    _: G |- t0 : Bool
                    _: G |- t1 : T2
                    _: G |- t2 : T2
                    ---------------------------------------- T-If
                    _: G |- (if t0 then t1 else t2) : T2
                is
                    proof by unproved 
                end case

                case rule
                    q: t : T2 in G
                    -------------------- T-Var
                    _: G |- t : T2
                is
                    use inversion of rule var on q
                    where t := x
                    proof by unproved
                end case

                case rule
                    _: (G, x : T0) |- t0[x] : T3
                    ------------------------------------------- T-Abs
                    _: G |- (fn x : T0 => t0[x]) : (T0 -> T3)
                is
                    proof by unproved
                end case

                case rule
                    _: G |- t0 : (T0 -> T2)
                    _: G |- t1 : T0
                    ----------------------------- T-App
                    _: G |- (t0 t1) : T2
                is
                    proof by unproved
                end case

                
            end case analysis
        end case

        case rule
            _: (G, x : T0) |- t0[x] : T3
            ------------------------------------------- T-Abs
            _: G |- (fn x : T0 => t0[x]) : (T0 -> T3)
        is
            proof by unproved
        end case

        case rule
            _: G |- t0 : (T0 -> T1)
            _: G |- t1 : T0
            ----------------------------- T-App
            _: G |- (t0 t1) : T1
        is
            proof by unproved
        end case

        
    end induction
end theorem