blob: d22e71065f874a0401e6e19dc53f6dd65948b380 (
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
|
theory test
imports HoTT
begin
text \<open>Check trivial stuff:\<close>
lemma "Null : U"
by (rule Null_form)
text \<open>
Do functions behave like we expect them to?
(Or, is my implementation at least somewhat correct?...
\<close>
lemma "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A"
proof -
have "A \<equiv> B \<Longrightarrow> B \<equiv> A" by (rule DefEq_symmetry)
then have "\<And>x. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types)
thus "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. 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
|
