Email Gateway (Aug 22 2022 at 17:29): Email Gateway (Aug 22 2022 at 17:29):From: Joshua Chen <joshua.chen@uni-bonn.de>
Dear Eisbach/Isabelle/ML experts,
I have a repetitive structured proof whose functionality I
would like to encapsulate as a method.
For example:
notepad begin
assume *: "Πx:A. Πy: B x. Πz: C x y. D x y
z : U"
have 0: "A : U" using * by rule
-- {* "B: A -> U" abbreviates "!!x. x : A ==> B x : U" *}
have 1: "B: A -> U"
proof -
fix x assume "x : A"
with * have **: "Πy: B x. Πz: C x y. D x y z
: U" by rule
then show "B x : U" by rule
qed
have 2: "!!x. x : A ==> C x : B x -> U"
proof -
fix x assume "x : A"
with * have **: "Πy: B x. Πz: C x y. D x y z
: U" by rule
fix y assume "y : B x"
with ** have "Πz: C x y. D x y z : U" by rule
then show "C x y : U" by rule
qed
have 3: "!!x y. [| x : A; y : B x |] ==> D x y : C x y ->
U"
proof -
fix x assume "x : A"
with * have **: "Πy: B x. Πz: C x y. D x y z
: U" by rule
fix y assume "y : B x"
with ** have "Πz: C x y. D x y z : U" by rule
then show "D x y: C x y -> U" by rule
qed
end
In the above proofs, "rule" is applying one or the other
of two rules previously declared as [elim]:
Prod_form_cond1 [elim]: "!!A B. (Πx:A. B x : U) ==> A
: U"
Prod_form_cond2 [elim]: "!!A B. (Πx:A. B x : U) ==>
B: A -> U"
Given "Πx:T. S x : U", the basic proof pattern is
then:
Fix x, assume "x : T", and derive either "T: U" or "S x :
U" by rule. Recurse, essentially performing a
breadth-first search over a binary tree.
I have tried and failed at automating this proof with
Eisbach, my difficulty is in getting it to perform the
"fix...assume" steps to instantiate a "scope" for the
variable and introduce the typing assumption.
Is there any method that emulates this? If not, how does
one go about implementing such functionality in an
Isabelle/ML tactic?
Thanks very much! :)
Email Gateway (Aug 22 2022 at 17:40):From: Thomas.Sewell@data61.csiro.au
There's some confusion here, I think.
Eisbach is, to my understanding, mostly for scripting what can
be done at the method level (e.g. inside an apply (...)) step
rather than what can be done in a structured proof document
(e.g. the fix, assume statements of these proofs). So your
first step would be to "compress" these structured proofs
into unstructured ones.
Re-reading the end of your message, I think it's pretty simple.
You can apply your 'elim' rules in unstructured style as
destruction rules, e.g. apply (drule Prod_form_cond1).
Isabelle natively supports backtracking with ',', so the
below might just work.
method try_solve = (assumption | (drule Prod_form_cond1 Prod_form_cond2, try_solve))
I didn't actually test that though, try playing around with
similar things.
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 17:46):From: Joshua Chen <joshua.chen@uni-bonn.de>
Thanks Thomas,
I had indeed already tried what you suggest, using 'rule'
with the 'OF' attribute to pick up assumptions along the
way (as 'drule' doesn't do what I need it to in this
case).
This unguided search through assumptions resulted in
unifier mismatches, hence my wondering if there was a way
to direct the method to use particular assumptions.
In the end I wrapped up the problematic steps in the 'try'
method provided by Eisbach_Tools and now my method works
exactly as intended :)
Best wishes,
Josh
Last updated: Apr 27 2024 at 01:05 UTC