Implementing a typechecker for Quantitative Type Theory

#Typechecker for QTT

This gist contains an implementation for a typechecker for Quantitative Type Theory (QTT), in Isabelle/HOL.

QTT.thy

theory QTT
  imports
    Main
    "HOL.Groups"
begin

class semiring = zero + one + plus + times +
  assumes multiplicative_monoid: \<open>monoid (*) 1\<close>
      and additive_comm_monoid: \<open>comm_monoid (+) 0\<close>
      and distrib_times_plus: \<open>(a + b) * c = (a * c) + (b * c)\<close>
      and times_zero_left: \<open>0 * \<rho> = 0\<close>
      and times_zero_right: \<open>\<rho> * 0 = 0\<close>

class resource_semiring = semiring +
  assumes positiveness: \<open>\<rho> + \<pi> = 0 \<Longrightarrow> \<rho> = 0 \<and> \<pi> = 0\<close>
      and zero_product: \<open>\<rho> * \<pi> = 0 \<Longrightarrow> \<rho> = 0 \<or> \<pi> = 0\<close>

text \<open>
  A multiplicity is one of:
  \<^item> \<open>0\<close>, meaning erased;
  \<^item> \<open>1\<close>, meaning linear;
  \<^item> \<open>\<omega>\<close>, meaning unrestricted.
\<close>

datatype multiplicity =
  Zero | One | Many (\<open>\<omega>\<close>)

fun plus_mult :: \<open>multiplicity \<Rightarrow> multiplicity \<Rightarrow> multiplicity\<close>
where \<open>plus_mult Zero \<rho> = \<rho>\<close>
    | \<open>plus_mult \<rho> Zero = \<rho>\<close>
    | \<open>plus_mult One One = Many\<close>
    | \<open>plus_mult Many _ = Many\<close>
    | \<open>plus_mult _ Many = Many\<close>

fun times_mult :: \<open>multiplicity \<Rightarrow> multiplicity \<Rightarrow> multiplicity\<close>
where \<open>times_mult Zero _ = Zero\<close>
    | \<open>times_mult _ Zero = Zero\<close>
    | \<open>times_mult One \<rho> = \<rho>\<close>
    | \<open>times_mult \<rho> One = \<rho>\<close>
    | \<open>times_mult Many Many = Many\<close>

text \<open>
  We make sure that @{typ multiplicity} together with @{const plus_mult} and @{const times_mult} is a
  valid resource semiring.
\<close>

instantiation multiplicity :: \<open>{zero, one, plus, times}\<close>
begin
  definition \<open>0 \<equiv> Zero\<close>
  definition \<open>1 \<equiv> One\<close>
  definition \<open>(+) \<equiv> plus_mult\<close>
  definition \<open>(*) \<equiv> times_mult\<close>

  instance ..
end (* instantiation multiplicity :: {plus, times} *)

lemma multiplicative_semigroup_mult: \<open>semigroup ((*) :: multiplicity \<Rightarrow> multiplicity \<Rightarrow> multiplicity)\<close>
  unfolding times_multiplicity_def
  by (smt (verit, del_insts) multiplicity.exhaust semigroup.intro times_mult.simps)

interpretation times_semigroup_mult: semigroup \<open>(*) :: multiplicity \<Rightarrow> multiplicity \<Rightarrow> multiplicity\<close>
  by (rule multiplicative_semigroup_mult)

lemma multiplicative_monoid_mult: \<open>monoid (*) (1 :: multiplicity)\<close>
  unfolding one_multiplicity_def times_multiplicity_def
  by (smt (z3) monoid.intro monoid_axioms.intro multiplicative_semigroup_mult multiplicity.distinct(2) times_mult.elims times_multiplicity_def)

interpretation times_one_monoid_mult: monoid \<open>(*)\<close> \<open>1 :: multiplicity\<close>
  by (rule multiplicative_monoid_mult)

lemma additive_semigroup_mult: \<open>semigroup ((+) :: multiplicity \<Rightarrow> multiplicity \<Rightarrow> multiplicity)\<close>
  unfolding plus_multiplicity_def
  by (smt (verit, del_insts) multiplicity.exhaust plus_mult.simps semigroup.intro)

interpretation plus_semigroup_mult: semigroup \<open>(+) :: multiplicity \<Rightarrow> multiplicity \<Rightarrow> multiplicity\<close>
  by (rule additive_semigroup_mult)

lemma additive_abel_semigroup_mult: \<open>abel_semigroup ((+) :: multiplicity \<Rightarrow> multiplicity \<Rightarrow> multiplicity)\<close>
  unfolding plus_multiplicity_def
  by (smt (verit, best) abel_semigroup.intro abel_semigroup_axioms_def additive_semigroup_mult multiplicity.exhaust plus_mult.simps plus_multiplicity_def)

interpretation plus_abel_semigroup_mult: abel_semigroup \<open>(+) :: multiplicity \<Rightarrow> multiplicity \<Rightarrow> multiplicity\<close>
  by (rule additive_abel_semigroup_mult)

lemma commutative_additive_monoid_mult: \<open>comm_monoid (+) (0 :: multiplicity)\<close>
  unfolding zero_multiplicity_def plus_multiplicity_def
  by (smt (z3) additive_abel_semigroup_mult comm_monoid.intro comm_monoid_axioms.intro multiplicity.distinct(2) multiplicity.simps(4) plus_mult.elims plus_multiplicity_def)

interpretation plus_zero_commutative_monoid_mult: comm_monoid \<open>(+)\<close> \<open>0 :: multiplicity\<close>
  by (rule commutative_additive_monoid_mult)

instance multiplicity :: \<open>semiring\<close>
proof standard
  show \<open>monoid (*) (1 :: multiplicity)\<close>
    by (simp add: multiplicative_monoid_mult)
  show \<open>comm_monoid (+) (0 :: multiplicity)\<close>
    by (simp add: commutative_additive_monoid_mult)
  show \<open>\<And> a b c :: multiplicity. (a + b) * c = a * c + b * c\<close>
    unfolding plus_multiplicity_def times_multiplicity_def
    by (smt (verit, ccfv_threshold) multiplicity.exhaust plus_mult.simps times_mult.simps)
  show \<open>\<And> \<rho> :: multiplicity. 0 * \<rho> = 0\<close>
    by (simp add: times_multiplicity_def zero_multiplicity_def)
  show \<open>\<And> \<rho> :: multiplicity. \<rho> * 0 = 0\<close>
    using times_mult.elims times_multiplicity_def zero_multiplicity_def
    by auto
qed

