Question: proving pythagoras theorem

primepatel commented 2 years ago

Could we prove Pythagoras theorem using GeometricTheoremProver.jl ? I tried, but it showed an error. I also had a quick look in the documentation but did not find anything useful.

lucaferranti commented 2 years ago

Ritt-Wu algorithm in principle should be able to prove pythagoras theorem. The problem is that the parser currently cannot handle arbitrary expressions involving lengths like AB^2 + BC^2 = AC^2 for pythagoras theorem. Such functionality would definitely be nice to introduce gradually, e.g. starting by allowing expressions with lengths square.

Meanwhile, it would definitely be good to have more informative error messages when the parser fails, could you copy-paste how you tried to write hypothesis and thesis and what error you got?

primepatel commented 2 years ago

I tried something like this.

using GeometricTheoremProver

hp = @hp begin
    points(A, B, C)
    C :=  Segment(A, B) ⟂ Segment(B, C)
end

POINTS:
------------
A : free
B : free
C : semifree by (1)

HYPOTHESIS:
------------
(1) AB ⟂ BC

th = @th Segment(A, B)^2 + Segment(B, C)^2 == Segment(A, C)^2

LoadError: MethodError: no method matching _quotenodify(::Int64)
Closest candidates are:
  _quotenodify(::Expr) at ~\Julia\GeometricTheoremProver.jl\src\theorem\parse_constraints.jl:42
  _quotenodify(::Symbol) at ~\Julia\GeometricTheoremProver.jl\src\theorem\parse_constraints.jl:49
in expression starting at In[7]:1

prove(hp, th)

Language specifications doesn't have something like length. If somehow you could introduce the length attribute to the object Segment, then I guess the problem could be solved.

BTW, package worked fine for many other thms not involving ratio of Segments and Angles. Thanks

lucaferranti / GeometricTheoremProver.jl

Question: proving pythagoras theorem #8