Idea: `given` methods and `proven` proofs

[pigworker]

I'm writing to suggest two ideas, modulo bikeshedding, and a possible interaction between them.

1 the given method

At the moment, you can say

prove p -> p by ImpI

and leave ask to check that the subgoal is given, but there is no successful way to be explicit about it, i.e., if you write

prove p -> p by ImpI where
  given p prove p ?

In fact, we could add the rule prove p by Assumption where prove p ? and then users could make an explicit

prove p -> p by ImpI where
  given p prove p by Assumption

leaving the subgoal to be solved implicitly as before. But that's egregious, because it would lead to

prove p -> p by Assumption where
  prove p -> p ?

in situations where the goal is not given. For this reason, I propose to create a new method, given, which succeeds only if the goal really is given. This would allow the user to choose to document

prove p -> p by ImpI where
  given p prove p given

Note that ask checks which subgoals are discharged by subproofs before either declaring unused subproofs to be surplus or checking whether uncovered subgoals are actually obvious. So, as things stand, given p prove p given would neither be inserted nor removed by ask.

2 the proven proof

At the cost of a keyword (beloved of the Scots legal system), I propose that we allow prove to be replaced by proven when all subgoals have hereditarily been discharged. I moreover propose that ask acknowledge completion of goals and subgoals by making this substitution, amounting to a more explicit acknowledgement of achievement than "no comment". If the user writes proven but ask discovers open subgoals, then proven reverts to prove.

So, if we submit

prove p & q -> q & p by ImpI where
  given p & q prove q & p from q & p where
    given p, q prove q & p by AndI

we obtain

proven p & q -> q & p by ImpI where
  given p & q proven q & p from q & p where
    given p, q proven q & p by AndI

but if we submit

proven p & q -> q & p by ImpI where
  given p & q proven q & p by AndI

we get the corrective reminder

prove p & q -> q & p by ImpI where
  given p & q prove q & p by AndI
    prove q ?
    prove p ?

and replacing the first ? with from p & q then yields

prove p & q -> q & p by ImpI where
  given p & q prove q & p by AndI
    proven q from p & q
    prove p ?

telling us we've made at least some progress.

3 prove versus proven and the insertion of givens

This is a bit of a subtle idea, and I'm not sure whether I like it. Perhaps, when ask gets this

prove p & q -> q & p by ImpI where
  given p & q prove q & p from p & q where
    given p, q prove q & p by AndI

the response should be

proven p & q -> q & p by ImpI where
  given p & q proven q & p from p & q where
    given p, q proven q & p by AndI
      proven q given
      proven p given

That is, if we start from a prove with no subproofs, ask inserts completed subproofs for the givens (except for the h in from h, which we usually expect to be given). However, if the user then deletes those givens and sends

proven p & q -> q & p by ImpI where
  given p & q proven q & p from p & q where
    given p, q proven q & p by AndI

then the proof is returned unaltered, because the head was a proven, not a prove.

If a prove is submitted with some existing subproofs, then missing proven ... givens are not inserted, as that implies the user has already chosen which subproofs to see. Meanwhile, if the user does not want proven ... givens are not inserted in a prove with no subgoals, they should jolly well write proven instead.

What to do?

1 and 2 are independent of each other. 3 requires both 1 and 2, but is entirely optional. Open to alternative syntactic choices.

[fredrikNordvallForsberg]

Let me just quickly add in my support for 2. No feedback that my proof was really finished was indeed one thing that made me unsure when briefly playing around earlier today.

[pigworker]

Latest update. The given method is now implemented. I'm working on proven while rebuilding the prettyprinter with a tighter grip on whitespace. One annoyance is that if someone is silly enough to do

prove a & b by AndI where prove a ?
                          prove b ?

then solving the subgoals will make the main goal proven, necessitating a repair in the indentation. Options:

• Suck it up, detect the where-horizontal, rejig the whitespace.
• Ban the where-horizontal.
• Choose a 5 letter word to replace "proven", e.g. "happy" or "known" or "yaldi" or what?

Meanwhile, the question of whether proven-givens (also proven-from-Falses, proven-by-TrueIs) should be automatically inserted in empty prove-wheres but not in nonempty prove-wheres or provens, is really a tension between informative verbosity for beginners and clutter for the more advanced. If we do it, it should only be as an opt-in "beginner mode".

[pigworker]

1 & 2 have happened. 3 could still happen, but it seems like its at a priority below the threshold of action. So I'm closing this issue.