instance multiplicity :: \<open>resource_semiring\<close>
proof standard
  show \<open>\<And> \<rho> \<pi> :: multiplicity. \<rho> + \<pi> = 0 \<Longrightarrow> \<rho> = 0 \<and> \<pi> = 0\<close>
    using plus_mult.elims plus_multiplicity_def zero_multiplicity_def
    by auto
  show \<open>\<And> \<rho> \<pi> :: multiplicity. \<rho> * \<pi> = 0 \<Longrightarrow> \<rho> = 0 \<or> \<pi> = 0\<close>
    using times_mult.elims times_multiplicity_def
    by force
qed

text \<open>
  Naturals numbers @{typ nat}, together with @{const plus} and @{const times} form a resource semiring.
  A natural number means a number of runtime usage.
\<close>

instance nat :: \<open>semiring\<close>
proof standard
  show \<open>monoid (*) (1 :: nat)\<close>
    using mult.monoid_axioms
    by blast
  show \<open>comm_monoid (+) (0 :: nat)\<close>
    by (simp add: add.comm_monoid_axioms)
  show \<open>\<And> a b c :: nat. (a + b) * c = a * c + b * c\<close>
    using add_mult_distrib
    by force
  show \<open>\<And> \<rho> :: nat. 0 * \<rho> = 0\<close>
    by force
  show \<open>\<And> \<rho> :: nat. \<rho> * 0 = 0\<close>
    by simp
qed

instance nat :: \<open>resource_semiring\<close>
proof standard
  show \<open>\<And> \<rho> \<pi> :: nat. \<rho> + \<pi> = 0 \<Longrightarrow> \<rho> = 0 \<and> \<pi> = 0\<close>
    by fastforce
  show \<open>\<And> \<rho> \<pi> :: nat. \<rho> * \<pi> = 0 \<Longrightarrow> \<rho> = 0 \<or> \<pi> = 0\<close>
    by auto
qed

text \<open>
  Booleans @{typ bool}, together with @{const disj} and @{const conj} form a resource semiring where:
  \<^item> @{const True} means "Present"
  \<^item> @{const False} means "Erased"
\<close>

instantiation bool :: \<open>{zero, one, plus, times}\<close>
begin
  definition \<open>0 \<equiv> False\<close>
  definition \<open>1 \<equiv> True\<close>
  definition \<open>(+) = (\<or>)\<close>
  definition \<open>(*) = (\<and>)\<close>

  instance ..
end (* instantiation bool :: {zero, one, plus, times} *)

instance bool :: \<open>semiring\<close>
proof standard
  show \<open>monoid (*) (1 :: bool)\<close>
    unfolding times_bool_def one_bool_def
    by (simp add: conj.monoid_axioms)
  show \<open>comm_monoid (+) (0 :: bool)\<close>
    unfolding plus_bool_def zero_bool_def
    by (simp add: disj.comm_monoid_axioms)
  show \<open>\<And> a b c :: bool. (a + b) * c = a * c + b * c\<close>
    unfolding plus_bool_def times_bool_def
    by meson
  show \<open>\<And> \<rho> :: bool. 0 * \<rho> = 0\<close>
    unfolding times_bool_def zero_bool_def
    by simp
  show \<open>\<And> \<rho> :: bool. \<rho> * 0 = 0\<close>
    unfolding times_bool_def zero_bool_def
    by blast
qed

instance bool :: \<open>resource_semiring\<close>
proof standard
  show \<open>\<And> \<rho> \<pi> :: bool. \<rho> + \<pi> = 0 \<Longrightarrow> \<rho> = 0 \<and> \<pi> = 0\<close>
    unfolding plus_bool_def zero_bool_def
    by meson
  show \<open>\<And> \<rho> \<pi> :: bool. \<rho> * \<pi> = 0 \<Longrightarrow> \<rho> = 0 \<or> \<pi> = 0\<close>
    unfolding times_bool_def zero_bool_def
    by blast
qed

(*************************************************************************************)
(*************************************************************************************)
(*************************************************************************************)

datatype ('v, 'm :: resource_semiring) preterm =
  Var 'v
| Lambda 'v 'm \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close>
    (\<open>\<lambda>/ _/ \<Ztypecolon>\<^bsup>_\<^esup>/ _./ _\<^bsup>_\<^esup>\<close>)
| Appl 'v 'm \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close>
    (\<open>App\<^bsub>'(_/ \<Ztypecolon>\<^bsup>_\<^esup>/ _')/ (_)\<^esub>'(_,/ _')\<close>)
| Pair \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close> 'v 'm \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close>
    (\<open>'(_,/ _')\<^bsub>_/ \<Ztypecolon>\<^bsup>_\<^esup>/ _./ _\<^esub>\<close>)
| Unit
    (\<open>\<star>\<close>)
| Fst 'v 'm \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close>
    (\<open>fst\<^bsub>_/ \<Ztypecolon>\<^bsup>_\<^esup>/ _./ _\<^esub>/ _\<close>)
| Snd 'v 'm \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close>
    (\<open>snd\<^bsub>_/ \<Ztypecolon>\<^bsup>_\<^esup>/ _./ _\<^esub>/ _\<close>)
| LetPair 'v 'm \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close> 'v 'v 'v \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close>
    (\<open>let\<^bsub>_/ \<Ztypecolon>\<^bsup>_\<^esup>/ _./ _\<^esub>/ '(_,/ _')\<^bsub>'(_')\<^esub>/ =/ _/ in/ _\<close>)
| LetI 'v \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close>
    (\<open>let\<^sub>I/ \<star>\<^bsub>'(_')\<^esub>/ =/ _/ in/ _\<close>)
| TrueC
    (\<open>true\<close>)
| FalseC
    (\<open>false\<close>)
| If 'v \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close>
    (\<open>ElimBool\<^bsub>'(_')/ _\<^esub>'(_,/ _,/ _')\<close>)
| Pi 'v 'm \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close>
    (\<open>'(_/ \<Ztypecolon>\<^bsup>_\<^esup>/ _')/ \<rightarrow>/ _\<close>)
| Sigma 'v 'm \<open>('v, 'm) preterm\<close> \<open>('v, 'm) preterm\<close>
    (\<open>'(_/ \<Ztypecolon>\<^bsup>_\<^esup>/ _')/ \<otimes>/ _\<close>)
| I
| Bool
| El \<open>('v, 'm) preterm\<close>
| Set

datatype ('v, 'm :: resource_semiring) precontext =
  Empty
    (\<open>\<diamond>\<close>)
| Cons \<open>('v, 'm) precontext\<close> 'v 'm \<open>('v, 'm) preterm\<close>
    (\<open>_,/ _\<Ztypecolon>\<^bsup>_\<^esup>/ _\<close> [50, 30, 50] 50)

