Forward fact resolution with an implication · Beginner Questions

Assume I have some lemma a, which states that some implication holds, and a lemma b that shows some conclusion under the assumption that such an implication is satisfied, e.g.:

theory Scratch
  imports Main
begin

definition P where "P ≡ undefined"
definition f where "f ≡ undefined"

lemma a: "P a ⟹ P b ⟹ P (f a b)"
  sorry
lemma b:
  assumes "⋀a b. (Q a ⟹ Q b ⟹ Q (g a b))"
  shows "∀a ∈ set as. Q a ⟹ ∀b ∈ set bs. Q b ⟹ ∀c ∈ set (map2 g as bs). Q c"
  sorry

thm b[OF a]

However, this does not work and produces the following exception, which I don't understand:

exception THM 0 raised (line 313 of "drule.ML"):
  OF: multiple unifiers
  (⋀a b. ?Q a ⟹ ?Q b ⟹ ?Q (?g a b)) ⟹
  ∀a∈set ?as. ?Q a ⟹
  ∀b∈set ?bs. ?Q b ⟹ ∀c∈set (map2 ?g ?as ?bs). ?Q c
  P ?a ⟹ P ?b ⟹ P (f ?a ?b)

thm b[of P f, OF a]

(⋀a b. P a ⟹ P b ⟹ P a) ⟹
(⋀a b. P a ⟹ P b ⟹ P b) ⟹
∀a∈set ?as. P a ⟹ ∀b∈set ?bs. P b ⟹ ∀c∈set (map2 f ?as ?bs). P c

Wolfgang Jeltsch (Sep 13 2023 at 11:06):

As for why the first attempt does not work: OF doesn’t just use its argument as the premise of the manipulated fact but only the conclusion of its argument, inserting the premises of its argument as new premises into the manipulated fact.

Jonathan Julian Huerta y Munive (Sep 13 2023 at 11:08):

Your P is polymorphic. In your theorem a, the first argument of P has type 'a and the second argument has type 'b. You have to specify these types to help the unification algorithm. Try thm b[of "P :: 'b ⇒ bool" f, OF a[of "_ :: 'b" "_ :: 'b"]] . You can look at the types by ctrl/cmnd + hovering over a term in Isabelle jedit or by typing

declare [[show_types]]

before your lemmas. In general, it is unorthodox to unify higher-order terms (which you do when you try to match the hypothesis with the implication ⟹).

Wolfgang Jeltsch (Sep 13 2023 at 11:10):

Hmm, maybe what I described was more the reason for @Jakob Schulz’s second problem instead of his first.

Kevin Kappelmann (Sep 13 2023 at 11:39):

The problem is what the error message says: There isn't a unique solution when unifying the conclusion of a with the conclusion of the first subgoal of b and OF, rather than succeeding with some solution, is programmed to fail in such circumstances.

...although it introduces some trivial assumptions:

That's because b[OF a]does discharge the first premise of b with a but rather, as mentioned above, resolves the conclusion of the first subgoal of b with the conclusion of a. It is like you would use apply (rule a) on subgoal 1 of b.

Kevin Kappelmann (Sep 13 2023 at 11:43):

The solution is to pre-instantiate the theorems to obtain a unique unification result, as you did above in thm b[of P f, OF a].
As an alternative, I wrote some tools that will hopefully be published in the AFP soon, which, among other things, let you write b[uOF a] to obtain the result that you expected (shameless plug).

Wolfgang Jeltsch (Sep 13 2023 at 13:10):

Please replace uOF by a better name. This bare mix of lower and upper case letters is completely against established Isabelle conventions.

Kevin Kappelmann (Sep 13 2023 at 13:30):

There's also urule, ufact, uassm, etc. The u stands for "unification", since these methods correspond to the known ones from the standard distribution but additionally allow the specification of a unifier. I don't know whether UOF would be an improvement over uOF from that perspective. But I'm open to suggestions.

Stream: Beginner Questions

Topic: Forward fact resolution with an implication