loganrjmurphy
Deaxiomatizing System E
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.
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?
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?
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.
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
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?
It would be more helpful if the screenshot include complete information. Currently I cannot see which tactic is failing and the exact error message.
Sorry folks, I've just returned from a few weeks away. I'll look into this this week.
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)?
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
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.
