Email Gateway (Aug 18 2022 at 18:10): Email Gateway (Aug 18 2022 at 18:10):From: Mamoun FILALI-AMINE <filali@irit.fr>
Hello,
I wonder if it is possible to instantiate schematic variables
after unfolding (see example below).
thanks
Mamoun
definition "ref P Q = (\<forall> s. P s \<longrightarrow> Q s)"
theorem
assumes r1: "ref A A'"
assumes r2: "ref B B'"
shows "ref (A \<union> B) (A' \<union> B')"
proof -
have "?thesis" unfolding ref_def (* is "\<forall> s. ?L s
\<longrightarrow> ?R s" *)
filali.vcf
Email Gateway (Aug 18 2022 at 18:10):From: Sascha Boehme <boehmes@in.tum.de>
Hello Mamoun,
Your example does not contain schematic variables after unfolding with
ref_def. Instead, the goal looks as follows:
\<forall>s. (A \<union> B) s \<longrightarrow> (A' \<union> B') s
The most common form to instantiate schematic variables in facts is
via the "of" attribute, for example as follows:
thm refl (* is "?t = ?t" *)
thm refl[of x] (* is "x = x" *)
This can also be applied to intermediate steps in a proof:
lemma "\<exists>n::nat. n \<ge> 0"
proof -
{
fix n :: nat
have "n \<ge> 0" by simp
}
(* we proved "?n \<ge> 0" *)
note this[of "1 :: nat"] (* is "1 \<ge> 0" *)
then show ?thesis ..
qed
A different form of this proof introduces schematic variables into the
goal, but in most cases it's best to let some tactic instantiate
these variables automatically:
lemma "\<exists>n::nat. n \<ge> 0"
apply (rule exI) (* the goal is now "?n \<ge> 0" *)
apply simp (* instantiates "?n" appropriately and solves the goal *)
done
Cheers,
Sascha
Mamoun FILALI-AMINE wrote:
Email Gateway (Aug 18 2022 at 18:11):From: Mamoun FILALI-AMINE <filali@irit.fr>
Hello,
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]
However, according to Sascha, most of the time proofs can be
restructured to avoid this need or Isabelle's proof methods (e.g.,
simp or auto) can collapse relevant proof steps such that these
patterns are not necessary.
Mamoun
filali.vcf
Email Gateway (Aug 18 2022 at 18:11):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 26 2024 at 20:16 UTC