## Stream: Beginner Questions

### Topic: ((A ==> B) & A) ==> B?

#### 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):

``````∀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
``````

#### Mathias Fleury (Jun 21 2021 at 10:09):

(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
oops
``````

and 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)

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)"`
``````

#### Manuel Eberl (Jun 21 2021 at 16:25):

`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