Stream: General

Topic: Reverse matching with Eisbach not working?

Wolfgang Jeltsch (Aug 22 2023 at 20:18):

Section 2.7 of the Eisbach User Manual presents the reverse matching technique. I wanted to try it out and came up with the following example:

lemma "(⋀n m. Suc n = m) ⟹ False"
  apply (
    match premises in P for P ⇒ ‹
      match ("Suc 1 = 1") in P ⇒ ‹
        match premises in prems: _ ⇒ ‹
          print_fact prems,
          print_term P
        ›
      ›
    ›
  )

I would have expected both printing methods to show Suc 1 = 1, but instead I get the following output:

print_fact: prems: Suc ?n15 = ?m15
print_term: P: Suc ?n11 = ?m11

Is reverse matching not working (anymore), or am I missing something?

Wolfgang Jeltsch (Aug 22 2023 at 20:36):

It seems that also the example in the user manual is at least not working as I understood it should: instantiation of schematic variables is not persistent. This is the example:

lemma
  assumes asms: "⋀x :: 'a. A x"
  shows "A y"
  apply (match asms in H: "A y" ⇒ ‹rule H›)?
  apply (
    match asms in H: P for P ⇒ ‹
     match ("A y") in P ⇒ ‹rule H›
    ›
  )
  done

Inserting diagnostic commands similar to the ones in my post above next to the rule H invocation will result in output containing a schematic variable instead of y. Now let’s restrict the type of the variable and replace y by a constant:

lemma
  assumes asms: "⋀x :: nat. A x"
  shows "A y"
  apply (match asms in H: "A y" ⇒ ‹rule H›)?
  apply (
    match asms in H: P for P ⇒ ‹
     match ("A 0") in P ⇒ ‹rule H›
    ›
  )
  done

This code still works, which again illustrates that the x from the assumption did not get bound beyond the actual matching activity, since otherwise rule H would have been specialized to A 0, making it impossible to prove A y with it.

Last updated: May 02 2024 at 01:06 UTC