0.3 (during following months, ideally until ICMS-2020 13.7. -- deeper connection between GUI and logic)

Main objectives for 0.3:
* (1) ability to create custom tools / lemmata
  * (1a) level creation
  * (1b) more flexible step editing
* (2) level solving
  * (2a) capture basic solving steps (problem reformulation, partial goal)
  * (2b) detect solved level (including sublemmata)
* (3) support for problems without direct construction
  * (3a) (re)capturing objects by a construction
  * examples
    * three points, circumcenter, and a point on it
      -> first a circle, then 4 points on it
    * triangle ABC, its incenter I
      -> first triangle ABI, constructing C out of it
    * given X,Y on a line so that XA = YB, make X movable and Y constructed using compass

Co je obecný stav?
* (1,3) (nehýbatelné) vstupní objekty
* (1) předpoklady (postulate)
* (1) proof (check, nevadí, když jednotlivý krok selže)
* (1,1b) závěry (check, možnost vytvořit pouze pár typů)

* Dorozmyslet (!):
  * Pravidla přechycení,
    a jak zajistit kompatibilitu s původním levelem

Akce:
* (3a) "zafixovat" objekt závislý jenom na vstupních objektech
  * (přidat předpoklady)?
* (3a) Jak něco odfixovat?
  * TODO
* (1a) fact tool (pro začátek funkčnost jako v geogebře -- numerický check)
  * přidat předpoklad, přidat cíl
* odebrat předpoklad / cíl
* (1b) přesunout / smazat krok
* (1b) analýza, proč krok selhal
* (1b) otevřít krok
* (1b,2a) přehled lemmat, která nejsou dokázaná
* (2b) reset input, check všech důkazů
* (1b) editace, k čemu je chycený průsečík
* (2a)
  * stanovení podcíle
    * vybrat vstupní objekty
    * vybrat předpoklady
    * podcíl
    * (export podcíle jako nástroje)
  * reformulace cíle
    * TODO
* jak zkombinovat fix / unfix a editaci předpokladů s řešením levelu?
* undo / redo v rámci komplexnějšich akcí

Remained
* more straightforward drawing of lies_on, computation of missing line:
  * own implementation of line / circle cut for points not contained by them
    -> cleaner exported picture, less drawing moves
* completely movable objects line / circle

long-term (more features)
* display equations
* geometrical mappings
  * general similar mapping without exceptions (copy_triangle does not support collinear points)
  * transferring objects, facts
  * automatic proof of compatibility of a symmetry and a tool
* separate logic and automatization
  * trace the assumptions used for a proof
* other intersection options?
  * So that XOO' has the same orientation as ABC
  * with a line AB firther in the direction AB
  (both cases can be emulated using current tools)

* more sophisticated tools
  * hidden construction
    * so there are less known facts in the end
    * non-expanding composed predicated (such as tangent)
  * num_check optimisation
    (find the propositions in a proof that should be checked without
    executing the entire proof from scratch)
  * alternative proofs (if the original proof fails)
  * allow proof more mixed with conclusions?
  * rigid check of elementary facts (topological reasoning)
    * case split
    * proof by contradiction
    * inequalities -> linear programming?
    * predicates:
      * ordered: P P P, P L P, P P L
      * oriented_as as a predicate about directions (Angle)
    * axioms / lemmata?
      * COMPLEMENTARY: A == B, A not_eq B
      * COMPLEMENTARY: A lies_on pc, A not_on pc
      * INCOMPATIBLE:
        oriented_as a0 a1 a2 b0 b1 b2
        oriented_as a0 a1 a2 b0 b2 b1
      * COVERING:
        oriented_as a0 a1 a2 b0 b1 b2
        oriented_as a0 a1 a2 b0 b2 b1
	a0 == a1
	a1 == a2
	a2 == a0
	b0 == b1
	b1 == b2
	b2 == b0
      * COVERING:
	A == B
	B == C
	C == A
        l = line A B, C not_on l
        ordered A B C
	ordered A C B
      * A not_on l, B lies_on l -> A != B
      * ordered A p B -> A != B, intersecting (line A B) p
      * A not_on (line B C) -> B not_on (line A C)
      * M = midpoint A B -> ordered A M B
      * ordered: transitivity + symmetry
      * ordered A B C -> not_eq A B, not_eq A C
      * ordered A p B -> not_on A p, not_eq A B
      * ordered A B p -> not_on A p, not_on B p
      * ordered A B C, B lies_on p, A not_on p -> diff_side A p C
        + similar analogous
      * oriented_as: transitivity + symmetry
      * A not_on p, B C D on p, ordered B C D
      	-> oriented_as A B C A B D
      * angle_pred a == (const != 0) + b -> not_eq a b
      * (direction_of l1) != (direction_of l2) -> intersecting l1, l2