; ***********************************************************
; ; Adapt path if necessary:
; (define path "~/minlog/examples/tait/diplomarbeit_schlenker/")

; ; Defines the function "pload" to load files 
; ; from the path defined above
; (define pload (lambda (x) (load (string-append path x))))

; ; Used Modules:
; (pload "./initiate.scm")
; (pload "./defsLamCalc.scm")
; (pload "./defsSubst.scm")
; (pload "./omega.scm")
; (pload "./defsNT.scm")
; (pload "./defsAxiomsSpecial.scm")
; (pload "./defsAxioms.scm")
; (pload "./trivial.scm")
; (pload "./auxSC.scm")

; NOTICE: Uncomment modules only when file is run on its own
; ***********************************************************


; =============================
;  Section: Global Auxiliaries
; =============================
; contains global auxiliaries used in more than one module

; Subsection: Miscellaneous
; =========================

; Lemma: "SubVar"
; ---------------
(set-goal (pf "all k,ss,m.
               k<Lh ss -> Sub(Var k) (Wrap m ss) = 
               (k thof ss)"))

(ind)
(ind)
(assume "m")
(auto)
(prop)
(auto)
(assume "n" "IHn")
(cases)
(assume "m")
(prop)
(auto)
(save "SubVar")

; Lemma: "TypJArrow"
; ------------------
(set-goal
 (pf "all rhos,rho,sig,r,s.
       TypJ rhos r (rho to sig) -> TypJ rhos s rho -> 
       TypJ rhos (r s) sig"))
(assume "rhos" "rho" "sig" "r" "s")
(assume 1 2)
(ng)
(split)(split)(split)
(use-with 1 'left)
(use-with 2 'left)
(simp-with 1 'right)
(simp-with 2 'right)
(ng)
(prop)
(simp-with 1 'right)
(ng)
(prop)
(save "TypJArrow")

; Lemma: "TypJTyp"
; ----------------
(set-goal
 (pf "all rhos,rho,r.
      TypJ rhos r rho -> rho = Typ rhos r"))
(assume "rhos" "rho" "r" 1)
(ng)
(simp-with "<-" 1 'right)
(prop)
(save "TypJTyp")


; Subsection: SCrs
; ================

; Lemma: "SCrsSTotal"
; -------------------
(set-goal (pf "all sigs,rhos,as^,ss.
 SCrs sigs rhos as^ ss -> STotal as^"))

(assume "sigs" "rhos" "as^" "ss")
(elim)
(assume "sigs1")
(use "STotalNilOmega")
(assume "sigs1" "rho" "rhos1" "a^" "as^1" 
 "s" "ss1" "H1" "H2" "H3" "H4")
(use "STotalConsOmega")
(use "H4")
(save "SCrsSTotal")

; Lemma: "SCrsLh"
; ---------------
(set-goal (pf "all sigs,rhos,as^,ss.SCrs sigs rhos as^ ss ->
 (Lh as^ =Lh rhos & Lh rhos=Lh ss)"))
(assume "sigs" "rhos" "as^" "ss")
(elim)
(strip)
(split)
(use "Truth-Axiom")
(use "Truth-Axiom")
(strip)
(use 4)
(save "SCrsLh")

; Lemma: "SCrsDefRev"
; -------------------
(add-global-assumption
 "SCrsDefRev"
 (pf "all sigs,rho,rhos,a^,as^,s,ss.
      SCrs sigs(rho::rhos)(a^ ::as^)(s::ss) ->
      (SCr sigs rho a^s & SCrs sigs rhos as^ss)"))
; proof by inversion

; Subsection: TypJExtCtx
; ======================

; Lemma: "TypJExtCtxAux1"
; -----------------------
(set-goal
 (pf "all rhos,r,s,sig.
      TypJ rhos (r s) sig -> TypJ rhos r ((Typ rhos s) to sig)"))

(assume "rhos" "r" "s" "sig" 1)
(ng)
(split)
(use-with 1 'left 'left 'left)
(assert (pf "Valtyp(Typ rhos r)=sig"))
(use-with 1 'right)
(assume 2)
(simp-with "<-" 2)
(use-with 1 'left 'right)
(save "TypJExtCtxAux1")

; Lemma: "TypJExtCtxAux2"
; -----------------------
(set-goal
 (pf "all rhos,r,s,sig.
      TypJ rhos (r s) sig -> TypJ rhos s (Typ rhos s)"))

(assume "rhos" "r" "s" "sig" 1)
(ng)
(use-with 1 'left 'left 'right)
(save "TypJExtCtxAux2")

; Lemma: "TypJExtCtx"
; -------------------
; auxiliary for "TypJAppIntro"

(set-goal
 (pf "all r,rhos,rho,sigs.
      TypJ rhos r rho -> TypJ (rhos :+: sigs) r rho"))

(ind)
; Base Case: r= Var n
(ind)
; Base Case: n=0
(assume "rhos" "rho" "sigs" 1)
(ng)
(split)
(assert (pf "0<Lh rhos"))
(use-with 1 'left)
(use "Trivial5")

(cases (pt "rhos"))
(assume 2)
(assert (pf "Lh rhos = 0"))
(simp-with 2)
(ng)
(prop)
(assume 3)

(assert (pf "0<Lh rhos -> F"))
(simp-with 3)
(use "Trivial6")
(assume 4)
(assert (pf "F"))
(use 4)
(use-with 1 'left)
(prop)

(assume "tau" "taus" 1)
(ng)
(assert (pf "Typ rhos(Var 0)=rho"))
(use-with 1 'right)
(simp-with 2)
(ng)
(prop)

(assume "n" "IH")
(cases)
(assume "rho" "sigs" 1)
(ng)
(prop)

(assume "rho" "rhos" "sig" "sigs" 1)
(ng)
(inst-with "IH" (pt "rhos") (pt "sig") (pt "sigs") 2)
(use 3)

;Step Case n+1
; Case rs
(assume "r" "s" "[IHr]" "[IHs]")
(assume "rhos" "sig" "sigs" "[TypJ]")
(inst-with-to "[IHr]" 
  (pt "rhos") (pt "((Typ rhos s) to sig)") (pt "sigs")
  "[IHr Inst]" )
(inst-with-to "[IHs]" 
  (pt "rhos") (pt "(Typ rhos s)") (pt "sigs") 
  "[IHs Inst]")

(assert (pf "TypJ rhos r(Typ rhos s to sig)"))
(use "TypJExtCtxAux1")
(use "[TypJ]")
(assume 6)
(inst-with "[IHr Inst]" 6)

(assert (pf "TypJ rhos s(Typ rhos s)"))
(use "TypJExtCtxAux2" (pt "r") (pt "sig"))
(use "[TypJ]")
(assume 8)

(inst-with "[IHs Inst]" 8)
(use "TypJArrow" (pt "(Typ rhos s)"))
(use 7)
(use 9)

; Case: Abs
(assume "rho" "r" "IH")
(assume "rhos" "sig" "sigs" 1)
(ng)
(inst-with "IH" (pt "rho::rhos") 
 (pt "(Typ(rho::rhos)r)") (pt "sigs"))
(ng)
(split)
(assert (pf "Cor(rho::rhos)r"))
(use-with 2 'left)
(assume 4)
(inst-with 3 4)
(use-with 5 'left)

(assert (pf "Cor(rho::rhos)r"))
(use-with 2 'left)
(assume 4)
(inst-with 3 4)
(simp-with 5 'right)
(use-with 2 'right)
(save "TypJExtCtx")


; Subsection: "TypJAppIntro"
; ==========================

; Lemma: "TypJAppIntro"
; ---------------------
(set-goal
(pf "all rhos,sigs,rho,sig,r,s.
     TypJ rhos r(rho to sig) -> TypJ(rhos:+:sigs)s rho -> 
     TypJ(rhos:+:sigs)(r s)sig"))

(assume "rhos" "sigs" "rho" "sig" "r" "s")
(assume 1 2)
(assert (pf "TypJ (rhos:+:sigs) r(rho to sig)"))
(use "TypJExtCtx")
(use 1)
(assume 3)
(use "TypJArrow" (pt "rho"))
(use 3)
(use 2)
(save "TypJAppIntro")


; Subsection: "TypJSub"
; =====================
; used for "Subject Reduction" and for an auxiliary for Lemma 3

; Definition: "TypJsSublist"
; --------------------------
; TypJ for a Sublist 
; (leads to easier proofs than with list of terms)

(add-program-constant "TypJsSublist" 
  (py "list type=> Sublist => list type=> boole") 1)

(add-computation-rule (pt "TypJsSublist sigs (Up n) (Nil type)")
		      (pt "T"))
(add-computation-rule (pt "TypJsSublist sigs (Up n) (rho::rhos)")
		      (pt "F"))
(add-computation-rule 
 (pt "TypJsSublist sigs (Dot r theta) (Nil type)")
 (pt "F"))
(add-computation-rule 
 (pt "TypJsSublist sigs (Dot r theta) (rho::rhos)")
 (pt "(TypJ sigs r rho) and (TypJsSublist sigs theta rhos)"))

; Definition: "TypJs"
; -------------------
; TypJ for a list of terms

(add-program-constant "TypJs" 
  (py "list type=> list term => list type=> boole") 1)

(add-computation-rule (pt "TypJs sigs ss rhos")
		      (pt "TypJsSublist sigs (Wrap 0 ss) rhos"))

; Lemma: "TypLiftAux1"
; --------------------
; auxiliary for "TypJLift"
(set-goal
 (pf "all sig, sigs, rhos,k. 
      k<Lh rhos -> 
      (Typ(rhos:+:(sig::sigs))(Var k)) = 
      (Typ(rhos:+:sigs)(Var k))"))

(assume "sig" "sigs")
(ind)
(assume "k" 1)
(ng)
(prop)

(assume "rho" "rhos" "IH")
(cases)
(assume 1)
(ng)
(prop)

(assume "n" 1)
(ng)
(use "IH")
(use 2)
(save "TypLiftAux1")

; Lemma: "TypLiftAux2"
; --------------------
; auxiliary for "TypJLift"

(set-goal
 (pf "all sig, sigs, rhos,k. 
      (k<Lh rhos -> F) -> 
      (Typ(rhos:+:(sig::sigs))(Var(Succ k))) =
      (Typ(rhos:+:sigs)(Var k))"))

(assume "sig" "sigs")
(ind)
(assume "k" 1)
(ng)
(prop)

(assume "rho" "rhos" "IH")
(cases)
(assume 1)
(ng)
(prop)

(assume "n" 1)
(ng)
(use "IH")
(use 2)
(save "TypLiftAux2")

; Lemma: "TypLift"
; ----------------
; auxiliary for "TypJLift"

(set-goal
 (pf "all sig,sigs,r,rhos,n.
      (Lh rhos = n) -> 
      (Typ (rhos:+:(sig::sigs)) (Lift r n 1)) = 
      (Typ (rhos:+:sigs) r)"))

(assume "sig" "sigs")
(ind)

; Case: Var k
(assume "k" "rhos" "n" "[Lh]")
(ng)
(casedist (pt "k<n"))
(assume 1)
(ng)
(simp "[Lh]")

(assert (pf "k<Succ(n+Lh sigs)"))
(use "Trivial8")
(use 2)
(assume 1)

(assert (pf "k<n+Lh sigs"))
(use "Trivial9")
(use 2)
(assume 1)
(use "TypLiftAux1" )
(simp "[Lh]")
(use 2)
(assume 1)
(ng)

(assert (pf "
  (Typ(rhos:+:(sig::sigs))(Var(Succ k))) =
  (Typ(rhos:+:sigs)(Var k))"))
(use "TypLiftAux2")
(simp "[Lh]")
(use 2)
(assume 1)
(simp 3)
(prop)

; Case: App
(assume "r" "s" "[IH r]" "[IH s]")
(assume "rhos" "n" "[Lh]")
(ng)
(assert 
 (pf "Typ(rhos:+:(sig::sigs))(Lift r n 1)=Typ(rhos:+:sigs)r"))
(use "[IH r]")
(use "[Lh]")
(assume 1)
(simp 4)
(prop)

; Case: Abs
(assume "rho" "r" "[IH]")
(assume "rhos" "n" "[Lh]")
(ng)
(inst-with "[IH]" (pt "rho::rhos") (pt "Succ n"))
(use 3)
(ng)
(use "[Lh]")
(save "TypLift")

; Lemma: "CorLift"
; -------------------
; auxiliary for "TypJLift"

(set-goal
 (pf "all sig,sigs,r,rhos,n.
      (Lh rhos = n) -> 
      (Cor (rhos:+:(sig::sigs)) (Lift r n 1)) = 
      (Cor (rhos:+:sigs) r)"))

(assume "sig" "sigs")
(ind)
(assume "k" "rhos" "n" "[Lh]")
(ng)
(casedist (pt "k<n"))
(assume 1)
(ng)
(simp "[Lh]")

(assert (pf "k<Succ(n+Lh sigs)"))
(use "Trivial8")
(use 2)
(assume 1)

(assert (pf "k<n+Lh sigs"))
(use "Trivial9")
(use 2)
(assume 1)
(simp 3)
(simp 4)
(ng)
(prop)
(assume 1)
(ng)
(prop)

;Case App
(assume "r" "s" "[IH r]" "[IH s]" )
(assume "rhos" "n" "[Lh]")
(ng)

(inst-with "[IH r]" (pt "rhos") (pt "n") "[Lh]")
(simp 4)
(inst-with "[IH s]" (pt "rhos") (pt "n") "[Lh]")
(simp 5)

(assert (pf "Typ(rhos:+:(sig::sigs))(Lift r n 1) =
             Typ(rhos:+:sigs)r"))
(use "TypLift")
(use "[Lh]")
(assume 1)
(simp-with 6)

(assert (pf "Typ(rhos:+:(sig::sigs))(Lift s n 1) =
             Typ(rhos:+:sigs)s"))
(use "TypLift")
(use "[Lh]")
(assume 1)
(simp-with 7)

(assert (pf "Valtyp(Typ(rhos:+:(sig::sigs))(Lift r n 1)) =
             Valtyp(Typ(rhos:+:sigs)r)"))
(simp-with 6)
(prop)
(assume 1)

(assert (pf "
  (Typ(rhos:+:(sig::sigs))(Lift s n 1)
    to Valtyp(Typ(rhos:+:(sig::sigs))(Lift r n 1))) =
  (Typ(rhos:+:sigs)s to Valtyp(Typ(rhos:+:sigs)r))"))
(simp-with 7)
(ng)
(simp 8)
(prop)

(assume 1)
(simp 9)
(ng)
(prop)

; Case: Abs
(assume "rho" "r" "[IH]")
(assume "rhos" "n" "[Lh]")
(ng)
(inst-with "[IH]" (pt "rho::rhos") (pt "Succ n"))
(use 3)
(ng)
(use "[Lh]")
(save "CorLift")

; Lemma: "TypJLift"
; -----------------
; auxiliary for "TypJsSubliftAux"

(set-goal
 (pf "all rhos,sig,sigs,rho,n,r.
      (Lh rhos = n) -> 
      (TypJ (rhos:+:(sig::sigs)) (Lift r n 1) rho) = 
      (TypJ (rhos:+:sigs) r rho)"))

(assume "rhos" "sig" "sigs" "rho" "n" "r" "[Lh]")
(ng)
(simp "CorLift")
(simp "TypLift")
(auto)
(save "TypJLift")

; Lemma: "TypJsSubliftAux"
; ------------------------
;
(set-goal
 (pf "all sig,sigs,rho,r.
      TypJ (sig::sigs) (Lift r 0 1) rho = 
      TypJ sigs r rho"))

(assume "sig" "sigs" "rho" "r")
(assert (pf "(TypJ ((Nil type):+:(sig::sigs)) (Lift r 0 1) rho) = 
      (TypJ ((Nil type):+:sigs) r rho)"))
(use "TypJLift")
(ng)
(prop)
(assume 1)
(assert (pf "(sig::sigs) = (Nil type):+:(sig::sigs)"))
(ng)
(prop)
(assume 2)
(simp 2)
(use 1)
(save "TypJsSubliftAux")

; Lemma: "TypJsSublift"
; ---------------------
(set-goal
  (pf "all sig, sigs, theta, rhos.
  TypJsSublist(sig::sigs)(Sublift theta 1)rhos = 
  TypJsSublist sigs theta rhos"))

(assume "sig" "sigs")
(ind)

; Case: theta = Up n
(cases)
(cases)
(ng)
(prop)

(assume "rho" "rhos")
(ng)
(prop)

(assume "n")
(cases)
(ng)
(prop)

(assume "rho" "rhos")
(ng)
(prop)

; Case: theta = Dot r theta
(assume "r" "theta" "[IH]")
(cases)
(ng)
(prop)

(assume "rho" "rhos")
(assert
 (pf "TypJ (sig::sigs) (Lift r 0 1) rho = 
      TypJ sigs r rho")) 
(use "TypJsSubliftAux")
(assume 2)
(ng)
(simp 2) 
(inst-with "[IH]" (pt "rhos"))
(simp 3)
(ng)
(prop)
(save "TypJsSublift")

; Lemma: "TypJSub"
; ----------------
(set-goal
 (pf "all r,rhos, theta, sigs,rho.TypJ rhos r rho ->
      TypJsSublist sigs theta rhos -> 
      TypJ sigs (Sub r theta) rho"))

(ind)
(ind)
(cases)
(cases) 
(assume "n" "sigs" "rho" "[TypJ]" "[TypJsSublist]")

(ng)
(prop)

(assume "r" "theta" "sigs" "rho" "[TypJ]" "[TypJsSublist]")
(ng)
(prop)

(assume "rho" "rhos")
(cases)
(assume "n" "sigs" "tau" "[TypJ]" "[TypJsSublist]")
(ng)
(prop)

(assume "r" "theta" "sigs" "tau" "[TypJ]" "[TypJsSublist]")
(ng)
(simp "<-" "[TypJ]")
(use-with "[TypJsSublist]" 'left)

; Case r = Succ k
(assume "n" "[IH]")
(cases)
(cases)
(assume "k" "sigs" "tau" "[TypJ]" "[TypJsSublist]")
(ng)
(prop)

(assume "r" "theta" "sigs" "rho" "[TypJ]" "[TypJsSublist]")
(ng)
(prop)

(assume "rho" "rhos")
(cases)
(assume "k" "sigs" "tau" "[TypJ]" "[TypJsSublist]")
(ng)
(prop)

(assume "r" "theta" "sigs" "tau" "[TypJ]" "[TypJsSublist]")
(ng)
(use "[IH]" (pt "rhos"))
(use "[TypJ]")
(use-with "[TypJsSublist]" 'right)

; Case: App
(assume "r" "s" "[IH r]" "[IH s]")
(assume "rhos" "theta" "sigs" "tau" "[TypJ]" "[TypJsSublist]")
(ng)

(assert (pf "Cor sigs(Sub s theta) and
             Typ sigs(Sub s theta)=Typ rhos s"))
(use "[IH s]" (pt "rhos"))
(split)
(use-with "[TypJ]" 'left 'left 'right)
(prop)
(use "[TypJsSublist]")
(assume "[Part s]")

(assert (pf "Cor sigs(Sub r theta) and
  Typ sigs(Sub r theta)=(Typ sigs(Sub s theta)to tau)"))
(use "[IH r]" (pt "rhos"))
(split)
(use-with "[TypJ]" 'left 'left 'left)  
(assert (pf "Valtyp(Typ rhos r)=tau"))
(use-with "[TypJ]" 'right)
(assume "[Simp 1]")

(assert (pf "Typ rhos r=(Typ rhos s to Valtyp(Typ rhos r))"))
(use-with "[TypJ]" 'left 'right)  
(assume "[Simp 2]")
(simp "[Simp 2]")
(simp "[Simp 1]")
(ng)
(use "Symmetry")
(use-with "[Part s]" 'right)
(use "[TypJsSublist]")
(assume "[Part r]")
(split)
(split)
(split)
(use-with "[Part r]" 'left)
(use-with "[Part s]" 'left)

(simp (pf "Valtyp(Typ sigs(Sub r theta))=tau"))

(use-with "[Part r]" 'right)
(simp-with 
 (pf "Typ sigs(Sub r theta)=(Typ sigs(Sub s theta)to tau)"))
(ng)
(prop)
(use-with "[Part r]" 'right)

(simp-with 
 (pf "Typ sigs(Sub r theta)=(Typ sigs(Sub s theta)to tau)"))
(ng)
(prop)
(use-with "[Part r]" 'right)

; Case: Abs
(get 4)
(assume "rho" "r" "[IH]")
(assume "rhos" "theta" "sigs" "tau" "[TypJ]" "[TypJsSublist]") 
(ng)
(simp-with "<-" (pf "(rho to Typ(rho::rhos)r)=tau"))
(ng)
(use "[IH]" (pt "rho::rhos"))
(split)
(use-with "[TypJ]" 'left)
(prop)
(ng)
(simp "TypJsSublift")
(use "[TypJsSublist]")
(use-with "[TypJ]" 'right)
(save "TypJSub")