Nuprl Lemma : Tactics for Constructive Geometry


All theorems of constructive geometry have the form
⌈∀e:EuclideanPlane. [prop]⌉

To prove a theorem like
  ⌈∀e:EuclideanPlane. ∀a,b:Point.  (P (a; b) ⇒ (∃c:Point. Q (a; b; c)))⌉
one typically starts with 
Auto and then "construct" the desired point c by instantiating
lemmas (that have already been proved to construct points)
or invoking the basic constructions.

To invove the construction that extends the segments AB by the segment CD,
use the tactic 
  Prolong ⌈A⌉ ⌈B⌉ `x' ⌈C⌉ ⌈D⌉
The points A, B, C, D will usually be variables (of type ⌈Point⌉) but
the can be expressions, too, so they are Nuprl terms 
(type control-o to get a ⌈[term]⌉ slot). The `x' is a ML variable.
It is used to name the new endpoint of the extended segment.

We have added "circle-circle-continutity" as a theorem
(it is unproved, so far, but does follow from the axioms, so it is safe
to use it in proofs). It lets you construct the intersection point(s) of
two cicles that overlap.
To invoke that use either  
  CircleCircle1 ⌈a⌉;⌈b⌉ ⌈c⌉ ⌈d⌉ `x'
 or
  CircleCircle2 ⌈a⌉;⌈b⌉ ⌈c⌉ ⌈d⌉ `x' `y'
(for more information about these, see: { circle-circle-tactics }).

"line-circle-continuity" is one of our axioms.
It lets you construct the intersection point(s) of a line and a circle
(that overlap).
Use 
   CircleLine1 ⌈a⌉;⌈b⌉ ⌈u⌉ ⌈v⌉ ⌈p⌉ `x'
 or
  CircleLine2 ⌈a⌉;⌈b⌉ ⌈u⌉ ⌈v⌉ ⌈p⌉ `x' `y'
(see { line-circle-tactics } for more information).

To construct the "crossing point" for segments ab and cd  (and name it x),
 use SegmentsCross ⌈a⌉ ⌈b⌉ ⌈c⌉ ⌈d⌉ `x'

 
 .

⋅

Latex:

All  theorems  of  constructive  geometry  have  the  form
\mkleeneopen{}\mforall{}e:EuclideanPlane.  [prop]\mkleeneclose{}

To  prove  a  theorem  like
    \mkleeneopen{}\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.    (P  (a;  b)  {}\mRightarrow{}  (\mexists{}c:Point.  Q  (a;  b;  c)))\mkleeneclose{}
one  typically  starts  with 
Auto  and  then  "construct"  the  desired  point  c  by  instantiating
lemmas  (that  have  already  been  proved  to  construct  points)
or  invoking  the  basic  constructions.

To  invove  the  construction  that  extends  the  segments  AB  by  the  segment  CD,
use  the  tactic 
    Prolong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}  `x'  \mkleeneopen{}C\mkleeneclose{}  \mkleeneopen{}D\mkleeneclose{}
The  points  A,  B,  C,  D  will  usually  be  variables  (of  type  \mkleeneopen{}Point\mkleeneclose{})  but
the  can  be  expressions,  too,  so  they  are  Nuprl  terms 
(type  control-o  to  get  a  \mkleeneopen{}[term]\mkleeneclose{}  slot).  The  `x'  is  a  ML  variable.
It  is  used  to  name  the  new  endpoint  of  the  extended  segment.

We  have  added  "circle-circle-continutity"  as  a  theorem
(it  is  unproved,  so  far,  but  does  follow  from  the  axioms,  so  it  is  safe
to  use  it  in  proofs).  It  lets  you  construct  the  intersection  point(s)  of
two  cicles  that  overlap.
To  invoke  that  use  either   
    CircleCircle1  \mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}d\mkleeneclose{}  `x'
  or
    CircleCircle2  \mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}d\mkleeneclose{}  `x'  `y'
(for  more  information  about  these,  see:  \{  circle-circle-tactics  \}).

"line-circle-continuity"  is  one  of  our  axioms.
It  lets  you  construct  the  intersection  point(s)  of  a  line  and  a  circle
(that  overlap).
Use 
      CircleLine1  \mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}u\mkleeneclose{}  \mkleeneopen{}v\mkleeneclose{}  \mkleeneopen{}p\mkleeneclose{}  `x'
  or
    CircleLine2  \mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}u\mkleeneclose{}  \mkleeneopen{}v\mkleeneclose{}  \mkleeneopen{}p\mkleeneclose{}  `x'  `y'
(see  \{  line-circle-tactics  \}  for  more  information).

To  construct  the  "crossing  point"  for  segments  ab  and  cd    (and  name  it  x),
  use  SegmentsCross  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}d\mkleeneclose{}  `x'

 
  .

\mcdot{}


Date html generated: 2015_07_17-PM-06_21_45
Last ObjectModification: 2015_07_17-PM-00_07_33

Home Index