Simon Hanssen (Jun 21 2021 at 10:00): Simon Hanssen (Jun 21 2021 at 10:00):So I got to the point where my proof state looks like this
using this:
∀x y. x ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ y ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ on_line x y r ⟹
r ∈ convex_polygon_of_points [p1, p2, p3, p1]
∀x y. x ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ y ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ on_line x y r ⟹
r ∈ convex_polygon_of_points [p1, p2, p3, p1] ⟹ convex (convex_polygon_of_points [p1, p2, p3, p1])
goal (1 subgoal):
1. convex (convex_polygon_of_points [p1, p2, p3, p1])
From how this looks to me, this shouldn't be the hardest thing to prove, but somehow nothing succeeds.
The original theorem I intended to use looks like this ∀x y. x ∈ ?s ∧ y ∈ ?s ∧ on_line x y ?p ⟹ ?p ∈ ?s ⟹ convex ?s but even instanitating the unknowns in it doen't seem to help.
Mathias Fleury (Jun 21 2021 at 10:04):If I read this correctly,
∀x y. x ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ y ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ on_line x y r ⟹
convex (convex_polygon_of_points [p1, p2, p3, p1])
is an obvious consequence (and probably what you have in mind), but I don't see how to discharge ∀x y. x ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ y ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ on_line x y r
Mathias Fleury (Jun 21 2021 at 10:08):In Isabelle terms:
lemma
assumes
"∀x y. x ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ y ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ on_line x y r ⟹
r ∈ convex_polygon_of_points [p1, p2, p3, p1]" (is ‹?A ⟹ ?B›)
"∀x y. x ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ y ∈ convex_polygon_of_points [p1, p2, p3, p1] ∧ on_line x y r ⟹
r ∈ convex_polygon_of_points [p1, p2, p3, p1] ⟹ convex (convex_polygon_of_points [p1, p2, p3, p1])"
(is ‹?A ⟹ ?B ⟹ _›)
shows "convex (convex_polygon_of_points [p1, p2, p3, p1])"
proof -
have H: ?thesis if ?A
apply (rule assms(2))
apply (rule that)
apply (rule assms(1))
apply (rule that)
done
show ?thesis
apply (rule H)
(*not obviously entailed by your assumption*)
oops
(I have no knowledge of the symbols here: without interpretation, quickcheck finds a counterexample)
Mathias Fleury (Jun 21 2021 at 10:15):About the title, you are trying to prove that:
lemma ‹(A ⟶ B) ∧ (A ⟶ B ⟶ C) ⟹ C›
nitpick
oops
and that does not hold for everything False.
Simon Hanssen (Jun 21 2021 at 10:28):Mathias Fleury said:
About the title, you are trying to prove that:
lemma ‹(A ⟶ B) ∧ (A ⟶ B ⟶ C) ⟹ C› nitpick oopsand that does not hold for everything False.
Seems like I somehow got a wrong idea with that... I now am even more confused than before, but i think your anwer might help getting to the core of it.
Simon Hanssen (Jun 21 2021 at 10:33):Looking at it I guess there is a fundamental flaw in ∀x. x ∈ s as it rather should be ∀x ∈s.
Mathias Fleury (Jun 21 2021 at 10:34):are you confusing ∀x. P ==> Q with ∀x. (P ==> Q)?
Mathias Fleury (Jun 21 2021 at 10:35):because ∀x ∈ s. P x is exactly ∀x. (x ∈ s --> P)
Simon Hanssen (Jun 21 2021 at 10:42):I think I am messing everything together right now... l'll take a break mabye I'll be less confused afterwards :sweat_smile:
Simon Hanssen (Jun 21 2021 at 15:58):Okay there were two problems,
First, I should have written ∀x∈s. ∀y∈s. ∀p. on_line x y p ⟶ p ∈ s⟹ convex s as this was what I actually meant to say, not quantifying p was gibberish.
And second I fixed x and y and then assumed what i needed for them instead of just fixing them and showing that if my assumtions hold more follows (if that makes any sense)
Manuel Eberl (Jun 21 2021 at 16:04):You probably defined on_line yourself, right? Note that HOL-Analysis contains the definition closed_segment together with a lot of other material about convexity.
Simon Hanssen (Jun 21 2021 at 16:15):Yes I did. Looking at closed_segment it seems to be pretty much what I needed, but it is working on vectors though while Councerclockwise_2D_Strict uses points
Simon Hanssen (Jun 21 2021 at 16:17):(there might aswell be a conversion but seems like i didn't find that yet)
Manuel Eberl (Jun 21 2021 at 16:22):What is a point?
Manuel Eberl (Jun 21 2021 at 16:23):Ah, point is just an abbreviation for real × real. That should work fine with closed_segment though.
Manuel Eberl (Jun 21 2021 at 16:24):Yes, works fine:
term "closed_segment (1,2) (3::real,4::real)"`
closed_segment has type 'a::real_vector ⇒ 'a ⇒ 'a set, i.e. it works for any type that has a real_vector instance. And there are corresponding instances for real and the product type, so real × real works fine.
Last updated: Jul 15 2022 at 23:21 UTC