On Mon, Jul 22, 2019 at 7:13 AM vvs <[email protected]> wrote:
> Writing tactic for a specific theorem seems too cumbersome if I could just
> do it directly.
>
That depends on the tactic, and the theorem. The point of tactics is that
they automate proof writing, and the reason the tactic language is
commingled with the definitions and proofs is because some tactics are
domain specific. For example, the arithmetic algorithm relies on the
definition of +, decimal numbers and so on, and a set of theorems used as
building blocks. I have been burned before trying to separate the two,
because development of the tactic may require changes to the theorems and
vice versa, and the result is a maintenance headache. (Consider the recent
mmj2 breakage caused by renaming "set" to "setvar". If the definition
checker was inline with set.mm that wouldn't have happened.)
> In ideal world one should simply point to one of the options and apply it
> to the theorem in question to get a feedback, then either proceed to
> another iteration or undo and return to a previous state. Also, visual
> clues are very important. I can't see too much if my workspace is cluttered
> with irrelevant information. In fact I might want to concentrate on
> different parts at different times, e.g. I can select different premises
> and conclusions to apply deduction rules or unification. I've tried this in
> mmj2 and found that there is not much feedback, but unification and
> derivation features were most useful.
>
In MM1 the primary interaction mode is just using a "refine" proof
(automatically called if you give a quoted lisp expression as the proof,
like all the current proofs in peano.mm1). Here's a real interaction
session I just had with MM1 for proving the equivalence relation theorems
for class equality:
theorem eqsid: $ A == A $ =
'_;
^ |- A == A
'(ax_gen _);
^ |- ?a e. A <-> ?a e. A
'(!! ax_gen x _);
^ |- x e. A <-> x e. A
'(!! ax_gen x biid);
theorem eqscom: $ A == B -> B == A $ =
'(alimi _);
^ |- (?a e. A <-> ?a e. B) -> (?a e. B <-> ?a e. A)
'(!! x alimi _);
^ |- (x e. A <-> x e. B) -> (x e. B <-> x e. A)
'(!! x alimi bicom);
theorem eqstr: $ A == B -> B == C -> A == C $ =
'(syl _ ax_6);
^^^^ failed to unify: ?b -> ?c =?= E. ?e ?e = ?d
'(syl _ ax_4);
^ |- A == B -> A. ?a ((?a e. B <-> ?a e. C) -> (?a e. A <-> ?a e. C))
'(syl _ (!! ax_4 x));
^ |- A == B -> A. x ((x e. B <-> x e. C) -> (x e. A <-> x e. C))
'(syl (alimi _) (!! ax_4 x));
^ |- (x e. A <-> x e. B) -> (x e. B <-> x e. C) -> (x e. A <->
x e. C)
'(syl (!! alimi x _) ax_4);
^ |- (x e. A <-> x e. B) -> (x e. B <-> x e. C) -> (x e.
A <-> x e. C)
'(syl (!! alimi x eqtr) ax_4);
^^^ failed to unify:
A == B -> B == C -> A == C
=?=
A. x ?f = ?g -> A. x ?g = ?h -> A. x ?f = ?h
'(syl (!! alimi x bitr) ax_4);
I would argue that the number of characters I have to type here is about
the same as you would get with an mmj2 proof, but because the computer
isn't constantly rewriting the text area I have more control and don't have
to move the cursor all around the place.
(By the way, did you notice the automatic definition unfolding? Sweet!)
> This is not always a valid move, for instance if the lisp program also has
>> some side effects like adding new definitions and so on, but I imagine that
>> many tactics will fit this mode of operation, and as long as the user is in
>> the driver's seat here they can choose to use it only when it is applicable.
>>
>
> Exactly. I find it inconvenient when the system is doing something
> unexpected and I want to examine it first and then make a decision myself.
>
This is also an advantage of having a complete record of your interaction
on the page so you can edit it as desired.
PS: mm0-hs now supports hover (show me the statement of the theorem) and go
to definition.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSuZZCRCLffX218NZdMkuYa9epnz%2ByJfevhSaWP2%2BUT_2w%40mail.gmail.com.
