Re: [isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE



On 12/16/2013 10:25 AM, Makarius wrote:
The particular problem above is "blast" failing repeatedly in a rather noise way....

I now have a practical example that causes the PIDE to go off and not come back, which is because of auto, blast, and declare commands.

declare[[show_sorts=true]]
lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False"
apply(auto)
oops

I haven't completely figured it out, but it seems "declare[[show_sorts=true]]" puts it over the edge. With it "false", Isabelle2013-2.exe will jump up to about 50% of the CPU, but recover. With it "true", after "auto" runs long enough, the PIDE becomes unresponsive, and it can't recover. It may not be particular to "show_sorts".

Using "apply blast" creates a bunch of messages, but it still proves the theorem, so it's the interaction between auto and blast.

I suppose it's just more of the same. I attach and include a theory with variations that work or don't work.

...You can try something like this:

theorem "(!!P. P::bool) ==> PROP P" by blast

e.g. with "isabelle tty" on the Terminal.

I tried the theorem in tty mode. It goes into a loop after getting to 6: "PROOF FAILED for depth 6". If you're telling me that blast will prove "(!!P. P::bool) ==> PROP P", that would be important to know.

Regarding that other list, I use Sourcetree on Windows for github.com. It's easy to install and use, and has way more features than the GitHub Windows application. It allows me to keep from having to know much.

I do my part as an imaginary power-user, a logical cult-of-one, peering out from the curtains of my compound, waiting for the NSA and that ex-KGB agent, Vladimir Putin, to arrive at any moment.

Regards,
GB




(****************************************************************************************)
theory i131214a__isaU_Trueprop_False_meta_eq_auto_hangs_PIDE
imports Complex_Main
begin

declare[[show_sorts=true]]
declare[[show_brackets=true]]
declare[[show_question_marks=true]]
notation Trueprop ("_∷⇩T" [1000] 1000)

(*With "Auto Methods" off, auto goes off and doesn't come back, if it's allowed
to run very long.*)

lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(rule equal_intr_rule)
(*apply(auto)*)
oops


(*This direction with auto is the problem. I need to terminate it within less
than about 5 seconds when I have "show_sorts=true".*)

lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False"
(*apply(auto)*)
oops


(*No problem with blast to prove ==, instead of auto.*)

lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(rule equal_intr_rule)
apply(blast)
apply(blast) (*Failure messages here.*)
done


(*This direction with blast is okay, though there are failure messages.*)

lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False"
apply(blast) (*Failure messages here.*)
done


(*The other direction with auto is okay.*)

lemma "False ==> (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(auto)
done

end




theory i131214a__isaU_Trueprop_False_meta_eq_auto_hangs_PIDE
imports Complex_Main 
begin

declare[[show_sorts=true]]
declare[[show_brackets=true]]
declare[[show_question_marks=true]]
notation Trueprop ("_\<Colon>\<^sub>T" [1000] 1000)

(*With "Auto Methods" off, auto goes off and doesn't come back, if it's allowed
  to run very long.*)
  
lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(rule equal_intr_rule)
(*apply(auto)*)
oops


(*This direction with auto is the problem. I need to terminate it within less
  than about 5 seconds when I have "show_sorts=true".*)

lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False"
(*apply(auto)*)
oops


(*No problem with blast to prove ==, instead of auto.*)

lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(rule equal_intr_rule)
apply(blast)
apply(blast) (*Failure messages here.*)
done


(*This direction with blast is okay, though there are failure messages.*)

lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False"
apply(blast) (*Failure messages here.*)
done


(*The other direction with auto is okay.*)

lemma "False ==> (!!f. !!a. f = (%a. a | f a) ==> (f a = a))"
apply(auto)
done

end








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.