Email Gateway (Aug 18 2022 at 13:03): Email Gateway (Aug 18 2022 at 13:03):From: Chris Capel <pdf23ds@gmail.com>
Isabelle is running for 30+ seconds when I try to apply (rule exI) in
the middle of my structured proof, eating memory at about 20 MB/sec. I
ran out of memory after that point. At first I thought it was
unification exploding but then I got rid of my function schematic
variable. Could this be a bug? (I'm running from rev
29862:17d1e32ef867, BTW. I can try updating if needed.)
The below theory ought to reproduce this.
Chris Capel
theory Lojban
imports Main
begin
datatype token =
Start nat -- {* nat is phrase id *}
| Trm nat bool -- {* phrase id, is elided *}
-- {* Allowable phrase to phrase relations *}
consts
mapPhPh :: "nat => nat set"
mapMem :: "nat => nat => bool" (infix ":*" 50)
mapNotMem :: "nat => nat => bool" (infix "~:*" 50)
translations
"a :* b" == "a : mapPhPh b"
"a ~:* b" == "a ~: mapPhPh b"
-- {* ({({ } _) _} ) *}
fun canAppend1 :: "token list => nat => bool" where
"canAppend1 ((Trm pid el)#xs) p = (~el | p ~:* pid & canAppend1 xs p)" |
"canAppend1 ((Start _ )#xs) p = True"
fun canAppend :: "token list => nat => nat => bool" where
"canAppend xs p outID = (p :* outID & canAppend1 (rev xs) p)"
primrec insert_list :: "'a list => nat => 'a list => 'a list" where
"insert_list list 0 outer = list @ outer" |
"insert_list list (Suc n) os = (hd os) # (insert_list list n (tl os))"
fun rmTrm where
"rmTrm lst = filter (% y. case y of Trm _ _ => False | _ => True) lst"
inductive_set P :: "token list set" where
base: "[Start tid, Trm tid el] : P" |
beside: "[| base : P; take 2 (drop pos base) = [Trm aID el1, Trm oID el2];
canAppend ((take pos base) @ [Trm aID el1]) newID oID |]
==> insert_list [Start newID, Trm newID elided]
(Suc pos) base
: P" |
inside: "[| base : P; 0 < pos;
take 2 (drop (pos - 1) base) = [Start oldID, Trm oldID oldEl];
rmTrm (drop pos base) = [];
newID :* oldID |]
==> insert_list [Start newID, Trm newID elided] pos base : P"
datatype 'tok prod =
PTrm 'tok
| Prod "nat list list"
primrec powerlist :: "'a list => 'a list list" where
"powerlist [] = []" |
"powerlist (x # xs) = (x # xs) # powerlist xs"
function
parse_len :: "'tok prod list => 'tok prod => 'tok list => int" where
"parse_len gr (PTrm tok) toks = (if ((hd toks) = tok) then 1 else -1)"
| "parse_len gr (Prod pl) toks =
last (sort (map (%p. foldl (% (len::int) (p, l).
if len = -1 then -1
else len + parse_len gr (gr!p) l)
0 (zip p (powerlist toks)))
pl))"
by pat_completeness auto
fun getPhMap :: "(nat * nat) list => nat => nat set" where
"getPhMap ls x = set (map snd (filter (%y. (fst y) = x) ls))"
fun rm_elided :: "token list => token list" where
"rm_elided st = filter (%s. case s of Start _ => True | Trm _ el => ~el) st"
lemma assumes "st : P" and "mapt ~= []" and "mapPhPh = getPhMap mapt"
shows "EX gr X Y. parse_len_dom (gr, gr!0, (rm_elided st)) -->
(nat (parse_len gr (gr!0) (rm_elided st)) = length (rm_elided st))
& size gr < X * length (rm_elided st) * length mapt
+ Y * length (rm_elided st)"
(is "EX gr. ?LinGr gr")
using assms(1) proof (induct st rule: P.induct)
fix gr tid el
have "?LinGr [Prod [[1, 2]], PTrm (Start tid), PTrm (Trm tid el)]"
sorry
-- {* hence "EX gr. ?LinGr gr" ..*}
thus "EX gr X Y.
parse_len_dom (gr, gr ! 0, rm_elided [Start tid, Trm tid el]) -->
nat (parse_len gr (gr ! 0) (rm_elided [Start tid, Trm tid el])) =
length (rm_elided [Start tid, Trm tid el]) &
length gr
< X * length (rm_elided [Start tid, Trm tid el]) * length mapt +
Y * length (rm_elided [Start tid, Trm tid el])" apply (rule exI)
qed
Email Gateway (Aug 18 2022 at 13:03):From: Lawrence Paulson <lp15@cam.ac.uk>
The inclusion of the previous result (by your use of "thus" rather
than "show") seems to be part of the problem, though I am not sure why.
Another part of your problem is that the previous result does not
appear to match up with the new result that you want to prove. Higher-
order unification can get out of control quite quickly when you have a
big search space but no solutions.
I was able to make some progress with the following fragment:
have l: "?LinGr [Prod [[1, 2]], PTrm (Start tid), PTrm (Trm tid el)]"
sorry
-- {* hence "EX gr. ?LinGr gr" ..*}
have "EX gr X Y.
parse_len_dom (gr, gr ! 0, rm_elided st) -->
nat (parse_len gr (gr ! 0) (rm_elided st)) =
length (rm_elided st) &
length gr
< X * length (rm_elided st) * length mapt +
Y * length (rm_elided st)"
by (rule exI, rule l)
The previous result is now labelled l. We no longer include it in the
next proof (no "from"). I have corrected the statement to be proved so
that it matches. Now the proof is instantaneous. Alternatively, you
can include the previous result and prove the next one using blast
with no arguments.
So the problem appears to be the interaction between the rule method
and piped in facts.
Larry Paulson
Last updated: May 03 2024 at 08:18 UTC