Deaxiomatizing System E

[FrederickPu]

Right now System E is formulated as a bunch of axioms.
However, I believe it would more sensible for it to be formulated as a type class such as Group.
All of the theorems would more or less be the same, but proofs from LeanEuclid could more readily be used to prove theorems about the EuclideanSpace typeclass.
Additionally, it would make it easier to construct models of System E and prove the consistency of System E and/or that it has been properly formalized.

I understand that this may be beyond the scope of the project, but I would be willing to do this in a separate branch and make a pull request.

[yangky11]

Hi, we probably won't have the capacity for this, but PRs are welcome!

[FrederickPu]

Hi, for mathlib I remember that they wanted me to create a PR from a branch, in which case I would need to be given some sort of permission. In this case, should I just make my changes in a fork and then create a PR from that fork?

[yangky11]

You could just PR from your own fork.

[FrederickPu]

alright thanks!

[FrederickPu]

The proofs in Book/Prop01 are failing cause euclid_apply can't solve the goals. I also noticed that some of the latest commits are failing the ci process. Is this just an issue with the latest commits?

[yangky11]

Which theorem is failing? Can you paste the SMT query displayed in the infoview panel?

Most failures are due to the instability of SMT solvers across different platforms or even different runs on the same platform. It may help to upgrade to the latest development version of Z3 and CVC5.

[FrederickPu]

It's failing on this theorem

theorem proposition_1 : ∀ (a b : Point) (AB : Line),
  distinctPointsOnLine a b AB →
  ∃ c : Point, |(c─a)| = |(a─b)| ∧ |(c─b)| = |(a─b)| :=
by
  euclid_intros
  euclid_apply circle_from_points a b as BCD
  euclid_apply circle_from_points b a as ACE -- failing on this line
  euclid_apply intersection_circles BCD ACE as c
  euclid_apply point_on_circle_onlyif a b c BCD
  euclid_apply point_on_circle_onlyif b a c ACE
  use c
  euclid_finish

It's saying could not prove: ¬b = a
Also, I don't see any smt query displayed in the infoview panel

[yangky11]

If it's proposition_1, it's probably not an SMT issue (only the last few proofs are challenging for SMT). I don't see immediately what the issue is. ¬b = a shouldn't be difficult since it's implied by the definition of distinctPointsOnLine.

Can you take a screenshot of the infoview panel?

[FrederickPu]

[FrederickPu]

somehow it's not picking up on symmetry of equality or something

[yangky11]

It would be more helpful if the screenshot include complete information. Currently I cannot see which tactic is failing and the exact error message.

[FrederickPu]

[yangky11]

I'm not able to reproduce this issue. @loganrjmurphy any idea?

[loganrjmurphy]

Sorry folks, I've just returned from a few weeks away. I'll look into this this week.

[loganrjmurphy]

Hi Frederick, I also can't reproduce what you're seeing. Could you confirm which version of Lean is being used? I.e., from within the project directory, run elan show and see what appears under "active toolchain". I assume that there were no build issues otherwise (i.e., steps 1-3 here)?

[FrederickPu]

sorry, I just got a new computer after the old one bricked. I'm trying to setup the repo again i cant seem to find Server Env Paths in the settings for the lean4 extension

[Suyashtnt]

Hello. I'm having the same issue after cloning and running the instructions.

NOTE: to get it to build I did have to change Solve.lean finish

/- invoke `applyHole` only if the hole actually exists -/
def finish : EuclidStepM Unit := do
  let Γ ← read
  withMainContext do
    match (← getLCtx).findFromUserName? Γ.holeName with
    | none =>   dbg_trace "finish: fail" ; failure
    | some d =>
      applyHole (← d.toExpr.toSyntax) (← getUnusedUserName `h) |>.run Γ
      evalTactic $ ← `(tactic| try (clear ($(mkIdent Γ.holeName))))
      evalTactic $ ← `(tactic| try aesop (add safe [destructProducts])) /- <- Changed line 70 -/

smt-portfolio & Co is installed

PS C:\Users\suyas\OneDrive\Documents\LeanEuclid> Where.exe smt-portfolio 
C:\Users\suyas\OneDrive\Documents\LeanEuclid\.venv\Scripts\smt-portfolio.exe
PS C:\Users\suyas\OneDrive\Documents\LeanEuclid> lake script run check                                                                                                               
All requirements are satisfied.