metis_tac proving wrong theorem · Isabelle/ML

Somehow, metis_tac swallows variables of my predicate when I want to prove a theorem. See the following code:

ML_val \<open>
val t = @{thm allE}
val x = writeln ("Original thm: " ^ @{make_string} t)
val y = writeln ("Proven thm: " ^ @{make_string}
  (Goal.prove @{context} [] [] (Thm.prop_of t)
  (K (Metis_Tactic.metis_tac ["no_types"]
        ATP_Problem_Generate.combsN @{context} [] 1))))\<close>

As one can clearly see, the schematic variable ?x got destroyed and the type of ?P got changed from 'a => bool to bool. I don't quite understand why.

Kevin Kappelmann (Aug 20 2024 at 08:04):

Metis does not prove the wrong theorem. But metis does use unification and you are feeding in a problem with higher-order meta variables (often also called schematic variables). Those are the variables prefixed with ?.

In higher-order unification, some problems don't have a most-general solution. In such cases, Isabelle's higher-order unifier delays those problems not offering a most-general solution. Those problems are also referred to as "flex-flex pairs". You can see that your code creates a flex-flex pair using the code snippet I provide below (just comment out the indicated line). You have to use show_hyps to display these delayed problems.

When Isabelle is done proving a theorem, it checks if there are any flex-flex pairs that are still unsolved. In your case, there is one. Since there is no canonical solution to it, Isabelle will pick some solution for you. In your case, it decides to instantiate ?P by \x -> ?P', that is the argument provided to ?P is simply ignored.

So what can you do? Presumably, you do not want to have those meta variables in your goal to begin with: you want to show the claim for arbitrary P and R. So you fix P and R and show it for the fixed, but arbitrary P and R. And once you are done, you should be allowed to use the theorem for every P and R you can dream of - that's what they teach you in maths departments.

Indeed, Isabelle allows you to do just that as you can see in the code below: First fix the meta variables, then prove the claim, then generalise it to use meta variables again.

declare [[show_hyps]]
ML_val ‹
  val ctxt1 = @{context}
  val thm = @{thm allE}
  val _ = writeln ("Original thm: " ^ @{make_string} thm)
  val ((_, [thm]), ctxt2) = Variable.import true [thm] ctxt1 (*comment this line to see flex-flex pairs*)
  val _ = writeln ("thm with fixed meta variables: " ^ @{make_string} thm)
  fun tac {context,...} st =
    (Metis_Tactic.metis_tac ["no_types"] ATP_Problem_Generate.combsN context [] 1 st
    |> Seq.map (tap (fn st => writeln ("state: " ^ @{make_string} st))))
  val res_thm = Goal.prove ctxt2 [] [] (Thm.prop_of thm) tac
  val _ = writeln ("Proven thm: " ^ @{make_string} res_thm)
  val res_thm = singleton (Variable.export ctxt2 ctxt1) res_thm
  val _ = writeln ("Result thm: " ^ @{make_string} res_thm)
›

Stream: Isabelle/ML

Topic: metis_tac proving wrong theorem

Christian Zimmerer (Aug 19 2024 at 15:50):

Kevin Kappelmann (Aug 20 2024 at 08:04):

Christian Zimmerer (Aug 20 2024 at 08:20):