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