Email Gateway (Aug 22 2022 at 17:40): Email Gateway (Aug 22 2022 at 17:40):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Michael,
here is a slightly shortened (and completed) version of proof:
theorem (in solid) PLATONIC_SOLIDS:
fixes s::nat ― ‹number of sides on each face›
and m::nat ― ‹number of faces that meet at each vertex›
assumes "s ≥ 3" ― ‹faces must have at least 3 sides›
and "m ≥ 3" ― ‹at least three faces must meet at each vertex›
and "E>0"
and eq0: "s * F = 2 * E"
and eq1: "m * V = 2 * E"
shows "(s,m) ∈ {(3,3), (3,4), (3,5), (4,3), (5,3)}"
proof -
― ‹Following Euler, as explained here:
https://www.mathsisfun.com/geometry/platonic-solids-why-five.html›
have iq0: "1/s + 1/m > 1/2"
proof -
have f:"F = 2*E/s" using s ≥ 3 eq0 E>0
by (metis mult_eq_0_iff neq0_conv nonzero_mult_div_cancel_left of_nat_eq_0_iff of_nat_mult zero_neq_numeral)
have v:"V = 2*E/m" using m ≥ 3 eq1 E>0
by (metis mult_eq_0_iff neq0_conv nonzero_mult_div_cancel_left of_nat_eq_0_iff of_nat_mult zero_neq_numeral)
have "F + V - E = 2" using polyhedron_formula .
hence "(1/s + 1/m - 1/2) = 1/E" using E>0 f v
by (simp add: field_simps)
moreover from E>0 have "1/E>0" by simp
ultimately show ?thesis by argo
qed
hence "s ≤ 5" and "m ≤ 5"
proof -
have le5: "s≤5" if iq0: "1/s + 1/m > 1/2" and "m≥3" for s m :: nat
proof (rule ccontr)
assume "¬s≤5"
hence "s > 5" by simp
hence "1/s < 1/5" by simp
hence "1/5 + 1/m > 1/2" using iq0 by linarith
hence "1/m > 3/10" by simp
hence "m ≤ 3" using less_imp_inverse_less by fastforce
moreover have "m≠3"
using iq0 div_by_1 floor_of_nat s > 5 by (auto simp: linorder_not_le field_simps)
ultimately show "False" using m≥3 by auto
qed
show "s≤5"
using le5[of s m] iq0 m ≥ 3 by blast
show "m≤5"
using le5[of m s] iq0 s ≥ 3 by linarith
qed
hence "(s,m) ∈ {3,4,5} × {3,4,5}" using assms by force
thus "(s,m) ∈ {(3,3), (3,4), (3,5), (4,3), (5,3)}" using iq0 by force
qed
Some comments:
The step "le5" corresponds to your comment \<open>!HELP!: same argument as above, swapping m and s\<close>: I have generalised the expression to work for any s and m.
You had several steps either repeating the previous step (like hence "m < 10/3" […] hence "m < 10/3" by simp) or repeating it in an equivalent form (like hence "s ≤ 5" and "m ≤ 5" […] hence "s ≤ 5 ∧ m ≤ 5").
thus "¬s≤5 ⟹ False" by simp works but is strange. You already have the assumption "¬s≤5", so "thus False" is enough (in this case it can be merged with the previous line).
ac_simps, algebra_simps, and field_simps are collections of simplifications lemmas that are useful here. It is probably possible to shorten the proof more with these lemmas.
Any thoughts on how I could streamline this?
If you finish the proof of polyhedron_formula, it would be a good candidate for an AFP entry <https://www.isa-afp.org/>.
Cheers,
Mathias
On 24. Jul 2018, at 08:44, Michal Wallace <michal.wallace@gmail.com> wrote:
Hi all,
I made a start on a proof of the number of platonic solids (#50 on Freek
Wiedijk's "formalizing 100 theorems" page):(nicely formatted gist:)
https://gist.github.com/tangentstorm/23bed08c4086a22c7100982790cbda83(actual isar file:)
https://github.com/tangentstorm/tangentlabs/blob/master/isar/Poly100.thyIt relies on the polyhedron formula, which is #13 on the list, and also
outstanding in Isabelle, AFAIK. I'm planning to take that on next, but I
was hoping to get some feedback on what I've done so far... It feels pretty
verbose/redundant, and I'm hoping some of you Isabelle experts can help me
make it nicer. :)Any thoughts on how I could streamline this?
Thanks!
Michal J Wallace
http://tangentstorm.com/
Email Gateway (Aug 22 2022 at 17:41):From: Makarius <makarius@sketis.net>
A note on Isar style: you are using 'hence' with 'using' a lot, but that
is slightly awkward.
Isar proofs become more smooth (and overall shorter) if you abandon
'hence' and 'thus' altogether and use 'have' / 'show' with 'from' /
'with' more often than 'using'.
The general pattern is as follows:
have something \<proof> (* last fact: "this" *)
with primary_facts have something_else
using secondary_facts \<proof>
Where primary_facts are things you just had a few lines before, and
secondary_facts from further off or from the library.
Makarius
Email Gateway (Aug 22 2022 at 17:42):From: Makarius <makarius@sketis.net>
I've now seen your updates on Github:
https://github.com/tangentstorm/tangentlabs/commit/09a7b30a9a3758d5648a0e424541dec3195c0966
Some more hints:
from facts have something .
is more often written like this:
have something by (rule facts)
or more rarely like this:
have something by (fact facts)
or occasionally even:
note ‹something›
The last form has a delicate point, though: its literal fact proposition
does not bind the ellipsis ("…") for the ongoing calculation.
Makarius
Email Gateway (Aug 22 2022 at 17:54):From: Michal Wallace <michal.wallace@gmail.com>
Hi all,
I made a start on a proof of the number of platonic solids (#50 on Freek
Wiedijk's "formalizing 100 theorems" page):
(nicely formatted gist:)
https://gist.github.com/tangentstorm/23bed08c4086a22c7100982790cbda83
(actual isar file:)
https://github.com/tangentstorm/tangentlabs/blob/master/isar/Poly100.thy
It relies on the polyhedron formula, which is #13 on the list, and also
outstanding in Isabelle, AFAIK. I'm planning to take that on next, but I
was hoping to get some feedback on what I've done so far... It feels pretty
verbose/redundant, and I'm hoping some of you Isabelle experts can help me
make it nicer. :)
Any thoughts on how I could streamline this?
Thanks!
Michal J Wallace
http://tangentstorm.com/
Last updated: Apr 26 2024 at 08:19 UTC