RFE for ghilbert spec: Permute hypotheses when applying a theorem

[GoogleCodeExporter]

Oftentimes I am in the middle of a proof and want to apply a theorem with two 
or more hypotheses (an inference).  However, about half the time, it turns out 
that I have the hypotheses on the stack in the wrong order.  (For example, I 
first prove "(-> ph ps)" and then prove "ph", and want to apply "ax-mp".)  This 
is harmful to my proving "flow" for two reasons:

1) when I use the "unified" tab in the javascript proof editor, it can't find 
the theorem I want.  This makes me second-guess my stack and start wondering if 
either (a) something doesn't match up the way I think it does, or (b) the 
theorem I'm looking for actually isn't in prop.ghi.  

2) when I finally find the theorem I'm looking for, and discover that I need to 
rearrange my stack, it's hard to actually do.  I need to cut and paste some 
section of my proof text, but for a complicated proof it's not at all easy to 
find what to cut and where to paste it.

Therefore I suggest the following enhancement to the ghilbert spec.  When 
applying a theorem, allow an optional prermutation to apply to its hypotheses 
before matching them against the stack.  The syntax would be an optional list, 
which must include the numbers 1 to n, where n is the number of hypotheses of 
the next proof step.  If the list is missing, the intentity permutation (1 2 3 
... n) is used; this makes the change backwards-compatible to existing ghilbert 
proofs.

Here's an example of the new syntax:
thm (id2 () () (-> ph ph)
# Prove (-> (...) (-> ph ph))
  ph (-> ps ph) ax-1
  ph (-> ps ph) ph ax-2
  ax-mp

# Prove the antecedent
  ph ps ax-1

# Detach
  (2 1) ax-mp
)

For exporting a proof back to metamath (or earlier versions of ghilbert), it 
should be a simple matter to rearrange the proof stanzas to put the stack in 
the correct order.

I think this would also make many proofs more readable.  I often find myself 
writing comments like "# This isn't important right now, but I have to tuck it 
away on the stack for later."

If you think this is a good idea, let me know, and I will be happy to try 
implementing it.

Original issue reported on code.google.com by abliss on 10 Aug 2010 at 4:24

[GoogleCodeExporter]

Hi Adam,

One thing I'm in favor of is allowing assertions with numbers
of conclusions different from one. This is easy to implement,
I've done it in other ghilbert versions.  One can then make
simple 'structural' theorems like

thm (swap () (1 ph 2 ps) (ps ph)
  2 1
)

or any other desired permutation, without introducing any
significant new syntax.  Besides permutation, this is sometimes
useful for other purposes such as

thm (both () (1 (/\ ph ps)) (ph ps)
   1 pm3.26i
   1 pm3.27i
)

or, having used a theorem that provides more than one conclusion
when one doesn't need the last one

thm (drop () (1 ph) ()
)

I agree that having to rearrange the order of presentation of a proof
just to get the hypotheses in order to match an existing theorem is
inconvenient, and providing multiple versions of a theorem with permuted
hypotheses is also inconvenient and further doesn't scale.

- Dan

Original comment by [email protected] on 10 Aug 2010 at 5:56

[GoogleCodeExporter]

Oh, and one other: if as part of a proof one proves an expression and
needs to use that expression more than once in the proof -- surprisingly
uncommon but it happens sometimes -- the following is useful, in
conjunction with permuter theorems:

thm (dup () (1 ph) (ph ph)
  1 1
)

Original comment by [email protected] on 10 Aug 2010 at 6:06