blob: b37ac76d5ec5e54c8ea83cf90b2afb5b0cc077cc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
theory HoTT_Test
imports HoTT
begin
text \<open>Check trivial stuff:\<close>
lemma "Null : U"
by (rule Null_form)
lemma "\<lbrakk>A \<equiv> B; x : B\<rbrakk> \<Longrightarrow> x : A"
proof -
assume "A \<equiv> B"
then have "B \<equiv> A" by (rule Pure.symmetric)
then have "x : B \<Longrightarrow> x :A" by (rule equal_types)
oops
(* qed---figure out how to discharge assumptions *)
text \<open>
Do functions behave like we expect them to?
(Or, is my implementation at least somewhat correct?...
\<close>
\<comment> {* NOTE!!! The issues with substitution here.
We need the HoTT term \<open>b\<close> and the type family \<open>B\<close> to indeed be a Pure \<lambda>-term!
This seems to mean that I have to implement the HoTT types in more than one Pure type.
See CTT.thy for examples.
*}
lemma "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x:A. x) : B\<rightarrow>A"
proof -
have "A \<equiv> B \<Longrightarrow> B \<equiv> A" by (rule Pure.symmetric)
then have "\<And>x::Term. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types)
thus "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x:A. x) : B\<rightarrow>A" by (rule Function_intro)
qed
lemma "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A"
proof -
have "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. x : B \<rightarrow> A" by (rule Function_intro)
thus "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A" by (rule Function_intro)
qed
text \<open>Here's a dumb proof that 2 is a natural number:\<close>
lemma "succ(succ 0) : Nat"
proof -
have "0 : Nat" by (rule Nat_intro1)
from this have "(succ 0) : Nat" by (rule Nat_intro2)
thus "succ(succ 0) : Nat" by (rule Nat_intro2)
qed
text \<open>
We can of course iterate the above for as many applications of \<open>succ\<close> as we like.
The next thing to do is to implement some kind of induction tactic to automate such proofs.
When we get more stuff working, I'd like to aim for formalizing the encode-decode method.
\<close>
end
|
