Re: [isabelle] Implicitly referring to previous facts in the moreover-ultimately paradigm



On 23/03/18 14:19, Peter Lammich wrote:
> 
>> I don't see anything unnatural or unnecessary about it. On the
>> contrary
>> too much implicit fact management can make Isar proofs hard to read
>> and
>> hard to maintain, also hard to explain to casual readers who are not
>> familiar with the language.
> 
> In my opinion, it is indeed a bit strange that the moreover-ultimately
> construction chains the implicit facts (so they are available for your
> last proof) but you cannot name them.
> 
>     ultimately have "D" by (blast intro: foo)
> 
> which the more experienced Isabelle user might be tempted to write is
> not exactly clearer than
> 
>     using foo[OF ...] .
> 
> So we have a construct that provides some nice implicit fact management
> for the complicated cases, but not for the simpler cases, where a
> simple forward proof does work.

We are talking about the final step of a calculational proof here, i.e.
'finally' or 'ultimately'. The proof following that can be more than
just 'by', but there is no systematic way to refer to the chained facts
in a complex proof here.

This is not a problem of the calculation, but of what can be done with
"proof method ... qed method". I've once had something like this in the
pipeline:

  <chained facts>
  <goal>
  proof -
    case facts
    then show ?thesis sorry
  qed

I.e. the proof method "-" provides a case that "notes" the chained facts
for later use in the subproof. It did not emerge so far, because "notes"
cannot be part of proof method cases -- just by accident: it was not
required so far, and these things have some complexities internally.

Moreover, prospective applications for that have been too rare so far.
As a rule of thumb there need to be 2-3 good reasons to add more
features (read: complexity), not just half a reason. Alternatively, it
is possible to "trade" features: removing historic things that are not
really needed, and using the freed conceptual space to add new things.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.