diff options
author | Josh Chen | 2018-08-15 11:47:30 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-15 11:47:30 +0200 |
commit | f4f468878fc0459a806b02cdf8921af6fcac2759 (patch) | |
tree | 5f646632b36c97cc783fe3209d7df1e4b47d59b0 /ex/HoTT Book | |
parent | e94784953a751b0720689b686e607c95ba0f0592 (diff) |
Tweak proof methods, some type rules; add HoTT Book examples
Diffstat (limited to 'ex/HoTT Book')
-rw-r--r-- | ex/HoTT Book/Ch1.thy | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/ex/HoTT Book/Ch1.thy b/ex/HoTT Book/Ch1.thy new file mode 100644 index 0000000..84a5cf4 --- /dev/null +++ b/ex/HoTT Book/Ch1.thy @@ -0,0 +1,37 @@ +theory Ch1 + imports "../../HoTT" +begin + +chapter \<open>HoTT Book, Chapter 1\<close> + +section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close> + +text "Prove that the only inhabitants of the \<Sigma>-type are those given by the pair constructor." + +schematic_goal + assumes "(\<Sum>x:A. B(x)): U(i)" and "p: \<Sum>x:A. B(x)" + shows "?a: p =[\<Sum>x:A. B(x)] <fst p, snd p>" + +text "Proof by induction on \<open>p: \<Sum>x:A. B(x)\<close>:" + +proof (rule Sum_elim[where ?p=p]) + text "We just need to prove the base case; the rest will be taken care of automatically." + + fix x y assume asm: "x: A" "y: B(x)" show + "refl(<x,y>): <x,y> =[\<Sum>x:A. B(x)] <fst <x,y>, snd <x,y>>" + proof (subst (0 1) comp) + text " + The computation rules for \<open>fst\<close> and \<open>snd\<close> require that \<open>x\<close> and \<open>y\<close> have appropriate types. + The automatic proof methods have trouble picking the appropriate types, so we state them explicitly, + " + show "x: A" and "y: B(x)" by (fact asm)+ + + text "...twice, once each for the substitutions of \<open>fst\<close> and \<open>snd\<close>." + show "x: A" and "y: B(x)" by (fact asm)+ + + qed (derive lems: assms asm) + +qed (derive lems: assms) + + +end
\ No newline at end of file |