Stream: General

Topic: Metis: The assumptions are inconsistent

Chengsong Tan (Mar 13 2024 at 13:19):

Hi all,

I got the error message Metis: The assumptions are inconsistent while proving subgoals with metis of a lemma of the following form:

assumes "P T ∧ Q T∧ R T"
  shows "P T'"

I presume that means "P T ∧ Q T∧ R T" is False.
How do I get a witness from metis that the assumption is indeed inconsistent?
(I have removed all sorry before that lemma, and introduced no new axioms).
Please see lin 340 of the file SimpleDeviceIIAGO_WritePull.thy for the specific issue.

Best,
Chengsong
SimpleDeviceIIAGO_WritePull.thy
Transposed.thy
BasicInvariants.thy
BuggyRules.thy
CoherenceProperties.thy

Mathias Fleury (Mar 13 2024 at 13:23):

    have i204: False
      using assms i617 nextReqRespIs.simps(1)[of _] unfolding nextGOPendingIs_def
      supply [[metis_trace]]
      by metis

Mathias Fleury (Mar 13 2024 at 13:26):

With this is is clear:

    have i204: False
      using assms i617 nextReqRespIs.simps(1)[of ‹GO_WritePull›] unfolding nextGOPendingIs_def simp_thms
        if_True

Mathias Fleury (Mar 13 2024 at 13:26):

(look at the proof state)

Mathias Fleury (Mar 13 2024 at 13:27):

(I did this per hand)

Chengsong Tan (Mar 13 2024 at 13:31):

Thanks a lot, Mathias!
Doing a have "False" try also yields the conflicting facts, but how did you come up with the
using assms i617 nextReqRespIs.simps(1)[of ‹GO_WritePull›] unfolding nextGOPendingIs_def simp_thms bit?

Mathias Fleury said:

    have i204: False
      using assms i617 nextReqRespIs.simps(1)[of _] unfolding nextGOPendingIs_def
      supply [[metis_trace]]
      by metis

Mathias Fleury (Mar 13 2024 at 13:38):

I first transformed the proof into:

have  False
   using XXXX by metis

Mathias Fleury (Mar 13 2024 at 13:39):

Then I looked at the facts and saw some definition. So I applied it, yielding:

have  False
   using XXXX  unfolding YYY by metis

After the unfolding there was a "if 0 = 0 then ... else ..." which I wanted to remove

Mathias Fleury (Mar 13 2024 at 13:56):

ho, and there was a single fact nextReqRespIs.simps that required instantiation. I looked at the context and there was a single matching term.

Last updated: May 02 2024 at 04:18 UTC