Email Gateway (Aug 18 2022 at 12:02): Email Gateway (Aug 18 2022 at 12:02):From: Denis Bueno <dbueno@gmail.com>
[The following is all in context of the LList2 library, available from afp.]
During the course of a proof I attempt to ensure that a finite llist
does not have any of a certain element. After many unsuccessful
attempts at actual pattern matching using LNil and LCons (using fun
and primrec) I finally saw the definition of llength in LList2.thy:
constdefs
llength :: "'a llist => nat"
"llength == finlsts_rec 0 (λ a r n. Suc n)"
This uses the completely opaque (to me) `finlsts_rec' operator. I
gather the following from its uses:
- 0 is the base case; if the list is LNil, 0 is returned
- a is the current element of the list
- r is the rest of the list
- n is the current "accumulator state"
- it has some special magic for telling Isabelle it will only deal
with finite llists
These observations lead me to the following definition, `noBot'
(mnemonic: "no bottom state"):
constdefs
noBot :: "state llist => bool"
"noBot == finlsts_rec True (% s r b. b & (s ~= BottomState))"
As a sanity check, I try to prove that "noBot LNil = True":
lemma
"noBot LNil = True" unfolding noBot_def using finlsts_rec_LNil
(here) by blast
When ProofGeneral has consumed everything up to "(here)", the
proofstate looks like:
using this:
finlsts_rec ?c ?d LNil = ?c
goal (1 subgoal):
1. finlsts_rec True (%s r b. b & s ~= BottomState) LNil = True
This looks like it can be proved directly by unification. Consuming
the blast does not prove the theorem, even after a long time.
What exactly is going on here?
Email Gateway (Aug 18 2022 at 12:02):From: Lawrence Paulson <lp15@cam.ac.uk>
Blast doesn't look like the right tool for this problem.
You can prove it like this:
lemma
"noBot LNil = True" unfolding noBot_def
by (simp add: finlsts_rec_LNil)
Larry Paulson
Email Gateway (Aug 18 2022 at 12:02):From: Denis Bueno <dbueno@gmail.com>
I had the same thought, but I tried:
lemma
"noBot LNil = True" unfolding noBot_def
using finlsts_rec_LNil
by simp
And it failed. I expected to be able to substitute "using" in Isar
for the "add:" argument to simp. What is different?
Email Gateway (Aug 18 2022 at 12:02):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Denis,
That is, in general, not the case. Facts chained in to simp (e.g. using
"using") are not instantiated wrt. to types, where simp rules given to
simp with add: are.
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 12:02):From: Makarius <makarius@sketis.net>
Automated proof methods like "simp" merely insert the facts being "used"
into the goal before doing their usual business. This means a polymorphic
rule like using finlsts_rec_LNil essentially looses its polymorphism, it
can be instantiated at most once for logical reasons, and the Simplifier
does not instantiate even do that, but ignores it due to schematic type
variables in the goal premises.
In contrast, the "add" method modifier inserts the rule into the
Simplifier context as an independented fact. It is eventually matched
against a redex in the goal, and its types get instantiated as expected.
As a rule of thumb (and a matter of style), the "using" part typically
refers to local things from the very proof, while rules from the library
are specified via extra method modifiers (simp add/del, blast
intro/elim/dest etc.).
Makarius
Last updated: May 03 2024 at 12:27 UTC