Mario Carneiro (Aug 22 2024 at 16:22): Mario Carneiro (Aug 22 2024 at 16:22):While playing around with exports, I came up with this, which is a list of the most commonly reproved theorems (in the sense that independent calls to the kernel to unconstrain a thm with this statement are made), during evaluation of the HOL session. Possibly this could be used to reduce the build cost by storing and reusing these theorems instead of proving them repeatedly.
1411 (:000 + 1 \<le> :000) = (0 * :000 + 1 \<le> 0)
1411 :000 + 1 \<le> :000 \<equiv> 1 \<le> 0
1411 (:000 + 1 \<le> :000) = (Numeral1 * :000 + 1 \<le> Numeral1 * :000 + 0)
1343 (:001 + 1 \<le> :001) = (0 * :001 + 1 \<le> 0)
1343 :001 + 1 \<le> :001 \<equiv> 1 \<le> 0
1343 (:001 + 1 \<le> :001) = (Numeral1 * :001 + 1 \<le> Numeral1 * :001 + 0)
900 False \<Longrightarrow> False
900 \<not> True \<Longrightarrow> False
750 \<lbrakk>OFCLASS(?'a, type_class); PROP ?P1.0 =simp=> ?x \<equiv> ?y\<rbrakk> \<Longrightarrow> PROP ?P1.0 =simp=> ?x = ?y
750 \<lbrakk>OFCLASS(?'a, type_class); PROP P1 =simp=> x \<equiv> y\<rbrakk> \<Longrightarrow> PROP P1 =simp=> x = y
659 OFCLASS(?'a, type_class) \<Longrightarrow> ?a1 = ?b1 \<equiv> ?b1 = ?a1
656 Suc n \<le> n \<equiv> Suc 0 \<le> 0
599 y + 1 \<le> y \<equiv> 0 + 1 \<le> 0
500 OFCLASS(?'a, type_class) \<Longrightarrow> ?x1 = ?x1
487 (Suc n \<le> n) = (0 * n + Numeral1 \<le> 0)
487 Suc n \<le> n \<equiv> False
487 (Suc n \<le> n) = (Numeral1 * n + Numeral1 \<le> Numeral1 * n + 0)
480 x + 1 \<le> x \<equiv> 0 + 1 \<le> 0
386 Suc m \<le> m \<equiv> Suc 0 \<le> 0
318 (Suc :000 \<le> :000) = (0 * :000 + Numeral1 \<le> 0)
318 Suc :000 \<le> :000 \<equiv> False
318 (Suc :000 \<le> :000) = (Numeral1 * :000 + Numeral1 \<le> Numeral1 * :000 + 0)
304 OFCLASS(?'a, type_class) \<Longrightarrow> ?a1 \<in> Collect ?P1 \<equiv> ?P1 ?a1
302 \<lbrakk>OFCLASS(?'a, type_class); OFCLASS(?'b, type_class); OFCLASS(?'c, type_class)\<rbrakk> \<Longrightarrow> case (?a1, ?b1) of (c, d) \<Rightarrow> ?f1 c d \<equiv> ?f1 ?a1 ?b1
287 (Suc a__ \<le> a__) = (0 * a__ + Numeral1 \<le> 0)
287 Suc a__ \<le> a__ \<equiv> False
287 (Suc a__ \<le> a__) = (Numeral1 * a__ + Numeral1 \<le> Numeral1 * a__ + 0)
264 2 = 2
252 (a + :000 < :000 + a) = (0 * a + :000 < :000 + 0)
252 a + :000 < :000 + a \<equiv> :000 < :000
252 (a + :000 < :000 + a) = (Numeral1 * a + :000 < Numeral1 * a + :000)
251 (b + :000 < a + b) = (0 * b + :000 < a + 0)
251 b + :000 < a + b \<equiv> :000 < a
251 (b + :000 < a + b) = (Numeral1 * b + :000 < Numeral1 * b + a)
231 ?x \<equiv> ()
220 \<And>dummy. PROP dummy \<Longrightarrow> PROP dummy
217 \<lbrakk>t1; \<not> t1 \<or> t2\<rbrakk> \<Longrightarrow> t2
217 Suc (:000 + n) \<le> n + :000 \<equiv> Suc n \<le> n
202 (Suc (:000 + n) \<le> n + :000) = (0 * :000 + (Numeral1 + n) \<le> n + 0)
202 (Suc (:000 + n) \<le> n + :000) = (Numeral1 * :000 + (Numeral1 + n) \<le> Numeral1 * :000 + n)
192 Suc n__ \<le> n__ \<equiv> Suc 0 \<le> 0
189 m \<le> n \<Longrightarrow> n \<le> m \<equiv> n = m
177 (2 + :000 \<le> :000) = (0 * :000 + 2 \<le> 0)
177 (2 + :000 \<le> :000) = (Numeral1 * :000 + 2 \<le> Numeral1 * :000 + 0)
161 Suc (m + n) \<le> n + m \<equiv> Suc n \<le> n
160 (=) \<le> (=)
142 1 * 2 = 2
139 (:000 + 1 \<le> :001 + :000) = (0 * :000 + 1 \<le> :001 + 0)
139 :000 + 1 \<le> :001 + :000 \<equiv> 1 \<le> :001
139 (:000 + 1 \<le> :001 + :000) = (Numeral1 * :000 + 1 \<le> Numeral1 * :000 + :001)
139 (:001 + 1 \<le> :000 + :001) = (0 * :001 + 1 \<le> :000 + 0)
139 :001 + 1 \<le> :000 + :001 \<equiv> 1 \<le> :000
139 (:001 + 1 \<le> :000 + :001) = (Numeral1 * :001 + 1 \<le> Numeral1 * :001 + :000)
137 2 + :000 \<le> :000 \<equiv> 2 \<le> 0
136 ?x \<equiv> a\<^sub>1
125 (1 + n \<le> n) = (0 * n + 1 \<le> 0)
125 1 + n \<le> n \<equiv> 1 \<le> 0
125 (1 + n \<le> n) = (Numeral1 * n + 1 \<le> Numeral1 * n + 0)
124 a + 1 \<le> a \<equiv> 0 + 1 \<le> 0
123 :000 + 1 + 1 = 2 * 1 + (:000 + 0)
123 :000 + 1 + 1 \<equiv> 2 + :000
123 :000 + 1 + 1 = Numeral1 * 1 + (Numeral1 * 1 + (:000 + 0))
122 k + 1 \<le> k \<equiv> 0 + 1 \<le> 0
119 (2 + :001 \<le> :001) = (0 * :001 + 2 \<le> 0)
119 (2 + :001 \<le> :001) = (Numeral1 * :001 + 2 \<le> Numeral1 * :001 + 0)
118 (n + 1 \<le> n) = (0 * n + 1 \<le> 0)
118 n + 1 \<le> n \<equiv> 1 \<le> 0
118 (n + 1 \<le> n) = (Numeral1 * n + 1 \<le> Numeral1 * n + 0)
117 k \<le> n \<Longrightarrow> n \<le> k \<equiv> n = k
117 (Suc m \<le> m) = (0 * m + Numeral1 \<le> 0)
117 Suc m \<le> m \<equiv> False
117 (Suc m \<le> m) = (Numeral1 * m + Numeral1 \<le> Numeral1 * m + 0)
116 a + 1 + 1 \<le> a \<equiv> 0 + 1 + 1 \<le> 0
112 u__ \<le> m__ * n__ \<Longrightarrow> m__ * n__ \<le> u__ \<equiv> m__ * n__ = u__
110 2 + :001 \<le> :001 \<equiv> 2 \<le> 0
110 n = 1 * n + 0
109 :001 + 1 + 1 = 2 * 1 + (:001 + 0)
109 :001 + 1 + 1 \<equiv> 2 + :001
109 :001 + 1 + 1 = Numeral1 * 1 + (Numeral1 * 1 + (:001 + 0))
109 a < 0 \<Longrightarrow> 0 \<le> a \<equiv> False
105 (2 + n \<le> n) = (0 * n + 2 \<le> 0)
105 (2 + n \<le> n) = (Numeral1 * n + 2 \<le> Numeral1 * n + 0)
105 a < 0 \<Longrightarrow> a \<le> 0 \<equiv> True
102 :000 < n \<Longrightarrow> n = 0 \<equiv> False
102 (Suc (:000 + n) \<le> n) = (0 * n + (Numeral1 + :000) \<le> 0)
102 Suc (:000 + n) \<le> n \<equiv> False
102 (Suc (:000 + n) \<le> n) = (Numeral1 * n + (Numeral1 + :000) \<le> Numeral1 * n + 0)
98 (Suc b__ \<le> b__) = (0 * b__ + Numeral1 \<le> 0)
98 Suc b__ \<le> b__ \<equiv> False
98 (Suc b__ \<le> b__) = (Numeral1 * b__ + Numeral1 \<le> Numeral1 * b__ + 0)
97 0 < y \<Longrightarrow> y \<le> 0 \<equiv> False
97 b' + 1 + 1 \<le> b' \<equiv> 0 + 1 + 1 \<le> 0
95 0 < b' \<Longrightarrow> 0 \<le> b' \<equiv> True
94 2 + n \<le> n \<equiv> 2 = 0
93 0 \<le> a \<Longrightarrow> a \<le> 0 \<equiv> a = 0
93 (a__ + 1 \<le> a__) = (0 * a__ + 1 \<le> 0)
93 a__ + 1 \<le> a__ \<equiv> 1 \<le> 0
93 (a__ + 1 \<le> a__) = (Numeral1 * a__ + 1 \<le> Numeral1 * a__ + 0)
91 2 * pi / 2 = 2 * (Numeral1 * pi) / (2 * (Numeral1 * 1))
91 2 * pi / 2 \<equiv> pi / 1
I guess you are also counting the theorems produced during rewriting by simprocs?
Mathias Fleury (Aug 22 2024 at 18:16):because a lot of steps look like that…
Mario Carneiro (Aug 22 2024 at 22:27):Is every step of a proof considered its own independent theorem? At the kernel level the only way I can tell that something is supposed to be a top level theorem is that they called unconstrainT or name_derivation or similar, which produces a new "proof box", which may or may not be properly named (so it does include a lot of internal things). My hope is that all of these theorems are actually put in public places where they will be reused multiple times, and are not simply a lemma for a single theorem and not otherwise accessible.
Mario Carneiro (Aug 22 2024 at 22:30):I think lemmas produced by simp preprocessing should be listed, but lemmas produced by simprocs should not (that's a prescriptive judgment, not a descriptive one - I'm pretty sure simprocs are producing many of these results) unless the lemmas are in some way reusable.
Mario Carneiro (Aug 23 2024 at 07:12):Here's an innocuous looking bit of Int.thy:
subsection ‹Integers form a commutative ring›
instantiation int :: comm_ring_1
begin
lift_definition zero_int :: "int" is "(0, 0)" .
lift_definition one_int :: "int" is "(1, 0)" .
lift_definition plus_int :: "int ⇒ int ⇒ int"
is "λ(x, y) (u, v). (x + u, y + v)"
by clarsimp
which is apparently (on the by clarsimp line) proving the following lemma:
Suc (:006 + :005 + (:004 + :007)) \<le> :004 + :007 + (:006 + :005) \<equiv> Suc (:006 + :005 + :007) \<le> :007 + (:006 + :005)
What even is this :005 notation? I've seen the notation for numbers and they don't involve colons or leading zeroes. I'm not sure whether this is the work of the clarsimp proof method or the lift_definition command, both of which sem a bit out of the ordinary.
Dmitriy Traytel (Aug 23 2024 at 07:24)::005 comes from ML ‹Name.bound 5›. I think terms might get such free variables introduced when they are inserted and later retrieved from a term net (~/src/Pure/net.ML), which the simplifier uses.
Dmitriy Traytel (Aug 23 2024 at 07:27):I had done some experiments in the past where I counted all theorems (type thm) produced by the kernel by instrumenting all functions that use the Thm constructor in thm.ML .
Dmitriy Traytel (Aug 23 2024 at 07:28):Those are the statistics for the proof of the first user-level theorem in HOL.thy:
1 gen_instantiate
1 generalize
1 reflexive
2 eta_conversion
2 incr_indexes
3 lift_rule
3 name_derivation
6 trim_context_thm
8 transfer
10 bicompose_aux
10 strip_shyps
14 adjust_maxidx_thm gteq
16 map_tags
And here are they for the declarations of lists:
1 eta_long_conversion
2 adjust_maxidx_thm(less)
5 unconstrainT
12 trivial
17 varifyT_global'
35 axiom
64 renamed_prop
81 forall_intr
129 permute_prems
188 rotated_rule
225 assumption
308 forall_elim
321 of_class
332 symmetric
497 implies_elim
518 beta_conversion
661 implies_intr
775 generalize
836 abstract_rule
839 name_derivation
908 equal_elim
991 assume
2420 map_tags
3015 transitive
3045 strip_shyps
4154 gen_instantiate
4723 lift_rule
4872 trim_context_thm
4922 combination
5460 bicompose_aux
5462 incr_indexes
5477 reflexive
7105 adjust_maxidx_thm(gteq)
17396 transfer
56139 eta_conversion
(The numbers are the numbers of calls to the respective function.)
Mario Carneiro (Aug 23 2024 at 07:30):that's not too different from what I'm doing now, except I'm restricting attention to top level theorems
Apparently the by metric line here generates 185 "top level theorems":
lemma "dist a b ≠ dist a c ⟹ b ≠ c"
by metric
most of them seem to be numerical evaluation lemmas like 1 - 1 / 2 = Numeral1 / Numeral1 * (1 / 1) + (- 1 / 2 * (1 / 1) + 0)
Mario Carneiro (Aug 23 2024 at 07:30):I can't help but think that this is a huge amount of garbage being unnecessarily pushed through the kernel
Mario Carneiro (Aug 23 2024 at 07:37):lemma "dist x y ≤ e ⟹ dist x z ≤ e ⟹ dist y z ≤ e
⟹ p ∈ (cball x e ∪ cball y e ∪ cball z e) ⟹ dist p x ≤ 2*e"
by metric
This theorem generates a proof 3 million proof steps long, which takes 500s just to hashcons for export. I'm thinking of modifying poly/ml to deal with these proofs
Last updated: Dec 21 2024 at 12:33 UTC