Email Gateway (Aug 18 2022 at 12:02): Email Gateway (Aug 18 2022 at 12:02):From: Andrei Popescu <uuomul@yahoo.com>
Hello,
I have proved the consistency of specialized theorem prover
in Isabelle, but when I am trying to use it, I find serious problems
with "executing"/simplifying some functions that initally looked to me
very amenable to simplification.
Particularly, I have the following problems:
-- Isabelle won't simplify underneath existential quantifiers, and would loop
if I try to simplify after replacing the existentially quantified variables
with schematic variables (via existential introduction) or if try
to enforce an "under-exists" simplification rule
-- in cases when simplification does
what I wish (using auto
for some
trivial FOL
arrangements to help
simplification), it takes too much time (I think
auto tries to hard)
I have tried to capture these problems with the following small example,
where:
-- a term is either a basic term "Bas n" or a compound term "Cpd Ts";
-- a rule deduces terms (conclusions) from lists of terms (hypotheses);
-- there are only five rules: R1, R2, R1', R1'', R2';
-- the function mdr mathes a term against these rules constructing
backwards a proof subject to some constraints (that the term is the
conclusion of the rule and its immediate
subterms are less or equal to (le) the hypotheses of the rule -- I
have added this complication with "le" so that I do not have
unique proofs).
Here is the theory (I am also attaching it as a thy file):
datatype trm = Bas nat | Cpd "trm list"
record rule =
hyps :: "trm list"
cnc :: "trm"
constdefs
R1 :: "rule"
"R1 == (| hyps = [Bas 1, Cpd[Bas 2, Bas 3]],
cnc = Cpd [Bas 1, Cpd[Bas 2, Bas 3]] |)"
R2 :: "rule"
"R2 == (|hyps = [Bas 2, Cpd[Bas 3, Bas 4]],
cnc = Cpd [Bas 1, Cpd[Bas 2, Bas 3]] |)"
R1' :: "rule"
"R1' == (|hyps = [Bas 2, Bas 3],
cnc = Cpd [Bas 2, Bas 3] |)"
R1'' :: "rule"
"R1'' == (|hyps = [Bas 3, Bas 4],
cnc = Cpd [Bas 2, Bas 3] |)"
R2' :: "rule"
"R2' == (|hyps = [Bas 4, Bas 5],
cnc = Cpd [Bas 3, Bas 4] |)"
constdefs Rls :: "rule
set"
"Rls == {R1, R2, R1', R1'', R2'}"
consts le :: "trm => rm => bool"
axioms le_simps_Bas:
"ge (Bas n) T' = True"
axioms le_simps_Ind:
"le (Cpd Ts) T' =
(case T' of Bas n' => False
|Cpd Ts' => length Ts = length Ts' /\
(ALL i < length Ts. le (Ts!i) (Ts'!i)))"
lemmas le_simps = le_simps_Bas le_simps_Ind
declare le_simps [simp]
lemmas rules_defs = Rls_def R1_def R2_def R1'_def R1''_def R2'_def
declare rules_defs [simp]
consts mdr :: "trm => rule set"
axioms mdr_simps_Bas:
"mdr (Bas n) = {(| hyps = [Bas n], cnc = Bas n
|)}"
axioms mdr_simps_Cpd:
"mdr (Cpd Ts) =
{(|hyps = concat (map hyps drls),
cnc = Cpd Ts |)
|rl drls.
rl: Rls /\
cnc rl = Cpd Ts /\
length (hyps rl) = length Ts /\
length drls = length Ts /\
(ALL i < length Ts. le (Ts ! i) (hyps rl ! i) /\
drls!i : mdr (hyps rl ! i))}"
lemmas mdr_simps = mdr_simps_Bas mdr_simps_Cpd
declare mdr_simps [simp]
I would like to be able to execute mdr, so that I always obtain, for example,
instead
of "x : mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])", a disjunction of 6 facts
(according to the six
possible decompositions), where, for example, one of the dijuncts would be
"x = (| hyps = [Bas (Suc 0), Bas 2, Bas 3],
cnc = Cpd [Bas (Suc 0), Cpd [Bas 2, Bas 3]] |)"
In order to achieve this, I try to help the engine by adding the following simplification rules:
lemma help_map0[simp]:
"length xs = 0 ==> map f xs = []"
sorry
lemma help_map1[simp]:
"length xs = Suc n ==>
map f xs = map f (butlast xs) @ [f(xs ! n)]"
sorry
lemma help_butlast[simp]:
"i < length xs ==> butlast xs ! i = xs ! i"
sorry
lemma help_finite_pred[simp]:
"(ALL j < Suc n. phi j) = ((ALL j < n. phi j) /\ phi n)"
sorry
With these, auto is able to reduce a goal like
"mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]]) <= X"
to six goals having conclusions of the form "rl : X" for
each of the six elements rl of "mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])",
which is satisfactory, although the reduction is quite slow for this
small example already.
The above reduction is clearly safe, which would make me hope for the possibility of a dual reduction to a disjunction. However, if I place
"mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])" on a positive position
in a goal, as in "x : mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])",
I am not able to decompose the goal into a disjunction no matter how I try.
For instance, if I try (adding a seemingly useful distributive law)
lemma "x : mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])"
apply (auto simp add: conj_disj_distribR)
it will not apply the needed simplifications.
If I try (at the same lemma),
apply (auto simp add: conj_disj_distribR, rule exI, rule exI, auto)
it will loop,
and also if I add the further lemma
lemma simp_inside_EX:
"(!! x y. P x y = Q x y) ==> (EX x y. P x y) = (EX x y. Q x y)"
by blast
and then try
apply (auto simp add: conj_disj_distribR,
simp add: simp_inside_EX)
it will loop again.
So my question is: do I need to write my own rewrite engine/tactical, or
would a proper use of existing ones in Isabelle solve my problems regarding the
possibility of decomposition and its computational complexity ?
Many thanks in advance for any advice regarding this matter,
Andrei Popescu
miniTest.thy
Last updated: May 03 2024 at 04:19 UTC