fun is_Empty :: \<open>('v, 'm :: resource_semiring) precontext \<Rightarrow> bool\<close>
where \<open>is_Empty \<diamond> = True\<close>
    | \<open>is_Empty (_, _ \<Ztypecolon>\<^bsup>_\<^esup> _) = False\<close>

fun split_precontext :: \<open>('v, 'm :: resource_semiring) precontext \<Rightarrow> 'v \<Rightarrow> 'm \<Rightarrow> ('v, 'm) preterm \<Rightarrow> ('v, 'm) precontext \<Rightarrow> ('v, 'm) precontext\<close>
                        (\<open>_/ @/ _/ \<Ztypecolon>\<^bsup>_\<^esup>/ _/ @/ _\<close> [60, 30, 30, 30, 60] 60)
where \<open>\<Gamma>\<^sub>1 @ x \<Ztypecolon>\<^bsup>\<rho>\<^esup> S @ \<diamond> = (\<Gamma>\<^sub>1, x \<Ztypecolon>\<^bsup>\<rho>\<^esup> S)\<close>
    | \<open>\<Gamma>\<^sub>1 @ x \<Ztypecolon>\<^bsup>\<rho>\<^esup> S @ (\<Gamma>\<^sub>2, y \<Ztypecolon>\<^bsup>\<pi>\<^esup> T) = ((\<Gamma>\<^sub>1 @ x \<Ztypecolon>\<^bsup>\<rho>\<^esup> S @ \<Gamma>\<^sub>2), y \<Ztypecolon>\<^bsup>\<pi>\<^esup> T)\<close>

fun to_set :: \<open>('v, 'm :: resource_semiring) precontext \<Rightarrow> ('v \<times> 'm \<times> ('v, 'm) preterm) set\<close>
where \<open>to_set \<diamond> = {}\<close>
    | \<open>to_set (\<Gamma>, x \<Ztypecolon>\<^bsup>\<rho>\<^esup> A) = insert (x, \<rho>, A) (to_set \<Gamma>)\<close>

