Code not compiling

Stream: new members

[Andre Hernandez-Espiet (Rutgers)]

Hi all. I was messing around with some code, and for some reason it decided to give me some odd errors. Could anybody suggest what I am doing wrong? Below I have attached the error it gives and the file I was using.

image.png test.lean test.lean

[Alex J. Best]

Unfortunately we can't tell from your screenshot what the definition of B is as we don't have the file you are working on, it's much easier to help if you can post copy-pasteable code in the form of a #mwe. Even if its a full file.

[Kevin Buzzard]

If you read the error you will see that it says that B does not want to eat a, it wants to eat something of a different type. If you hover over B you'll see its type and what will be happening is that the first round bracket input for B will not be the thing you want to set as a. But in general, what Alex said.

[Alex J. Best]

If I had to guess though I'd say B had explicit arguments for the type point and line, so you might want B point line a b c instead but its just a guess.

[Andre Hernandez-Espiet (Rutgers)]

That is odd. I thought I had attached the file. Here it is again. test.lean

[Alex J. Best]

You did! My bad, it just came up next to the link to the image title so I didn't spot it, sorry for the noise :smile:, Or maybe I didn't see the edit in time as my internet is spotty...

[Kevin Buzzard]

Oh my bad too :-) Apologies. What people usually do is post code and errors between triple back-ticks rather than uploading files or screenshots.

[Kevin Buzzard]

Indeed, if you hover over B then you see

Euclidean_plane.B : Π {point : Type} (line : Type) [self : Euclidean_plane point line], point → point → point → Prop

so the first input which B wants from the user is a term line of type Type, and you gave it a point -- the point is supposed to come later.

[Andre Hernandez-Espiet (Rutgers)]

Hmm, but I defined B with point → point → point → Prop. Why would it be expecting a line? Does this have to do with the second line in the code?

[Kevin Buzzard]

class Euclidean_plane (point : Type) (line : Type):=
(B : point → point → point → Prop)

#check Euclidean_plane.B
/-
Euclidean_plane.B : Π (line : Type) [self : Euclidean_plane ?M_1 line], ?M_1 → ?M_1 → ?M_1 → Prop
-/

It's to do with design decisions when making structures. Euclidean_plane expects inputs point and line, but B can't possibly figure out what line is because it only takes terms of type point so it asks the user to supply it explicitly.

[Kevin Buzzard]

By the way you might be interested in my summer student Tianchen Zhao's project on Hilbert's set-up for Euclidean geometry: https://ja1941.github.io/hilberts-axioms/

[Andre Hernandez-Espiet (Rutgers)]

Yes that does seem interesting. Thanks for sharing.

How would I have to modify the class so that I have two objects 'point' and 'line' but that they would not be both required as inputs for the 'B' function?

[Alex J. Best]

Well the way its set up, there could be multiple different euclidean plane structures on your type e.g.

namespace Euclidean_plane
variables {point : Type} {line line2 : Type} [Euclidean_plane point line2] [Euclidean_plane point line]

local attribute [instance, priority 0] prop_decidable



