Stream: Beginner Questions

Topic: Sledgehammer (smt verit) reconstruction failure

Patrick Nicodemus (Oct 26 2023 at 22:55):

Hi,
I am on Isabelle 2023 and I am trying to prove the following with Sledgehammer.

theory category
  imports Main
begin

locale category =
  fixes   E :: "'a ⇒ bool" and
  composition_law :: "'a ⇒ 'a ⇒ 'a" (infix "⋅" 60)
  (* Existence predicate *)
  (* Domain *)
  and dom :: "'a ⇒ 'a"
  (* Codomain *)
  and cod :: "'a ⇒ 'a"
  assumes assoc : "f ⋅ (g ⋅ h) = (f ⋅ g) ⋅ h"
  and
  "⟦ E f ⟧ ⟹ (dom f) ⋅ f = f" and
  "⟦ E f ⟧ ⟹ f ⋅ (cod f) = f" and
  "⟦ E f ; E g ; cod f = dom g ⟧ ⟹ E (f ⋅ g)" and
  "⟦ E f ; E g ; cod f = dom g ⟧ ⟹ dom (f ⋅ g) = dom f" and
  "⟦ E f ; E g ; cod f = dom g ⟧ ⟹ cod (f ⋅ g) = cod g" and
  "⟦ E (f ⋅ g) ⟧ ⟹ E g" and
  "⟦ E (f ⋅ g) ⟧ ⟹ E f" and
  "⟦ E f ⟧ ⟹ cod (dom f) = dom f"

theorem (in category) codid :
 "⟦ E f ; E g; cod f = cod g ⟧ ⟹ g ⋅ (cod f) = g"
sledgehammer

When I run sledgehammer it says that cvc4, verit and zipperposition found a proof.
cvc4 says "Try this: by (smt (verit) category_axioms category_def)" but when I do this verit fails and says

Failure node
Enter MATCH

and then returns a huge verit proof-term that is too big to copy and paste here.
zipperposition says: "One-line proof reconstruction failed: by (metis category_axioms category_def)" and doesn't give anything more.

Something seems wrong here. This theorem seems easy and it should be fine for sledgehammer to reconstruct it.
Should I reinstall Isabelle or what?
Can anybody else reproduce this error?

Patrick Nicodemus (Oct 27 2023 at 20:23):

This seems messed up, like something is wrong with the way I installed verit or a configuration problem. How can I debug this?

Patrick Nicodemus (Oct 27 2023 at 21:59):

Ah i see what the problem is, i didn't name my locale assumptions and that breaks things apparently. Adding names to the locale assumptions makes everything work. However I do think that this should be an error or a warning for the user at the time the locale is defined! it is very confusing that it accepts the locale definition and then later code just doesn't work

Mathias Fleury (Oct 28 2023 at 04:33):

This is a problem in the reconstruction, but not one we can fix. In the reconstruction there is one rule where we call auto and then its unifiers starts looping (causing your error message)

Mathias Fleury (Oct 28 2023 at 04:34):

z3 instead works

Mathias Fleury (Oct 28 2023 at 04:34):

This has nothing to do with the locale name, you just entered the non-determinism of Sledgehammer suggestions…

Mathias Fleury (Oct 28 2023 at 04:36):

With

theorem (in category) codid :
 "⟦ E g; cod f = cod g ⟧ ⟹ g ⋅ (cod f) = g"
  supply [[smt_trace]]
  by (smt (verit) category_axioms category_def)

you can see the proof steps

Patrick Nicodemus (Oct 28 2023 at 15:28):

Ok. So when I fixed the problem by giving specific names to the assumptions, do you have any idea how that would have made that resolve the issues?

Last updated: Apr 28 2024 at 04:17 UTC