fun scale :: \<open>('m :: resource_semiring) \<Rightarrow> ('v, 'm) precontext \<Rightarrow> ('v, 'm) precontext\<close>
             (infix \<open>\<cdot>\<close> 80)
where \<open>\<pi> \<cdot> \<diamond> = \<diamond>\<close>
    | \<open>\<pi> \<cdot> (\<Gamma>, x \<Ztypecolon>\<^bsup>\<rho>\<^esup> A) = ((\<pi> \<cdot> \<Gamma>), x \<Ztypecolon>\<^bsup>\<pi> * \<rho>\<^esup> A)\<close>

lemma context_zeroing: \<open>\<forall> (x, \<rho>, A) \<in> to_set (0 \<cdot> \<Gamma>). \<rho> = 0\<close>
  by (induct \<Gamma>, auto simp add: times_zero_left)

lemma scale_by_one_is_identity: \<open>1 \<cdot> \<Gamma> = \<Gamma>\<close>
  by (induct \<Gamma>, auto simp add: monoid.left_neutral multiplicative_monoid)

lemma to_set_of_split [simp]: \<open>to_set (\<Gamma>\<^sub>1 @ x \<Ztypecolon>\<^bsup>\<rho>\<^esup> A @ \<Gamma>\<^sub>2) = to_set \<Gamma>\<^sub>1 \<union> {(x, \<rho>, A)} \<union> to_set \<Gamma>\<^sub>2\<close>
  by (induct rule: to_set.induct; simp)

inductive add_precontext :: \<open>('v, 'm :: resource_semiring) precontext \<Rightarrow> ('v, 'm) precontext \<Rightarrow> ('v, 'm) precontext \<Rightarrow> bool\<close>
where add_Empty: \<open>add_precontext \<diamond> \<diamond> \<diamond>\<close>
    | add_Cons: \<open>add_precontext \<Gamma>\<^sub>1 \<Gamma>\<^sub>2 \<Gamma>\<^sub>3 \<Longrightarrow> add_precontext (\<Gamma>\<^sub>1, x \<Ztypecolon>\<^bsup>\<rho>\<^esup> A) (\<Gamma>\<^sub>2, x \<Ztypecolon>\<^bsup>\<pi>\<^esup> A) (\<Gamma>\<^sub>3, x \<Ztypecolon>\<^bsup>\<rho> * \<pi>\<^esup> A)\<close>

code_pred add_precontext .

lemma add_precontext_output_unique: \<open>0 \<cdot> \<Gamma>\<^sub>1 = 0 \<cdot> \<Gamma>\<^sub>2 \<Longrightarrow> (\<exists>! \<Gamma>\<^sub>3. add_precontext \<Gamma>\<^sub>1 \<Gamma>\<^sub>2 \<Gamma>\<^sub>3)\<close>
proof (induct \<Gamma>\<^sub>1 arbitrary: \<Gamma>\<^sub>2)
  case Empty
  then show ?case
    by (smt (verit, del_insts) add_precontext.simps precontext.simps(3) scale.elims)
next
  case (Cons \<Gamma>\<^sub>1' x \<rho> A \<Gamma>\<^sub>2)
  then obtain \<Gamma>\<^sub>2' \<pi> where \<Gamma>\<^sub>2_is: \<open>\<Gamma>\<^sub>2 = (\<Gamma>\<^sub>2', x \<Ztypecolon>\<^bsup>\<pi>\<^esup> A)\<close>
    by (smt (verit, ccfv_SIG) precontext.inject scale.elims)
  then have \<open>0 \<cdot> \<Gamma>\<^sub>1' = 0 \<cdot> \<Gamma>\<^sub>2'\<close>
    using Cons.prems
    by auto
  then have \<open>\<exists>! \<Gamma>\<^sub>3. add_precontext \<Gamma>\<^sub>1' \<Gamma>\<^sub>2' \<Gamma>\<^sub>3\<close>
    using Cons.hyps
    by presburger
  then obtain \<Gamma>\<^sub>3 where \<open>add_precontext \<Gamma>\<^sub>1' \<Gamma>\<^sub>2' \<Gamma>\<^sub>3\<close>
                   and unique_addition_output: \<open>\<forall> \<Gamma>\<^sub>3'. add_precontext \<Gamma>\<^sub>1' \<Gamma>\<^sub>2' \<Gamma>\<^sub>3' \<longrightarrow> \<Gamma>\<^sub>3 = \<Gamma>\<^sub>3'\<close>
    by blast
  then have \<open>add_precontext (\<Gamma>\<^sub>1', x \<Ztypecolon>\<^bsup>\<rho>\<^esup> A) (\<Gamma>\<^sub>2', x \<Ztypecolon>\<^bsup>\<pi>\<^esup> A) (\<Gamma>\<^sub>3, x \<Ztypecolon>\<^bsup>\<rho> * \<pi>\<^esup> A)\<close>
    by (meson add_Cons)
  then show ?case
    by (smt (verit, del_insts) \<Gamma>\<^sub>2_is add_precontext.cases precontext.distinct(1) precontext.inject unique_addition_output)
qed

instantiation precontext :: (type, resource_semiring) plus
begin
  definition \<open>0 \<cdot> \<Gamma>\<^sub>1 = 0 \<cdot> \<Gamma>\<^sub>2 \<Longrightarrow> \<Gamma>\<^sub>1 + \<Gamma>\<^sub>2 \<equiv> (THE \<Gamma>\<^sub>3. add_precontext \<Gamma>\<^sub>1 \<Gamma>\<^sub>2 \<Gamma>\<^sub>3)\<close>
    \<comment>\<open>Thanks to @{thm add_precontext_output_unique}, we know that there is a single result.\<close>

  instance ..
end (* instantiation precontext :: (type, resource_semiring) plus *)

text \<open>
  Substitution is the process of replacing a free variable in a term with a given term.
  For example, \<^text>\<open>(f x y)[0 / x] \<equiv> f 0 y\<close>.
  We only need to be careful about not accidentally substituting a bound variable: \<^text>\<open>(\<lambda> x. f x y)[0 / x] \<equiv> (\<lambda> x. f x y)\<close>.
\<close>

no_notation Fields.inverse_class.inverse_divide (infixl \<open>'/\<close> 70)

fun preterm_substitute :: \<open>('v, 'm :: resource_semiring) preterm \<Rightarrow> ('v, 'm) preterm \<Rightarrow> 'v \<Rightarrow> ('v, 'm) preterm\<close>
                          (\<open>_[_'/_]\<close> [70, 30, 30] 70)
where \<open>(Var x)[e / y] = (if x = y then e else Var x)\<close>
    | \<open>(\<lambda> x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. M\<^bsup>T\<^esup>)[e / y] = \<lambda> x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S[e / y]. (if x = y then M else M[e / y])\<^bsup>T[e / y]\<^esup>\<close>
    | \<open>(App\<^bsub>(x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S) T\<^esub>(M, N))[e / y] = App\<^bsub>(x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S[e / y]) if x = y then T else T[e / y]\<^esub>(M[e / y], N[e / y])\<close>
    | \<open>((M, N)\<^bsub>x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S. T\<^esub>)[e / y] = (M[e / y], N[e / y])\<^bsub>x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S[e / y]. if x = y then T else T[e / y]\<^esub>\<close>
    | \<open>\<star>[_ / _] = \<star>\<close>
    | \<open>(fst\<^bsub>x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S. T\<^esub> M)[e / y] = fst\<^bsub>x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S[e / y]. if x = y then T else T[e / y]\<^esub> (M[e / y])\<close>
    | \<open>(snd\<^bsub>x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S. T\<^esub> M)[e / y] = snd\<^bsub>x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S[e / y]. if x = y then T else T[e / y]\<^esub> (M[e / y])\<close>
    | \<open>(let\<^bsub>x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S. T\<^esub> (a, b)\<^bsub>(z)\<^esub> = M in N)[e / y] = let\<^bsub>x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S[e / y]. if x = y then T else T[e / y]\<^esub> (a, b)\<^bsub>(z)\<^esub> = M[e / y] in (if y = a \<or> y = b \<or> y = z then N else N[e / y])\<close>
    | \<open>(let\<^sub>I \<star>\<^bsub>(z)\<^esub> = M in N)[e / y] = let\<^sub>I \<star>\<^bsub>(z)\<^esub> = M[e / y] in (if y = z then N else N[e / y])\<close>
    | \<open>true[_ / _] = true\<close>
    | \<open>false[_ / _] = false\<close>
    | \<open>(ElimBool\<^bsub>(z) T\<^esub>(M\<^sub>t, M\<^sub>f, N))[e / y] = ElimBool\<^bsub>(z) if y = z then T else T[e / y]\<^esub>(if y = z then M\<^sub>t else M\<^sub>t[e / y], if y = z then M\<^sub>f else M\<^sub>f[e / y], N[e / y])\<close>
    | \<open>((x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<rightarrow> T)[e / y] = (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S[e / y]) \<rightarrow> (if x = y then T else T[e / y])\<close>
    | \<open>((x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T)[e / y] = (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S[e / y]) \<otimes> (if x = y then T else T[e / y])\<close>
    | \<open>I[_ / _] = I\<close>
    | \<open>Bool[_ / _] = Bool\<close>
    | \<open>(El M)[e / y] = El (M[e / y])\<close>
    | \<open>Set[_ / _] = Set\<close>

lemma \<open>x \<noteq> y \<Longrightarrow> (\<lambda> x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S. M\<^bsup>T\<^esup>)[\<star> / y] \<equiv> (\<lambda> x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S[\<star> / y]. M[\<star> / y]\<^bsup>T[\<star> / y]\<^esup>)\<close>
  by simp

lemma \<open>(\<lambda> x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S. M\<^bsup>T\<^esup>)[\<star> / x] = (\<lambda> x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S[\<star> / x]. M\<^bsup>T[\<star> / x]\<^esup>)\<close>
  by simp

text \<open>
  We then define pretype formation, precontext welformedness and type-checking rules, as well as type and term equality.
\<close>

inductive to_normal_form :: \<open>('v, 'm :: resource_semiring) precontext \<Rightarrow> ('v, 'm) preterm \<Rightarrow> ('v, 'm) preterm \<Rightarrow> 'm \<Rightarrow> ('v, 'm) preterm \<Rightarrow> bool\<close>
                            (\<open>_/ \<turnstile>/ _/ \<leadsto>\<^sup>*\<^bsub>_\<^esub>\<^bsup>_\<^esup>/ _\<close> [30, 20, 20, 20, 30] 30)
where nf_Var: \<open>\<Gamma>\<^sub>1 @ x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> T @ \<Gamma>\<^sub>2 \<turnstile> Var x \<leadsto>\<^sup>*\<^bsub>T\<^esub>\<^bsup>\<sigma>\<^esup> Var x\<close>
    | nf_\<beta>: \<open>\<Gamma> \<turnstile> M[N / y] \<leadsto>\<^sup>*\<^bsub>T[N / y]\<^esub>\<^bsup>\<sigma>\<^esup> M' \<Longrightarrow> \<Gamma> \<turnstile> App\<^bsub>(x \<Ztypecolon>\<^bsup>\<sigma>\<^esup> (y \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<rightarrow> T) U\<^esub>(\<lambda> y \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. M\<^bsup>T\<^esup>, N) \<leadsto>\<^sup>*\<^bsub>T[N / y]\<^esub>\<^bsup>\<sigma>\<^esup> M'\<close>
    | nf_Lambda: \<open>(\<Gamma>, x \<Ztypecolon>\<^bsup>\<pi> * \<sigma>\<^esup> S) \<turnstile> M \<leadsto>\<^sup>*\<^bsub>T[Var x / x]\<^esub>\<^bsup>\<sigma>\<^esup> M' \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda> x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. M\<^bsup>T\<^esup>) \<leadsto>\<^sup>*\<^bsub>(x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<rightarrow> T\<^esub>\<^bsup>\<sigma>\<^esup> (\<lambda> x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. M'\<^bsup>T\<^esup>)\<close>
    | nf_App: \<open>\<Gamma> \<turnstile> M \<leadsto>\<^sup>*\<^bsub>(x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<rightarrow> T\<^esub>\<^bsup>\<sigma>\<^esup> M' \<Longrightarrow> \<Gamma> \<turnstile> N \<leadsto>\<^sup>*\<^bsub>T[M' / x]\<^esub>\<^bsup>\<sigma>\<^esup> N' \<Longrightarrow> \<Gamma> \<turnstile> App\<^bsub>(x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) T\<^esub>(M, N) \<leadsto>\<^sup>*\<^bsub>T\<^esub>\<^bsup>\<sigma>\<^esup> App\<^bsub>(x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) T\<^esub>(M', N')\<close>
    | nf_Pair: \<open>\<Gamma> \<turnstile> M \<leadsto>\<^sup>*\<^bsub>S\<^esub>\<^bsup>\<sigma> * \<pi>\<^esup> M' \<Longrightarrow> (\<Gamma>, x \<Ztypecolon>\<^bsup>0\<^esup> S) \<turnstile> N \<leadsto>\<^sup>*\<^bsub>T[M' / x]\<^esub>\<^bsup>\<sigma>\<^esup> N' \<Longrightarrow> \<Gamma> \<turnstile> (M, N)\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> \<leadsto>\<^sup>*\<^bsub>(x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T\<^esub>\<^bsup>\<sigma>\<^esup> (M', N')\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub>\<close>
    | nf_Unit: \<open>\<Gamma> \<turnstile> \<star> \<leadsto>\<^sup>*\<^bsub>I\<^esub>\<^bsup>\<sigma>\<^esup> \<star>\<close>
    | nf_Fst: \<open>\<Gamma> \<turnstile> M \<leadsto>\<^sup>*\<^bsub>(x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T\<^esub>\<^bsup>\<sigma>\<^esup> M' \<Longrightarrow> \<Gamma> \<turnstile> fst\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> (M, N)\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> \<leadsto>\<^sup>*\<^bsub>S\<^esub>\<^bsup>0\<^esup> M'\<close>
    | nf_Fst': \<open>\<Gamma> \<turnstile> M \<leadsto>\<^sup>*\<^bsub>S\<^esub>\<^bsup>0\<^esup> M' \<Longrightarrow> \<Gamma> \<turnstile> fst\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> M' \<leadsto>\<^sup>*\<^bsub>S\<^esub>\<^bsup>0\<^esup> N \<Longrightarrow> \<Gamma> \<turnstile> fst\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> M \<leadsto>\<^sup>*\<^bsub>S\<^esub>\<^bsup>0\<^esup> N\<close>
    | nf_Snd: \<open>\<Gamma> \<turnstile> N \<leadsto>\<^sup>*\<^bsub>T[M / x]\<^esub>\<^bsup>0\<^esup> N' \<Longrightarrow> \<Gamma> \<turnstile> snd\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> (M, N)\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> \<leadsto>\<^sup>*\<^bsub>T[M / x]\<^esub>\<^bsup>0\<^esup> N'\<close>
    | nf_Snd': \<open>(\<Gamma>, x \<Ztypecolon>\<^bsup>0\<^esup> S) \<turnstile> N \<leadsto>\<^sup>*\<^bsub>T[Var x / x]\<^esub>\<^bsup>0\<^esup> N' \<Longrightarrow> \<Gamma> \<turnstile> snd\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> N' \<leadsto>\<^sup>*\<^bsub>T[Var x / x]\<^esub>\<^bsup>0\<^esup> M \<Longrightarrow> \<Gamma> \<turnstile> snd\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> N \<leadsto>\<^sup>*\<^bsub>T[Var x / x]\<^esub>\<^bsup>0\<^esup> M\<close>
    | nf_LetPair: \<open>\<Gamma> \<turnstile> P[M / a][N / b] \<leadsto>\<^sup>*\<^bsub>U\<^esub>\<^bsup>\<sigma>\<^esup> P' \<Longrightarrow> \<Gamma> \<turnstile> let\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> (a, b)\<^bsub>(z)\<^esub> = (M, N)\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> in P \<leadsto>\<^sup>*\<^bsub>U\<^esub>\<^bsup>\<sigma>\<^esup> P'\<close>
    | nf_LetPair': \<open>\<Gamma> \<turnstile> M \<leadsto>\<^sup>*\<^bsub>(x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T\<^esub>\<^bsup>\<sigma>\<^esup> M' \<Longrightarrow> \<Gamma> \<turnstile> let\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> (a, b)\<^bsub>(z)\<^esub> = M' in N \<leadsto>\<^sup>*\<^bsub>U\<^esub>\<^bsup>\<sigma>\<^esup> N' \<Longrightarrow> \<Gamma> \<turnstile> let\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> (a, b)\<^bsub>(z)\<^esub> = M in N \<leadsto>\<^sup>*\<^bsub>U\<^esub>\<^bsup>\<sigma>\<^esup> N'\<close>
    | nf_LetUnit: \<open>\<Gamma> \<turnstile> M \<leadsto>\<^sup>*\<^bsub>U\<^esub>\<^bsup>\<sigma>\<^esup> M' \<Longrightarrow> \<Gamma> \<turnstile> let\<^sub>I \<star>\<^bsub>(z)\<^esub> = \<star> in M \<leadsto>\<^sup>*\<^bsub>U\<^esub>\<^bsup>\<sigma>\<^esup> M'\<close>
    | nf_LetUnit': \<open>\<Gamma> \<turnstile> M \<leadsto>\<^sup>*\<^bsub>I\<^esub>\<^bsup>\<sigma>\<^esup> M' \<Longrightarrow> \<Gamma> \<turnstile> let\<^sub>I \<star>\<^bsub>(z)\<^esub> = M' in N \<leadsto>\<^sup>*\<^bsub>U\<^esub>\<^bsup>\<sigma>\<^esup> N' \<Longrightarrow> \<Gamma> \<turnstile> let\<^sub>I \<star>\<^bsub>(z)\<^esub> = M in N \<leadsto>\<^sup>*\<^bsub>U\<^esub>\<^bsup>\<sigma>\<^esup> N'\<close>
    | nf_True: \<open>\<Gamma> \<turnstile> true \<leadsto>\<^sup>*\<^bsub>Bool\<^esub>\<^bsup>\<sigma>\<^esup> true\<close>
    | nf_False: \<open>\<Gamma> \<turnstile> false \<leadsto>\<^sup>*\<^bsub>Bool\<^esub>\<^bsup>\<sigma>\<^esup> false\<close>
    | nf_ElimBoolTrue: \<open>\<Gamma> \<turnstile> M\<^sub>t \<leadsto>\<^sup>*\<^bsub>T[true / z]\<^esub>\<^bsup>\<sigma>\<^esup> M\<^sub>t' \<Longrightarrow> \<Gamma> \<turnstile> ElimBool\<^bsub>(z) T\<^esub>(M\<^sub>t, M\<^sub>f, true) \<leadsto>\<^sup>*\<^bsub>T[true / z]\<^esub>\<^bsup>\<sigma>\<^esup> M\<^sub>t'\<close>
    | nf_ElimBoolFalse: \<open>\<Gamma> \<turnstile> M\<^sub>f \<leadsto>\<^sup>*\<^bsub>T[false / z]\<^esub>\<^bsup>\<sigma>\<^esup> M\<^sub>f' \<Longrightarrow> \<Gamma> \<turnstile> ElimBool\<^bsub>(z) T\<^esub>(M\<^sub>t, M\<^sub>f, false) \<leadsto>\<^sup>*\<^bsub>T[false / z]\<^esub>\<^bsup>\<sigma>\<^esup> M\<^sub>f'\<close>
    | nf_ElimBool: \<open>\<Gamma> \<turnstile> N \<leadsto>\<^sup>*\<^bsub>Bool\<^esub>\<^bsup>\<sigma>\<^esup> N' \<Longrightarrow> \<Gamma> \<turnstile> ElimBool\<^bsub>(z) T\<^esub>(M\<^sub>t, M\<^sub>f, N') \<leadsto>\<^sup>*\<^bsub>T\<^esub>\<^bsup>\<sigma>\<^esup> N'' \<Longrightarrow> \<Gamma> \<turnstile> ElimBool\<^bsub>(z) T\<^esub>(M\<^sub>t, M\<^sub>f, N) \<leadsto>\<^sup>*\<^bsub>T\<^esub>\<^bsup>\<sigma>\<^esup> N''\<close>
    | nf_Pi: \<open>\<Gamma> \<turnstile> S \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> S' \<Longrightarrow> (\<Gamma>, x \<Ztypecolon>\<^bsup>\<pi>\<^esup> Set) \<turnstile> T \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> T' \<Longrightarrow> \<Gamma> \<turnstile> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<rightarrow> T \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S') \<rightarrow> T'\<close>
    | nf_Sigma: \<open>\<Gamma> \<turnstile> S \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> S' \<Longrightarrow> (\<Gamma>, x \<Ztypecolon>\<^bsup>\<pi>\<^esup> Set) \<turnstile> T \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> T' \<Longrightarrow> \<Gamma> \<turnstile> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S') \<otimes> T'\<close>
    | nf_I: \<open>\<Gamma> \<turnstile> I \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> I\<close>
    | nf_Bool: \<open>\<Gamma> \<turnstile> Bool \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> Bool\<close>
    | nf_El: \<open>\<Gamma> \<turnstile> M \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> M' \<Longrightarrow> \<Gamma> \<turnstile> El M \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> El M'\<close>
    | nf_Set: \<open>\<Gamma> \<turnstile> Set \<leadsto>\<^sup>*\<^bsub>Set\<^esub>\<^bsup>0\<^esup> Set\<close>

definition normalize :: \<open>('v, 'm :: resource_semiring) precontext \<Rightarrow> ('v, 'm) preterm \<Rightarrow> 'm \<Rightarrow> ('v, 'm) preterm \<Rightarrow> ('v, 'm) preterm\<close>
                        (\<open>_/ \<Down>\<^bsub>_\<^esub>\<^bsup>_\<^esup>/ _\<close> [30, 20, 20, 30] 30)
where \<open>\<Gamma> \<Down>\<^bsub>T\<^esub>\<^bsup>\<sigma>\<^esup> M \<equiv> (THE N. \<Gamma> \<turnstile> M \<leadsto>\<^sup>*\<^bsub>T\<^esub>\<^bsup>\<sigma>\<^esup> N)\<close>

definition eq_preterm :: \<open>('v, 'm :: resource_semiring) precontext \<Rightarrow> ('v, 'm) preterm \<Rightarrow> ('v, 'm) preterm \<Rightarrow> 'm \<Rightarrow> ('v, 'm) preterm \<Rightarrow> bool\<close>
                         (\<open>_/ \<turnstile>/ _/ \<equiv>/ _/ \<Ztypecolon>\<^bsup>_\<^esup>/ _\<close> [20, 15, 15, 15, 20] 20)
where \<open>(\<Gamma> \<turnstile> M \<equiv> N \<Ztypecolon>\<^bsup>\<sigma>\<^esup> T) \<equiv> (\<Gamma> \<Down>\<^bsub>T\<^esub>\<^bsup>\<sigma>\<^esup> M) = (\<Gamma> \<Down>\<^bsub>T\<^esub>\<^bsup>\<sigma>\<^esup> N)\<close>

no_syntax
  "_list" :: "args => 'a list" ("[(_)]")
  (* Remove this syntax because it conflicts with our substitution syntax.
   * It should not really be useful anyway since we don't plan on using lists. *)

inductive wf_pretype :: \<open>('v, 'm :: resource_semiring) precontext \<Rightarrow> ('v, 'm) preterm \<Rightarrow> bool\<close>
                        (\<open>_/ \<turnstile>/ _/ wftype\<close> [15, 14] 15)
      and wf_precontext :: \<open>('v, 'm :: resource_semiring) precontext \<Rightarrow> bool\<close>
                           (\<open>_/ \<turnstile>/ wfctx\<close> [15] 15)
      and typecheck :: \<open>('v, 'm :: resource_semiring) precontext \<Rightarrow> ('v, 'm) preterm \<Rightarrow> 'm \<Rightarrow> ('v, 'm) preterm \<Rightarrow> bool\<close>
                       (\<open>_/ \<turnstile>/ _/ \<Ztypecolon>\<^bsup>_\<^esup>/ _\<close> [15, 14, 20, 15] 15)
where (* Precontext wellformedness *)
      wf_Empty: \<open>\<diamond> \<turnstile> wfctx\<close>
    | wf_Cons: \<open>\<Gamma> \<turnstile> wfctx \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> S wftype \<Longrightarrow> (\<Gamma>, x \<Ztypecolon>\<^bsup>\<rho>\<^esup> S) \<turnstile> wfctx\<close>

      (* Pretypes wellformedness *)
    | wf_Pi: \<open>0 \<cdot> \<Gamma> \<turnstile> S wftype \<Longrightarrow> ((0 \<cdot> \<Gamma>), x \<Ztypecolon>\<^bsup>0\<^esup> S) \<turnstile> T wftype \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<rightarrow> T wftype\<close>
    | wf_Sigma: \<open>0 \<cdot> \<Gamma> \<turnstile> S wftype \<Longrightarrow> ((0 \<cdot> \<Gamma>), x \<Ztypecolon>\<^bsup>0\<^esup> S) \<turnstile> T wftype \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T wftype\<close>
    | wf_I: \<open>0 \<cdot> \<Gamma> \<turnstile> wfctx \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> I wftype\<close>
    | wf_Set: \<open>0 \<cdot> \<Gamma> \<turnstile> wfctx \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> Set wftype\<close>
    | wf_Bool: \<open>0 \<cdot> \<Gamma> \<turnstile> wfctx \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> Bool wftype\<close>
    | wf_El: \<open>0 \<cdot> \<Gamma> \<turnstile> M \<Ztypecolon>\<^bsup>0\<^esup> Set \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> El M wftype\<close>

      (* Type-checking *)
    | tc_Var: \<open>(0 \<cdot> \<Gamma>\<^sub>1) @ x \<Ztypecolon>\<^bsup>\<rho>\<^esup> S @ (0 \<cdot> \<Gamma>\<^sub>2) \<turnstile> wfctx \<Longrightarrow> (0 \<cdot> \<Gamma>\<^sub>1) @ x \<Ztypecolon>\<^bsup>\<rho>\<^esup> S @ (0 \<cdot> \<Gamma>\<^sub>2) \<turnstile> Var x \<Ztypecolon>\<^bsup>\<rho>\<^esup> S\<close>
    | tc_Conv: \<open>\<Gamma> \<turnstile> M \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> S \<equiv> T \<Ztypecolon>\<^bsup>0\<^esup> Set \<Longrightarrow> \<Gamma> \<turnstile> M \<Ztypecolon>\<^bsup>\<sigma>\<^esup> T\<close>
    | tc_Lambda: \<open>(\<Gamma>, x \<Ztypecolon>\<^bsup>\<sigma> * \<pi> \<^esup>S) \<turnstile> M \<Ztypecolon>\<^bsup>\<sigma>\<^esup> T \<Longrightarrow> \<Gamma> \<turnstile> \<lambda> x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. M\<^bsup>T\<^esup> \<Ztypecolon>\<^bsup>\<sigma>\<^esup> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<rightarrow> T\<close>
    | tc_App: \<open>\<Gamma>\<^sub>1 \<turnstile> M \<Ztypecolon>\<^bsup>\<sigma>\<^esup> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<rightarrow> T \<Longrightarrow> \<Gamma>\<^sub>2 \<turnstile> N \<Ztypecolon>\<^bsup>\<sigma>'\<^esup> S \<Longrightarrow> 0 \<cdot> \<Gamma>\<^sub>1 = 0 \<cdot> \<Gamma>\<^sub>2 \<Longrightarrow>
                     (\<sigma>' = 0 \<longleftrightarrow> \<pi> = 0 \<or> \<sigma> = 0) \<Longrightarrow> (\<Gamma>\<^sub>1 + (\<pi> \<cdot> \<Gamma>\<^sub>2)) \<turnstile> App\<^bsub>(x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) T\<^esub>(M, N) \<Ztypecolon>\<^bsup>\<sigma>\<^esup> T[N / x]\<close>
    | tc_Pair: \<open>\<Gamma>\<^sub>1 \<turnstile> M \<Ztypecolon>\<^bsup>\<sigma>'\<^esup> S \<Longrightarrow> 0 \<cdot> \<Gamma>\<^sub>1 = 0 \<cdot> \<Gamma>\<^sub>2 \<Longrightarrow> \<Gamma>\<^sub>2 \<turnstile> N \<Ztypecolon>\<^bsup>\<sigma>\<^esup> T[M / x] \<Longrightarrow> (\<sigma>' = 0 \<longleftrightarrow> \<pi> = 0 \<or> \<sigma> = 0) \<Longrightarrow>
                          (\<pi> \<cdot> \<Gamma>\<^sub>1 + \<Gamma>\<^sub>2) \<turnstile> (M, N)\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> \<Ztypecolon>\<^bsup>\<sigma>\<^esup> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T\<close>
    | tc_Unit: \<open>0 \<cdot> \<Gamma> \<turnstile> wfctx \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> \<star> \<Ztypecolon>\<^bsup>\<sigma>\<^esup> I\<close>
    | tc_Fst: \<open>\<Gamma> \<turnstile> M \<Ztypecolon>\<^bsup>0\<^esup> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T \<Longrightarrow> \<Gamma> \<turnstile> fst\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> M \<Ztypecolon>\<^bsup>0\<^esup> S\<close>
    | tc_Snd: \<open>\<Gamma> \<turnstile> M \<Ztypecolon>\<^bsup>0\<^esup> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T \<Longrightarrow> \<Gamma> \<turnstile> snd\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> M \<Ztypecolon>\<^bsup>0\<^esup> T[fst\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> M / x]\<close>
    | tc_LetPair: \<open>((0 \<cdot> \<Gamma>\<^sub>1), z \<Ztypecolon>\<^bsup>0\<^esup> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T) \<turnstile> U wftype \<Longrightarrow> \<Gamma>\<^sub>1 \<turnstile> M \<Ztypecolon>\<^bsup>\<sigma>\<^esup> (x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S) \<otimes> T \<Longrightarrow>
                          ((\<Gamma>\<^sub>2, x \<Ztypecolon>\<^bsup>\<sigma> * \<pi>\<^esup> S), y \<Ztypecolon>\<^bsup>\<sigma>\<^esup> T) \<turnstile> N \<Ztypecolon>\<^bsup>\<sigma>\<^esup> U[(Var x, Var y)\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> / z] \<Longrightarrow> 0 \<cdot> \<Gamma>\<^sub>1 = 0 \<cdot> \<Gamma>\<^sub>2 \<Longrightarrow>
                          \<Gamma>\<^sub>1 + \<Gamma>\<^sub>2 \<turnstile> let\<^bsub>x \<Ztypecolon>\<^bsup>\<pi>\<^esup> S. T\<^esub> (x, y)\<^bsub>(z)\<^esub> = M in N \<Ztypecolon>\<^bsup>\<sigma>\<^esup> U[M / z]\<close>
    | tc_LetUnit: \<open>((0 \<cdot> \<Gamma>\<^sub>1), z \<Ztypecolon>\<^bsup>0\<^esup> I) \<turnstile> U wftype \<Longrightarrow> \<Gamma>\<^sub>1 \<turnstile> M \<Ztypecolon>\<^bsup>\<sigma>\<^esup> I \<Longrightarrow> \<Gamma>\<^sub>2 \<turnstile> N \<Ztypecolon>\<^bsup>\<sigma>\<^esup> U[\<star> / x] \<Longrightarrow> 0 \<cdot> \<Gamma>\<^sub>1 = 0 \<cdot> \<Gamma>\<^sub>2 \<Longrightarrow>
                         \<Gamma>\<^sub>1 + \<Gamma>\<^sub>2 \<turnstile> let\<^sub>I \<star>\<^bsub>(z)\<^esub> = M in N \<Ztypecolon>\<^bsup>\<sigma>\<^esup> U[M / x]\<close>
    | tc_False: \<open>0 \<cdot> \<Gamma> \<turnstile> wfctx \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> false \<Ztypecolon>\<^bsup>\<sigma>\<^esup> Bool\<close>
    | tc_True: \<open>0 \<cdot> \<Gamma> \<turnstile> wfctx \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> true \<Ztypecolon>\<^bsup>\<sigma>\<^esup> Bool\<close>
    | tc_ElimBool: \<open>((0 \<cdot> \<Gamma>\<^sub>1), z \<Ztypecolon>\<^bsup>0\<^esup> Bool) \<turnstile> T wftype \<Longrightarrow> \<Gamma>\<^sub>1 \<turnstile> M\<^sub>t \<Ztypecolon>\<^bsup>\<sigma>\<^esup> T[true / z] \<Longrightarrow> \<Gamma>\<^sub>1 \<turnstile> M\<^sub>f \<Ztypecolon>\<^bsup>\<sigma>\<^esup> T[false / z] \<Longrightarrow> \<Gamma>\<^sub>2 \<turnstile> N \<Ztypecolon>\<^bsup>\<sigma>\<^esup> Bool \<Longrightarrow>
                         0 \<cdot> \<Gamma>\<^sub>1 = 0 \<cdot> \<Gamma>\<^sub>2 \<Longrightarrow> \<Gamma>\<^sub>1 + \<Gamma>\<^sub>2 \<turnstile> ElimBool\<^bsub>(z) T \<^esub>(M\<^sub>t, M\<^sub>f, N) \<Ztypecolon>\<^bsup>\<sigma>\<^esup> T[N / z]\<close>
    | tc_pretype: \<open>0 \<cdot> \<Gamma> \<turnstile> T wftype \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> T \<Ztypecolon>\<^bsup>0\<^esup> Set\<close>
          \<comment>\<open>This rule replaces the "introductory rules" for pretypes (mentioned in the paragraph for \<open>El\<close>).\<close>

lemmas wf_pretype_induct = wf_pretype_wf_precontext_typecheck.inducts(1)
   and wf_precontext_induct = wf_pretype_wf_precontext_typecheck.inducts(2)
   and typecheck_induct = wf_pretype_wf_precontext_typecheck.inducts(3)

lemma usage_irrelevant_to_wfctx: \<open>\<Gamma>\<^sub>1 \<turnstile> wfctx \<Longrightarrow> 0 \<cdot> \<Gamma>\<^sub>1 = 0 \<cdot> \<Gamma>\<^sub>2 \<Longrightarrow> \<Gamma>\<^sub>2 \<turnstile> wfctx\<close>
proof (induct \<Gamma>\<^sub>1 arbitrary: \<Gamma>\<^sub>2)
  case Empty
  then show ?case
    using add_precontext.cases add_precontext_output_unique
    by blast
next
  case (Cons \<Gamma>\<^sub>1' x \<rho> A \<Gamma>\<^sub>2)
  then obtain \<Gamma>\<^sub>2' and \<pi> where \<Gamma>\<^sub>2_is: \<open>\<Gamma>\<^sub>2 = (\<Gamma>\<^sub>2', x \<Ztypecolon>\<^bsup>\<pi>\<^esup> A)\<close>
                          and \<open>0 \<cdot> (\<Gamma>\<^sub>1', x \<Ztypecolon>\<^bsup>\<rho>\<^esup> A) = 0 \<cdot> \<Gamma>\<^sub>2\<close>
    by (smt (verit, best) precontext.inject scale.elims)
  then have \<open>\<Gamma>\<^sub>2' \<turnstile> wfctx\<close>
    using Cons.hyps Cons.prems(1) wf_precontext.cases
    by auto
  then show ?case
    by (metis Cons.prems(1) Cons.prems(2) \<Gamma>\<^sub>2_is precontext.distinct(1) precontext.inject scale.simps(2) wf_Cons wf_precontext.cases)
qed

lemma tm_zero_admissible: \<open>\<Gamma> \<turnstile> M \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> M \<Ztypecolon>\<^bsup>0\<^esup> S\<close>
  (* Here's a quick problem: we have unresolved schematic variables. *)
proof (induct rule: typecheck_induct)
  oops

lemma tm_eq_zero_admissible: \<open>\<Gamma> \<turnstile> M \<equiv> N \<Ztypecolon>\<^bsup>\<sigma>\<^esup> S \<Longrightarrow> 0 \<cdot> \<Gamma> \<turnstile> M \<equiv> N \<Ztypecolon>\<^bsup>0\<^esup> S\<close>
  oops

lemma zeroing_entails_all_zero: \<open>(\<forall> (_, \<rho>, _) \<in> to_set \<Gamma>. \<rho> = 0) \<Longrightarrow> 0 \<cdot> \<Gamma> = \<Gamma>\<close>
  by (induct rule: to_set.induct, auto simp add: times_zero_left)

lemma zero_needs_nothing: \<open>\<Gamma> \<turnstile> M \<Ztypecolon>\<^bsup>0\<^esup> S \<Longrightarrow> 0 \<cdot> \<Gamma> = \<Gamma>\<close>
proof (induct rule: typecheck_induct)
  oops

end (* theory QTT *)