## Stream: Isabelle/ML

### Topic: Pattern matching goals

#### Hanno Becker (Apr 21 2023 at 11:39):

Hi! I'd like to do some goal-dependent branching in my tactics, but run into some issue with unification. The following is a minimal example illustrating the issue:

``````theory Scratch
imports Main
begin

ML‹
fun strip_trueprop ((Const (@{const_name HOL.Trueprop}, _)) \$ c) = c
| strip_trueprop c = c

val pattern = Syntax.parse_term @{context} "?x = ?y" |> Type.strip_constraints

fun is_unifiable_pair (ctxt : Proof.context) (t0 : term) (t1 : term) =
Unify.unifiers (Context.Proof ctxt, Envir.empty 0, [(t0,t1)])
|> Seq.pull
|> Option.isSome

fun is_equality (ctxt : Proof.context) (goal : term) : bool =
goal |> Type.strip_constraints |> is_unifiable_pair ctxt pattern

val term0 = @{term "x=y"} |> Type.strip_constraints
val term1 = Syntax.parse_term @{context} "x=y" |> Type.strip_constraints

val compare0 = is_equality @{context} term0 (* false *)
val compare1 = is_equality @{context} term1 (* true  *)
›

lemma test: ‹x=y›
apply (tactic‹SUBGOAL (fn (goal, _) =>
if goal |> strip_trueprop |> is_equality @{context}
then print_tac @{context} "match"
else print_tac @{context} "no match") 1›) (* no match *)
oops

end
``````

#### Hanno Becker (Apr 21 2023 at 11:40):

Can someone explain why the match isn't succeeding in all cases?

#### Wolfgang Jeltsch (Apr 21 2023 at 12:32):

Not an answer but a question: Why don’t you use Eisbach with its `match` method?

#### Hanno Becker (Apr 21 2023 at 12:38):

I'm working in the context of a quite performance sensitive proof automation and found that circumventing Eisbach by writing tactics directly in ML both gives me more control and leads to slightly better performance.

#### Kevin Kappelmann (Apr 21 2023 at 12:43):

The problem is that you only parsed the terms but did not check them. This left you with some placeholders `_` in your types, which it cannot unify against any other type other than `_` itself.
In particular, the concrete representation of your term `pattern` is the following:

``````Const ("HOL.eq", "_") \$ Var (("x", 0), "_") \$ Var (("y", 0), "_")
``````

while what you actually want is this:

``````Const ("HOL.eq", "?'a ⇒ ?'a ⇒ bool") \$ Var (("x", 0), "?'a") \$ Var (("y", 0), "?'a")
``````

You should use `read_term` rather than `parse_term` to get a type-checked term.
In the words of the implementation manual, page 94: `read = parse; check`.

Wow, super.

#### Hanno Becker (Apr 21 2023 at 12:47):

`Syntax.read_term` complains about the schematic variable, but `Proof_Context.read_term_pattern` seems to work fine?

#### Kevin Kappelmann (Apr 21 2023 at 12:51):

``````ML‹
val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
val pattern = Syntax.read_term ctxt "(?x :: ?'a) = ?y"

fun maxidx_of_terms terms = fold (Integer.max o Term.maxidx_of_term) terms (~1)

fun is_unifiable_pair (ctxt : Proof.context) (t0 : term) (t1 : term) =
Unify.unifiers (Context.Proof ctxt, Envir.empty (maxidx_of_terms [t0, t1] + 1), [(t0, t1)])
|> Seq.pull
|> Option.isSome

fun is_equality (ctxt : Proof.context) (goal : term) : bool =
goal |> is_unifiable_pair ctxt pattern

val term0 = @{term "x=y"}
val term1 = Syntax.read_term @{context} "x=y"

val compare0 = is_equality @{context} term0 (* true *)
val compare1 = is_equality @{context} term1 (* true  *)
›

lemma test: ‹x=y›
apply (tactic‹SUBGOAL (fn (goal, _) =>
if goal |> HOLogic.dest_Trueprop |> is_equality @{context}
then print_tac @{context} "match"
else print_tac @{context} "no match") 1›) (* match *)
oops
``````

#### Hanno Becker (Apr 21 2023 at 12:53):

Awesome, thanks a lot! Is there meaningful difference between `read_term` in `mode_schematic`, and `Proof_Context.read_term_pattern`?

#### Kevin Kappelmann (Apr 21 2023 at 12:55):

BTW. if you really just want to look whether some term matches the equality constant, you can simply do this:

``````  fun try_bool f = try f #> (Option.getOpt o rpair false)
val is_equality = try_bool \<^Const_fn>‹HOL.eq _ for _ _ => true›
``````

#### Hanno Becker (Apr 21 2023 at 12:56):

Thanks! No, my actual use is more complicated and will require the general version

#### Kevin Kappelmann (Apr 21 2023 at 13:00):

Kevin Kappelmann said:

``````ML‹
val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
val pattern = Syntax.read_term ctxt "(?x :: ?'a) = ?y"

fun maxidx_of_terms terms = fold (Integer.max o Term.maxidx_of_term) terms (~1)

fun is_unifiable_pair (ctxt : Proof.context) (t0 : term) (t1 : term) =
Unify.unifiers (Context.Proof ctxt, Envir.empty (maxidx_of_terms [t0, t1] + 1), [(t0, t1)])
|> Seq.pull
|> Option.isSome

fun is_equality (ctxt : Proof.context) (goal : term) : bool =
goal |> is_unifiable_pair ctxt pattern

val term0 = @{term "x=y"}
val term1 = Syntax.read_term @{context} "x=y"

val compare0 = is_equality @{context} term0 (* true *)
val compare1 = is_equality @{context} term1 (* true  *)
›

lemma test: ‹x=y›
apply (tactic‹SUBGOAL (fn (goal, _) =>
if goal |> HOLogic.dest_Trueprop |> is_equality @{context}
then print_tac @{context} "match"
else print_tac @{context} "no match") 1›) (* match *)
oops
``````

Small update: it should actually be `val pattern = Syntax.read_term ctxt "(?x :: ?'a) = ?y"`

#### Hanno Becker (Apr 21 2023 at 13:09):

Thanks again Kevin, this was very helpful

#### Kevin Kappelmann (Apr 21 2023 at 13:10):

Hanno Becker said:

Awesome, thanks a lot! Is there meaningful difference between `read_term` in `mode_schematic`, and `Proof_Context.read_term_pattern`?

There are some differences, but I do not know exactly what the differences are. One difference is that `mode_pattern` will create schematic types wherever possible whereas `mode_schematic` will create polymorphic types. Example:

``````ML‹
val pattern1 = Proof_Context.read_term_pattern @{context} "?x = ?y"
val pattern2 = Proof_Context.read_term_schematic @{context} "?x = ?y"
›
``````

creates the concrete terms:

``````val pattern1 =
Const ("HOL.eq", "?'a1 ⇒ ?'a1 ⇒ bool") \$ Var (("x", 0), "?'a1") \$ Var (("y", 0), "?'a1")
val pattern2 =
Const ("HOL.eq", "'a ⇒ 'a ⇒ bool") \$ Var (("x", 0), "'a") \$  Var (("y", 0), "'a")
``````

Last updated: Dec 07 2023 at 16:21 UTC