In my last post I should have said instead that HOL programmers have very good
concrete down-to-earth adjoint functors skills, which pure mathematicians tend
to have good theoretical adjoint functors skills, and maybe interfaces that
hides the adjoint functors calculations are good.
Today I'd argue that mathematicians trying to use HOL may need to improve their
concrete down-to-earth FOL skills. I'd like to improve mine, and I've started
using TAUT and theorems like DE_MORGAN_THM as a way to improve my FOL skills.
I'll give an example below where I successfully generalized this short proof
from Multivariate/topology.ml
let CLOSURE_INTERIOR = prove
(`!s:real^N->bool. closure s = UNIV DIFF (interior (UNIV DIFF s))`,
REWRITE_TAC[EXTENSION; closure; IN_UNION; IN_DIFF; IN_UNIV; interior;
IN_ELIM_THM; limit_point_of; SUBSET] THEN
MESON_TAC[]);;
First, let me give an example where my FOL skills were poor enough to cause me
trouble. I was trying to prove a simple topology result and I ended up with
this goal (rewritten with math characters for clarity):
0 [`s ⊂ topspace α`] (H1)
`x ∈ s ∨
x ∈ topspace α ∧
(∀t. x ∈ t ∧ open_in α t ⇒ (∃y. ¬(y = x) ∧ y ∈ s ∧ y ∈ t)) ⇔
x ∈ topspace α ∧
(∀t. x ∈ t ∧ open_in α t ⇒ (∃y. y ∈ s ∧ y ∈ t))`
I didn't know how to prove this, but I thought it was obvious, and I think it
would be obvious even if you don't know what topspace or open_in means. I just
happened to try MESON_TAC using the theorem SUBSET and the assumption H1, and
it worked. I was really surprised, and it took me a while to figure out why it
worked. But the answer is simple FOL. There's a tautology
∀a b c H. (H ∧ a ⇒ c) ∧ (b ⇒ c) ∧ (c ∧ ¬a ⇒ b) ⇒
H ⇒ (a ∨ b ⇔ c)
which you can see by
TAUT `!a b c H. (H /\ a ==> c) /\ (b ==> c) /\ (c /\ ~a ==> b) ==>
H ==> (a \/ b <=> c)`;;
and MESON_TAC can easily prove the three antecedents using SUBSET:
s ⊂ topspace α ∧ x ∈ s ⇒ x ∈ topspace α
x ∈ s ⇒ ∀t. x ∈ t ∧ open_in α t ⇒ (∃y. y ∈ s ∧ y ∈ t)
(∀t. x ∈ t ∧ open_in α t ⇒ (∃y. y ∈ s ∧ y ∈ t)) ∧ ¬(x ∈ s) ⇒
(∀t. x ∈ t ∧ open_in α t ⇒ (∃y. ¬(y = x) ∧ y ∈ s ∧ y ∈ t))
The first is the only one that uses SUBSET. For the second, just take y = x.
For the third,
¬(y = x) follows from ¬(x ∈ s) and y ∈ s.
I think good HOL programmers make such FOL deductions very quickly, perhaps
even subconsciously, but it was hard for me, and maybe that's because
mathematicians often "know things are obvious" without straightening out the
actual FOL thinking required. BTW here's the entire proof:
needs "RichterHilbertAxiomGeometry/Topology.ml";;
let IN_Closure = theorem `;
∀α s x. s ⊂ topspace α ⇒
(x ∈ Closure α s ⇔ x ∈ topspace α ∧
∀t. x ∈ t ∧ open_in α t ⇒ ∃y. y ∈ s ∧ y ∈ t)
proof
intro_TAC ∀α s x, H1;
simplify H1 Closure_DEF IN_UNION IN_LimitPointOf;
fol H1 SUBSET;
qed;
`;;
Let's turn to CLOSURE_INTERIOR, where I used TAUT etc. to predict the right
answer instead of just throwing HOL at the problem until it went away. After
some obvious preliminaries including a SIMP_TAC I ended up with the goal
0 [`s ⊂ topspace α`] (H1)
1 [`topspace α ━ s ⊂ topspace α`]
`∀x. x ∈ topspace α ∧
(∀t. x ∈ t ∧ open_in α t ⇒ (∃y. y ∈ s ∧ y ∈ t)) ⇔
x ∈ topspace α ∧
¬(∃t. open_in α t ∧ x ∈ t ∧ t ⊂ topspace α ━ s)`
Now I know this is easy, but my FOL isn't good enough to see how to prove it,
so I successively added TAUT/FOL things to the SIMP_TAC list
NOT_EXISTS_THM SUBSET DE_MORGAN_THM NOT_FORALL_THM
TAUT [∀a b c. ¬a ∨ ¬b ∨ c ⇔ b ∧ a ⇒ c]
TAUT [∀a b c. ¬(a ⇒ b ∧ ¬c) ⇔ c ∧ a ∨ ¬(a ⇒ b)]
and now have a goal that looks a lot more provable to me:
0 [`s ⊂ topspace α`] (H1)
1 [`topspace α ━ s ⊂ topspace α`]
`∀x. x ∈ topspace α ∧
(∀t. x ∈ t ∧ open_in α t ⇒ (∃y. y ∈ s ∧ y ∈ t)) ⇔
x ∈ topspace α ∧
(∀t. x ∈ t ∧ open_in α t
⇒ (∃x. x ∈ s ∧ x ∈ t ∨ ¬(x ∈ t ⇒ x ∈ topspace α)))`
The two sides of the biconditional are almost identical now, and the statement
x ∈ t ⇒ x ∈ topspace α
follows from open_in α t because of the theorem
OPEN_IN_SUBSET;;
val it : thm = |- ∀α s. open_in α s ⇒ s ⊂ topspace α
which of course will require SUBSET, so I think that MESON_TAC should prove the
goal together with OPEN_IN_SUBSET and SUBSET, and it does. But now I find I
can cut from the proof the assumption
topspace α ━ s ⊂ topspace α
and all of my TAUT/FOL crutches, and here's the short version:
let ClosureInterior = theorem `;
∀α s. s ⊂ topspace α ⇒
Closure α s = topspace α ━ (interior_in α (topspace α ━ s))
proof
intro_TAC ∀α s, H1;
simplify H1 EXTENSION IN_Closure IN_DIFF IN_interior_in SUBSET;
fol OPEN_IN_SUBSET SUBSET;
qed;
`;;
This is almost as short as John's CLOSURE_INTERIOR above, but I bet John saw
his proof right away, and didn't need my TAUT/FOL crutches. Maybe after enough
FOL practice, I won't need the crutches either.
--
Best,
Bill
------------------------------------------------------------------------------
CenturyLink Cloud: The Leader in Enterprise Cloud Services.
Learn Why More Businesses Are Choosing CenturyLink Cloud For
Critical Workloads, Development Environments & Everything In Between.
Get a Quote or Start a Free Trial Today.
http://pubads.g.doubleclick.net/gampad/clk?id=119420431&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
