Some axioms are wrong.

[miguelmarco]

I have noticed that some axioms are either not corresponding to Avigad's paper or plainly wrong.

For example,

axiom intersection_circles : ∀ (α β : Circle), α.intersectsCircle β →
  ∃ a : Point, (a.onCircle α) ∧ (a.onCircle β)

states that a circle intersecting another circle implies the existence of a common point. However, the paper that describes system E states clearly that intersection means transverse intersection, and provides an axiom that states that if two circles intersect, there are two different common points.

That was an example of this implementation diverging from the paper.

However, this is worse:

axiom intersection_circle_circle_1: ∀ (a b : Point) (α β : Circle),
  ¬(a.outsideCircle α) ∧ ¬(b.outsideCircle α) ∧ (a.insideCircle β) ∧ (b.outsideCircle β) →
   α.intersectsCircle β

as it is not true in Euclid's geometry: if β is contained in the interior of α (bit is smaller than α) , just take a being inside β and b in the region between α and β, this satisfies the hypothesis of this statement. But those circles should not intersect.

I think this comes from the paper, that says:

If a is on or inside α, b is on or inside α, a is inside β, and b is outside β,
then α and β intersect.

so in this case the error comes from the paper.

[miguelmarco]

In private communication, Avigad has told me that there is a mistake in the paper. There should be no or inside.

[yangky11]

Hi,

As discussed in the LeanEuclid paper, it implements a variant of Avigad's system E, so there may be some discrepancies in the axioms. Also, intersection_circles is actually correct even for a transverse intersection.

Thanks for pointing out the intersection_circle_circle_1 error! I'll fix it in this codebase.