(*  Title:  HoTT/HoTT_Test.thy
    Author: Josh Chen
    Date:   Aug 2018

This is an old "test suite" from early implementations of the theory.
It is not always guaranteed to be up to date, or reflect most recent versions of the theory.
*)

theory HoTT_Test
  imports HoTT
begin


text "
  A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
  
  Things that *should* be automated:
    - Checking that \<open>A\<close> is a well-formed type, when writing things like \<open>x : A\<close> and \<open>A : U\<close>.
    - Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
"

declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]]
  \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>


section \<open>\<Pi>-type\<close>

subsection \<open>Typing functions\<close>

text "
  Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following.
"

proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" using assms ..

proposition
  assumes "A : U(i)" and "A \<equiv> B"
  shows "\<^bold>\<lambda>x. x : B \<rightarrow> A"
proof -
  have "A\<rightarrow>A \<equiv> B\<rightarrow>A" using assms by simp
  moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" using assms(1) ..
  ultimately show "\<^bold>\<lambda>x. x : B \<rightarrow> A" by simp
qed

proposition
  assumes "A : U(i)" and "B : U(i)"
  shows "\<^bold>\<lambda>x y. x : A \<rightarrow> B \<rightarrow> A"
by (simple lems: assms)


subsection \<open>Function application\<close>

proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" by (simple lems: assms)

text "Currying:"

lemma
  assumes "a : A" and "\<And>x. x: A \<Longrightarrow> B(x): U(i)"
  shows "(\<^bold>\<lambda>x y. y)`a \<equiv> \<^bold>\<lambda>y. y"
proof
  show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. y : B(x) \<rightarrow> B(x)" by (simple lems: assms)
qed fact

lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b" by (compute, simple)

lemma "\<lbrakk>A: U(i); a : A \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. f x y)`a \<equiv> \<^bold>\<lambda>y. f a y"
proof compute
  show "\<And>x. \<lbrakk>A: U(i); x: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>y. f x y: \<Prod>y:B(x). C x y"
  proof
    oops

lemma "\<lbrakk>a : A; b : B(a); c : C(a)(b)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. \<^bold>\<lambda>y. \<^bold>\<lambda>z. f x y z)`a`b`c \<equiv> f a b c"
  oops


subsection \<open>Currying functions\<close>

proposition curried_function_formation:
  fixes A B C
  assumes
    "A : U(i)" and
    "B: A \<longrightarrow> U(i)" and
    "\<And>x. C(x): B(x) \<longrightarrow> U(i)"
  shows "\<Prod>x:A. \<Prod>y:B(x). C x y : U(i)"
  by (simple lems: assms)


proposition higher_order_currying_formation:
  assumes
    "A: U(i)" and
    "B: A \<longrightarrow> U(i)" and
    "\<And>x y. y: B(x) \<Longrightarrow> C(x)(y): U(i)" and
    "\<And>x y z. z : C(x)(y) \<Longrightarrow> D(x)(y)(z): U(i)"
  shows "\<Prod>x:A. \<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z): U(i)"
  by (simple lems: assms)


lemma curried_type_judgment:
  assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "\<And>x y. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y"
  shows "\<^bold>\<lambda>x y. f x y : \<Prod>x:A. \<Prod>y:B(x). C x y"
  by (simple lems: assms)


text "
  Polymorphic identity function. Trivial due to lambda expression polymorphism.
  (Was more involved in previous monomorphic incarnations.)
"

definition Id :: "Term" where "Id \<equiv> \<^bold>\<lambda>x. x"

lemma "\<lbrakk>x: A\<rbrakk> \<Longrightarrow> Id`x \<equiv> x"
unfolding Id_def by (compute, simple)
  

section \<open>Natural numbers\<close>

text "Automatic proof methods recognize natural numbers."

proposition "succ(succ(succ 0)): Nat" by simple

end