kdrag.theories.real.geometry
Module Attributes
line = define( |
|
@PTheorem(ForAll(p, p != origin, is_dir(dir(p)))) def unit_dir(l): p = l.fix() l.intros() l.unfold(is_dir) l.exists(vec2.smul(1 / vec2.norm(p), p)) l.unfold(vec2.norm) |
|
@PTheorem(ForAll(p, p != origin, is_dir(dir(p)))) def unit_dir(l): p = l.fix() l.intros() l.unfold(is_dir) l.exists(vec2.smul(1 / vec2.norm(p), p)) l.unfold(vec2.norm) |
- kdrag.theories.real.geometry.is_point = is_point
- line = define(
“line”, [x, y, z], Lambda(
[p], p.x * x + p.y * y + z == 0,
),
)
- kdrag.theories.real.geometry.unit = f!1881
@PTheorem(ForAll(p, p != origin, is_dir(dir(p)))) def unit_dir(l):
p = l.fix() l.intros() l.unfold(is_dir) l.exists(vec2.smul(1 / vec2.norm(p), p)) l.unfold(vec2.norm)
l.have(vec2.norm2(p) != 0, by=[vec2.norm2_zero]) l.have(vec2.norm2(p) > 0, by=[vec2.norm2_pos]) l.have(real.sqrt(vec2.norm2(p)) != 0, by=[real.sqrt_define(vec2.norm2(p))]) l.have(vec2.norm2(p) == vec2.dot(p, p), by=[vec2.norm2.defn]) l.split() l.auto(by=[vec2.dot.defn, vec2.smul.defn])
l.unfold(vec2.norm2, vec2.smul, vec2.dot) l.unfold(vec2.dot) l.simp() l.have(
real.sqrt(p.x * p.x + p.y * p.y) ** 2 == p.x * p.x + p.y * p.y, by=[real.sqrt_square(p.x * p.x + p.y * p.y)],
) l.auto() # l.have(is_dir(dir(p))
- kdrag.theories.real.geometry.unit_defn = |= ForAll(A!1879, is_dir(A!1879) == And(f!1881(A!1879) != Vec2(ToReal(0), ToReal(0)), Vec2.norm2(f!1881(A!1879)) == 1, dir(f!1881(A!1879)) == A!1879))
@PTheorem(ForAll(p, p != origin, is_dir(dir(p)))) def unit_dir(l):
p = l.fix() l.intros() l.unfold(is_dir) l.exists(vec2.smul(1 / vec2.norm(p), p)) l.unfold(vec2.norm)
l.have(vec2.norm2(p) != 0, by=[vec2.norm2_zero]) l.have(vec2.norm2(p) > 0, by=[vec2.norm2_pos]) l.have(real.sqrt(vec2.norm2(p)) != 0, by=[real.sqrt_define(vec2.norm2(p))]) l.have(vec2.norm2(p) == vec2.dot(p, p), by=[vec2.norm2.defn]) l.split() l.auto(by=[vec2.dot.defn, vec2.smul.defn])
l.unfold(vec2.norm2, vec2.smul, vec2.dot) l.unfold(vec2.dot) l.simp() l.have(
real.sqrt(p.x * p.x + p.y * p.y) ** 2 == p.x * p.x + p.y * p.y, by=[real.sqrt_square(p.x * p.x + p.y * p.y)],
) l.auto() # l.have(is_dir(dir(p))
- Parameters:
args (smt.ExprRef | Proof)