Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2019-RC2 Isar proof constructed by sle...

Email Gateway (Aug 22 2022 at 19:53):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I encounter things like this frequently, and it is probably not new to Isabelle2019-RC2,
but it is very rare that I can extract the example from what I am doing in a form that might
be helpful to someone trying to find and fix it.

I was using "try" to search for a proof of the first of 4 subgoals (see below, only the
first is included). There are a number of assumptions in the context, which were originally
introduced with "using" and then possibly modified by "apply simp_all".

When I tried the Isar proof that sledgehammer proposed, I found that it failed because the
statement to be proved didn't refine any pending goal. After investigation, I found that
the following had been assumed:

assume a6: "⋀μ ν. arrow_of_spans (⋅) μ ∧ arrow_of_spans (⋅) ν ∧ Dom ν = Cod μ ⟹
ν ∙ μ = ⦇Chn = Chn ν ⋅ Chn μ, Dom = Dom μ, Cod = Cod ν⦈"

whereas what should have been assumed was:

assume a6: "⋀ν μ. arrow_of_spans (⋅) μ ∧ arrow_of_spans (⋅) ν ∧ Dom ν = Cod μ ⟹
ν ∙ μ = ⦇Chn = Chn ν ⋅ Chn μ, Dom = Dom μ, Cod = Cod ν⦈"

the difference apparently being in the order of the quantified variables.

So either whatever is spitting out this assumption has incorrectly reordered the quantified
variables, or else whatever is matching the statement to be proved against the pending goal
is sensitive to the order of the variables when it shouldn't be.

- Gene Stark

(Context below)

proof (prove)
goal (4 subgoals):

1. Dom ((μ ⋆ ν ⋆ π) ⋆ ρ) = Cod (⦇Chn = μνπ.chine_assoc, Dom = Dom ((μ ⋆ ν) ⋆ π), Cod = Cod (μ ⋆ ν ⋆ π)⦈ ⋆ ρ) ⟹
   ¬ arrow_of_spans (⋅)
   ⦇Chn = μ_νπ_ρ.chine_assoc ⋅
   chine_hcomp ⦇Chn = μνπ.chine_assoc, Dom = Dom ((μ ⋆ ν) ⋆ π), Cod = Cod (μ ⋆ ν ⋆ π)⦈ ρ,
   Dom = Dom (⦇Chn = μνπ.chine_assoc, Dom = Dom ((μ ⋆ ν) ⋆ π), Cod = Cod (μ ⋆ ν ⋆ π)⦈ ⋆ ρ),
   Cod = Cod (μ ⋆ (ν ⋆ π) ⋆ ρ)⦈ ⟹
   «μ ⋆
   ⦇Chn = νπρ.chine_assoc, Dom = Dom ((ν ⋆ π) ⋆ ρ),
   Cod = Cod (ν ⋆ π ⋆ ρ)⦈ : μ ⋆ (ν ⋆ π) ⋆ ρ ⇒ μ ⋆ ν ⋆ π ⋆ ρ» ⟹
   «⦇Chn = μ_νπ_ρ.chine_assoc,
   Dom = Cod (⦇Chn = μνπ.chine_assoc, Dom = Dom ((μ ⋆ ν) ⋆ π), Cod = Cod (μ ⋆ ν ⋆ π)⦈ ⋆ ρ),
   Cod = Cod (μ ⋆ (ν ⋆ π) ⋆ ρ)⦈ : (μ ⋆ ν ⋆ π) ⋆ ρ ⇒ μ ⋆ (ν ⋆ π) ⋆ ρ» ⟹
   «⦇Chn = μνπ.chine_assoc, Dom = Dom ((μ ⋆ ν) ⋆ π), Cod = Cod (μ ⋆ ν ⋆ π)⦈ ⋆
   ρ : ((μ ⋆ ν) ⋆ π) ⋆ ρ ⇒ (μ ⋆ ν ⋆ π) ⋆ ρ» ⟹
   Chn (μ ⋆ ⦇Chn = νπρ.chine_assoc, Dom = Dom ((ν ⋆ π) ⋆ ρ), Cod = Cod (ν ⋆ π ⋆ ρ)⦈) =
   chine_hcomp μ ⦇Chn = νπρ.chine_assoc, Dom = Dom ((ν ⋆ π) ⋆ ρ), Cod = Cod (ν ⋆ π ⋆ ρ)⦈ ⟹
   Chn (⦇Chn = μνπ.chine_assoc, Dom = Dom ((μ ⋆ ν) ⋆ π), Cod = Cod (μ ⋆ ν ⋆ π)⦈ ⋆ ρ) =
   chine_hcomp ⦇Chn = μνπ.chine_assoc, Dom = Dom ((μ ⋆ ν) ⋆ π), Cod = Cod (μ ⋆ ν ⋆ π)⦈ ρ ⟹
   (⋀μ. arr μ = arrow_of_spans (⋅) μ) ⟹
   (⋀ν μ. arrow_of_spans (⋅) (ν ∙ μ) = (arrow_of_spans (⋅) μ ∧ arrow_of_spans (⋅) ν ∧ Dom ν = Cod μ)) ⟹
   (⋀ν μ. arrow_of_spans (⋅) μ ∧ arrow_of_spans (⋅) ν ∧ Dom ν = Cod μ ⟹
   ν ∙ μ = ⦇Chn = Chn ν ⋅ Chn μ, Dom = Dom μ, Cod = Cod ν⦈) ⟹
   (⋀f a b g c.
   «f : a ⇒ b» ⟹ «g : b ⇒ c» ⟹ arrow_of_spans (⋅) f ∧ arrow_of_spans (⋅) g ∧ Dom g = Cod f) ⟹
   C.null =
   chine_hcomp μ ⦇Chn = νπρ.chine_assoc, Dom = Dom ((ν ⋆ π) ⋆ ρ), Cod = Cod (ν ⋆ π ⋆ ρ)⦈ ⋅
   μ_νπ_ρ.chine_assoc ⋅ chine_hcomp ⦇Chn = μνπ.chine_assoc, Dom = Dom ((μ ⋆ ν) ⋆ π), Cod = Cod (μ ⋆ ν ⋆ π)⦈ ρ

Last updated: Nov 21 2024 at 12:39 UTC