theorem LinesOnePt {p p': point} {l1 l2 : line} (l1≠ l2): pointline p l1 →  pointline p l2 →  pointline p' l1 →  pointline p' l2 → p=p':=
begin
  intros hyp1 hyp2 hyp3 hyp4,
  apply by_contra,
  intros h,
  exact H( I1b p p' l1 l2 h hyp1 hyp3 hyp2 hyp4),

end

theorem afs (a b c  : point)  : B a b c → B a b c:=
begin
 tauto,
end
--def parallel (l1 l2 : line) : Prop := ∀ (a : point) pointline a l1 → ¬ pointline a l2


end Euclidean_plane

which should B refer to the Euclidean plane structure with line or line2?

[Alex J. Best]

That said, there is a way to achieve this with docs#out_param as follows:

import  data.set tactic.interactive
class Euclidean_plane (point : Type) (line : out_param Type):=
-- Equidistance of 4 Points

(pointline : point → line → Prop)
--pointline P L means P is on L
(eqd : point → point → point → point → Prop)

-- Between A B C means B is on the line segment AC
(B : point → point → point → Prop)
[dec_B : ∀ a b c, decidable (B a b c)]

(P1 {} : point) (P2 {} : point) (P3 {} : point)

(I1a : ∀ (a b : point), a≠b → ∃ (l: line) , pointline a l ∧ pointline b l)
(I1b : ∀ (a b : point), ∀ (l l': line), a≠b →  pointline a l →  pointline b l →  pointline a l' →  pointline b l'  →l=l')
(I2 : ∀ l : line, ∃ (X:point×point), pointline X.1 l ∧ pointline X.2 l ∧ X.1≠ X.2)
(I3 : ¬ ∃ l : line , pointline P1 l ∧ pointline P2 l ∧ pointline P3 l)


open classical
namespace Euclidean_plane
variables {point : Type} {line : Type} [Euclidean_plane point line]

local attribute [instance, priority 0] prop_decidable



theorem LinesOnePt {p p': point} {l1 l2 : line} (l1≠ l2): pointline p l1 →  pointline p l2 →  pointline p' l1 →  pointline p' l2 → p=p':=
begin
  intros hyp1 hyp2 hyp3 hyp4,
  apply by_contra,
  intros h,
  exact H( I1b p p' l1 l2 h hyp1 hyp3 hyp2 hyp4),

end

include line
theorem afs (a b c  : point)  : B a b c → B a b c:=
begin
 tauto,
end
--def parallel (l1 l2 : line) : Prop := ∀ (a : point) pointline a l1 → ¬ pointline a l2


end Euclidean_plane

[Andre Hernandez-Espiet (Rutgers)]

Where are you seeing the line "variables {point : Type} {line line2 : Type} [Euclidean_plane point line2] [Euclidean_plane point line]"?
I tried the "out_param" idea but it still gives me an error, unless I am misunderstanding something about this.
Sorry I'm so confused, I'm just kind of new to this kind of thing.

[Alex J. Best]

I modified all lines of your code to give some examples.
In the first message, I tried to show why lean is complaining that it wants to be told which line you are talking about, because if you have more variables there are two possible answers

[Alex J. Best]

For the out param I gave the full file test.lean again after my changes, it compiles on my machine

[Alex J. Best]

what error are you getting?

[Alex J. Best]

I would recommend you just write B line a b c for now whenever you want to say that a b c lie on the same line in the euclidean plane structure on point and line that you assume exists

[Andre Hernandez-Espiet (Rutgers)]

Ooooh it seems that I missed the "include line" that you put. Thanks a lot, it does work now!

[Kyle Miller]

If you want line to be implicit, then you can use the {} feature along with out_param:

class Euclidean_plane (point : Type) (line : out_param $ Type):=
(B {} : point → point → point → Prop)

#check @Euclidean_plane.B
-- Euclidean_plane.B : Π {point line : Type} [self : Euclidean_plane point line], point → point → point → Prop

(B [] also works, and I forget what the difference is...)

[Kevin Buzzard]

I would have mentioned this but I couldn't get it to work -- I think that without the out_param it won't do this? Looks like you have it working though.

[Kyle Miller]

Yeah, I had no idea that out_param interacts with {} like this, but nice to see that it does.

[Andre Hernandez-Espiet (Rutgers)]

Kyle Miller said:

If you want line to be implicit, then you can use the {} feature along with out_param:

class Euclidean_plane (point : Type) (line : out_param $ Type):=
(B {} : point → point → point → Prop)

#check @Euclidean_plane.B
-- Euclidean_plane.B : Π {point line : Type} [self : Euclidean_plane point line], point → point → point → Prop

(B [] also works, and I forget what the difference is...)

I couldn't quite make this one work. I wonder why...

[Kyle Miller]

@Andre Hernandez-Espiet (Rutgers) I'm not sure what I observed yesterday... I thought I had tested all four combinations of including or excluding out_param and {}, but I must not have tested out_param by itself. Sorry about that. It seems like out_param is all you need to make B take line implicitly.