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.

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 `

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)

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.

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.

Looking at it I guess there is a fundamental flaw in `∀x. x ∈ s`

as it rather should be `∀x ∈s.`

are you confusing `∀x. P ==> Q`

with `∀x. (P ==> Q)`

?

because `∀x ∈ s. P x`

is exactly `∀x. (x ∈ s --> P)`

I think I am messing everything together right now... l'll take a break mabye I'll be less confused afterwards :sweat_smile:

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)

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.

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

(there might aswell be a conversion but seems like i didn't find that yet)

What is a point?

Ah, `point`

is just an abbreviation for `real × real`

. That should work fine with `closed_segment`

though.

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