Stream: Beginner Questions

Topic: Proof method in purple


view this post on Zulip Gergely Buday (Jan 20 2021 at 10:53):

According to

https://stackoverflow.com/questions/22635300/what-do-colour-codes-mean-in-isabelle-jedit

purple is "running process on the command"

If that command is a by (simp add:lemma), then it went to infinite loop? Other than that, it led to No Subgoals! Is this a valid proof or not?

view this post on Zulip Manuel Eberl (Jan 20 2021 at 11:00):

If it is just purple indefinitely, it means that it has not terminated yet. As I explained in the other thread, that means that the proof is not yet completed. The ‘No subgoals!’ you see is provisional in the sense that it assumes that the proof is valid (which it isn't if the simp never terminates).

view this post on Zulip Mathias Fleury (Jan 20 2021 at 11:08):

(@Manuel Eberl : I got confused when reading your sentence, but I guess "yeat complicated" -> yet completed)

view this post on Zulip Manuel Eberl (Jan 20 2021 at 11:09):

Uh, probably.

view this post on Zulip Manuel Eberl (Jan 20 2021 at 11:10):

Not sure what happened there. Probably general brain fault. :smile:

view this post on Zulip Manuel Eberl (Jan 20 2021 at 11:10):

Temporary aphasia.

view this post on Zulip Gergely Buday (Jan 20 2021 at 11:11):

Thanks. At last I have found the necessary lemmas so now it works without problem.

view this post on Zulip Gergely Buday (Jan 20 2021 at 11:15):

Also, it used lots of processor and memory, that's why I thought of an infinite loop.


Last updated: Aug 13 2022 at 06:26 UTC