Zulip Chat Archive

The answer to the question is that c.center is fine, but you can't #print it because Lean doesn't know how to #print a point. You can do #check c.center to see that indeed it is a point, and you could even prove that the point is (0,0).

Eric Wieser (Nov 18 2022 at 15:36):

Kevin Buzzard said:

but you can't #print it because Lean doesn't know how to #print a point.

It's more fundamental than this, #print isn't for printing values at all

learnreal (Nov 18 2022 at 15:39):

Ahh. Got that now. Thanks a lot. #eval works.

learnreal (Nov 18 2022 at 15:40):

Eric Wieser said:

are (0, 0), 5 and (0, 0), -5 different circles?

Right. I see the point. How do I enforce the constraint that radius should be positive?

Eric Wieser (Nov 18 2022 at 16:24):

You could use docs#nnreal for the radius if you're happy with radius 0

learnreal (Nov 18 2022 at 16:42):

Eric Wieser said:

You could use docs#nnreal for the radius if you're happy with radius 0

Yes. That works for me.

However, what is best way to have general checks? Like "if radius is < 0 then return error else return my circle" kind of a thing.

Patrick Johnson (Nov 18 2022 at 16:54):

I have no idea what you're trying to implement. This is literal answer to your question, but I doubt it's what you actually want.

def mk_circ (x y r : ℝ) : string ⊕ circle :=
if r < 0
then sum.inl "Radius cannot be negative"
else sum.inr ⟨⟨x, y⟩, r⟩

learnreal (Nov 18 2022 at 17:27):

Thank you. This helps.

I am actually trying to define a circle, a tangent and prove that tangent is right angle to the radius. It might not need what I actually wrote above. But, still struggling to model the scenario correctly and move to the proof part.

Eric Wieser (Nov 18 2022 at 17:28):

However, what is best way to have general checks? Like "if radius is < 0 then return error else return my circle" kind of a thing.

You don't need this type of check if you use nnreal. Just like in C you don't need a "if this is not a whole number error" if you use int instead of float.

Kyle Miller (Nov 18 2022 at 17:30):

To give an alternative to nnreal, just for sake of example, here's how you can model a circle with positive radius:

structure circle :=
  (center: point) (radius: ℝ) (radius_pos : 0 < radius)

Kyle Miller (Nov 18 2022 at 17:31):

It's just impossible to create a circle with non-positive radius with this, since they require a proof of positivity to be constructed.

learnreal (Nov 18 2022 at 17:33):

It might be useful elsewhere. For eg.,

  (x y: \real)

structure circle :=
  (center: point) (radius: ℝ)

def circle.makenew (d e f: ℝ): circle :=
    circle.mk c (point.mk (-d/2) (-e/2)) (real.sqrt ((((d*d)+(e*e))/4)-f))

I might want to return an error if dd+ee < 4f. Do you suggest a better way to handle this instead of doing "if ... else"?

learnreal (Nov 18 2022 at 17:34):

Kyle Miller said:

To give an alternative to nnreal, just for sake of example, here's how you can model a circle with positive radius:
structure circle :=
  (center: point) (radius: ℝ) (radius_pos : 0 < radius)

Trying to understand here. Are we saying "radius_pos is a proposition and this prop has to be true for the proof to proceed"?

Kyle Miller (Nov 18 2022 at 17:36):

It's saying circle.mk takes three arguments to construct a circle: a point, a real, and a proof of 0 < radius.

Kyle Miller (Nov 18 2022 at 17:36):

if 0 < radius is false then you won't be able to construct a circle since you can't supply a proof

learnreal (Nov 18 2022 at 17:36):

Kyle Miller said:

It's saying circle.mk takes three arguments to construct a circle: a point, a real, and a proof of 0 < radius.

Understood. Thanks a lot. This clears up quite a few things for me.

Kyle Miller (Nov 18 2022 at 17:37):

(Lean can't automatically compute whether 0 < radius is true for you, but if you're lucky something like by norm_num or by linarith will work)

Kyle Miller (Nov 18 2022 at 17:38):

Here's an example:

import data.real.basic
import data.real.sqrt
import tactic

noncomputable theory

structure point :=
  (x y: ℝ)

structure circle :=
  (center: point) (radius: ℝ) (radius_pos : 0 < radius)

def circle.makenew (d e f: ℝ) (h : 0 < (d^2 + e^2)/4 - f) : circle :=
    circle.mk (point.mk (-d/2) (-e/2)) (real.sqrt ((d^2+e^2)/4-f)) (by rwa real.sqrt_pos)

def c2: circle := circle.makenew 10 10 1 (by linarith)

#norm_num [c2, circle.makenew] : c2.radius
-- real.sqrt 49

learnreal (Nov 18 2022 at 17:39):

Kyle Miller said:

(Lean can't automatically compute whether 0 < radius is true for you, but if you're lucky something like by norm_num or by linarith will work)

Got it. Learnt about norm_num in another thread. Separating proof vs compute looks very tricky to me. May be some thing fundamental that I am missing. But, got the basic idea to get some work progressing.

Kyle Miller (Nov 18 2022 at 17:39):

I modified circle.makenew to include a condition on the variables that guarantee the square root is positive.

Kyle Miller (Nov 18 2022 at 17:40):

Just to give another way to write it for sake of example:

def circle.makenew (d e f: ℝ) (h : f < (d^2 + e^2)/4) : circle :=
  circle.mk (point.mk (-d/2) (-e/2)) (real.sqrt ((d^2+e^2)/4-f)) (by { rw real.sqrt_pos, linarith })

learnreal (Nov 18 2022 at 17:41):

Cool. I like this much better (the condition h: ...). Thanks for this suggestion.

I actually got real.sqrt 49 with out rwa or linarith. May be just lucked out on this example.

learnreal (Nov 18 2022 at 17:44):

learnreal said:

Cool. I like this much better (the condition h: ...). Thanks for this suggestion.

I actually got real.sqrt 49 with out rwa or linarith (that was with out the h condition). May be just lucked out on this example.

Last updated: Dec 20 2023 at 11:08 UTC