circumcenter

Stream: general

[Damiano Testa]

Dear All,

I investigated a bit the circumcenter proof and I noticed something strange. In the file geometry/euclidean/basic.lean, lemma orthogonal_projection_vadd_smul_vsub_orthogonal_projection has among its assumptions both [nonempty s] and (hp : p1 ∈ s). This trickles down (and possibly up) to nonempty assumptions in several other lemmas. In particular, lemma eq_or_eq_reflection_of_dist_eq in geometry/euclidean/circumcenter.lean has some weirdness in its proof which, I believe, is partly caused by this. For instance, the have hn and have hc are unnecessary in the proof, but do appear as side goals that disappear on their own.

I am not fixing it myself, since I am not sure how to proceed: this is how I can "fix" orthogonal_projection_vadd_smul_vsub_orthogonal_projection:

lemma exxx {V P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P]
  {s : affine_subspace ℝ P} {p1 : P} (hp : p1 ∈ s) :
  nonempty ↥s :=
have f : inhabited s := {default := ⟨p1, by simpa⟩},
@nonempty_of_inhabited _ f

/-- Adding a vector to a point in the given subspace, then taking the
orthogonal projection, produces the original point if the vector is a
multiple of the result of subtracting a point's orthogonal projection
from that point. -/
lemma orthogonal_projection_vadd_smul_vsub_orthogonal_projection {s : affine_subspace ℝ P}
  [complete_space s.direction] {p1 : P} (p2 : P) (r : ℝ) (hp : p1 ∈ s) :
  @orthogonal_projection _ _ _ _ _ s (exxx hp) _
    (r • (p2 -ᵥ @orthogonal_projection _ _ _ _ _ s (exxx hp) _ p2 : V) +ᵥ p1) = ⟨p1, hp⟩ :=
@orthogonal_projection_vadd_eq_self _ _ _ _ _ _ (exxx hp) _ _ hp _
  (submodule.smul_mem _ _ (@vsub_orthogonal_projection_mem_direction_orthogonal _ _ _ _ _ s (exxx hp) _ _))

which does not look too good...

[Mario Carneiro]

For data-carrying typeclasses, this kind of transformation is generally not a good idea. Despite the apparent redundancy you should keep the typeclass arguments even though the hypotheses imply them. For Prop-classes it's not as much of a problem but it's still not really worthwhile. You can remove the typeclass arguments and use haveI to discharge them if they stop appearing in the types and only end up in the proof.

[Damiano Testa]

Ok, although, actually, the lines have hn and have hc are entirely redundant in the proof: Lean takes care of proving those side goals, even without assuming them.

[Damiano Testa]

Maybe I should simply remove the unnecessary lines. Besides, I only looked at this file since it timed out at some point.

[Mario Carneiro]

I wasn't able to find any theorems that had nonempty s assumptions which did not also mention orthogonal_projection or reflection

[Damiano Testa]

Here is a simple shortening: #7852.

[Damiano Testa]

In any case, I will no longer investigate this nonempty + member issue. Mario, I think that what you are saying is that the strangeness is not so evil and that I should simply live with it, right? :upside_down:

[Mario Carneiro]

it's "more general" for a very weird definition of general

[Heather Macbeth]

I was the one who introduced all these nonemptys, in #5408. I wanted to be able to define the orthogonal projection only when it made sense (which requires nonempty and complete_space), rather than have it always be defined and take on a junk value when it didn't make sense.

[Damiano Testa]

Heather, it certainly makes sense. I just was hoping that having an element in a type would "magically" produce a nonempty instance. I realize that this is probably not a good idea, though!