blob: 3ee973c9fb0a3dab291d5d00ba351f709c5e4ef6 (
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
|
(*
Title: ex/Synthesis.thy
Author: Joshua Chen
Date: 2018
Examples of synthesis
*)
theory Synthesis
imports "../HoTT"
begin
section ‹Synthesis of the predecessor function›
text ‹
In this example we construct a predecessor function for the natural numbers.
This is also done in @{file "~~/src/CTT/ex/Synthesis.thy"}, there the work is much easier as the equality type is extensional.
›
text ‹First we show that the property we want is well-defined.›
lemma pred_welltyped: "∑pred: ℕ→ℕ. (pred`0 =⇩ℕ 0) × (∏n:ℕ. pred`(succ n) =⇩ℕ n): U O"
by routine
text ‹
Now we look for an inhabitant of this type.
Observe that we're looking for a lambda term @{term pred} satisfying @{term "pred`0 =⇩ℕ 0"} and @{term "∏n:ℕ. pred`(succ n) =⇩ℕ n"}.
What if we require *definitional* instead of just propositional equality?
›
schematic_goal "?p`0 ≡ 0" and "⋀n. n: ℕ ⟹ (?p`(succ n)) ≡ n"
apply compute
prefer 4 apply compute
apply (rule Nat_routine | compute)+
oops
― ‹Something in the original proof broke when I revamped the theory. The completion of this derivation is left as an exercise to the reader.›
text ‹
The above proof finds a candidate, namely @{term "λn. ind⇩ℕ (λa b. a) 0 n"}.
We prove this has the required type and properties.
›
definition pred :: t where "pred ≡ ❙λn. ind⇩ℕ (λa b. a) 0 n"
lemma pred_type: "pred: ℕ → ℕ"
unfolding pred_def by routine
lemma pred_props: "<refl 0, ❙λn. refl n>: (pred`0 =⇩ℕ 0) × (∏n:ℕ. pred`(succ n) =⇩ℕ n)"
unfolding pred_def by derive
theorem "<pred, <refl(0), ❙λn. refl(n)>>: ∑pred:ℕ→ℕ . ((pred`0) =⇩ℕ 0) × (∏n:ℕ. (pred`(succ n)) =⇩ℕ n)"
by (derive lems: pred_type pred_props)
end
|
