Hanno Becker (Apr 21 2023 at 11:39): 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
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.
Gimme a second to adapt your code...
Hanno Becker (Apr 21 2023 at 12:45):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
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›
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_terminmode_schematic, andProof_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: May 04 2024 at 16:18 UTC