Re: [isabelle] schematic variables



On Wed, 10 Aug 2011, Mamoun FILALI-AMINE wrote:

 After discussing with Sascha Boehme, it seems to be technically
 impossible to match a goal against a pattern after unfolding with
 some rewrite rule:

   definition "foo x = bar x x"

   ...

   have "foo (f x)" (is "foo ?X")       [pattern is possible]
     unfolding foo_def (is "bar ?X _")  [pattern is not possible]

Strictly speaking it is not *technically* impossible, merely outside the scope of the structured proof language of Isar. Structure emerges by restricting low-level technical operations to something that conforms to certain higher concepts. Take ML as programming language for example: it allows much less operations than machine language, and is thus far more powerful -- the compiler and runtime system can do smart things for you.

One of the key principles of Isar is the distinction of the proof text and the proof state. Information may flow only from text to state, not the other way round.


Anyway, your example reminds me of the Ltac tactic definition language of Coq, with matching against the goal state. After so many years, Isar still lacks a structured proof method definition language. You have to use plain ML for that (via the 'method_setup' command, which is not really difficult).

When drafting the first versions of the Isar proof language, I was aware of this omission of a method definition language. It made certain things easier, and the quality of proofs (readability and maintainability) has actually improved by making the language more restrictive.

Structured proof method definition languages are still an interesting area of research, but I see more potential for the future in sophisticated editing support of Isar text in the Prover IDE. (The current Isabelle/jEdit implementation is a very modest beginning in that direction.)


This can be illustrated by looking again at what Coq has to offer. Since I am myself located in France, I have the privilege to discuss with many Coq users first-hand. I see two main movements of power-users at the moment:

  (1) Hardcore Ltac scripting according Chlipala.
      (This reminds me a lot of a tactical style that was popular in
      Isabelle/HOL in the late 1990-ies, e.g. see HOL/Bali or
      HOL/Hoare_Parallel).

  (2) Quick in-place tactic composition via ssreflect, according to
      Gonthier.  His language assigns a meaning to almost every character
      in the ASCII set, to make typing as efficient as possible.  This
      wins more and more converts, and recent versions of Matita seem to
      have adopted it as well.

Instead of imitating any of the above, I would eventually like to see a Prover IDE that allows very quick proof composition, but producing proper Isar proof text instead of recording the keystrokes in the script. This would be analogous to a typical Java IDE: a relatively weak language (here Isar) is composed and maintained by relatively strong tooling.


	Makarius





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