Stream: General

Topic: applying rules/facts up to unification


view this post on Zulip Kevin Kappelmann (Mar 18 2020 at 12:52):

Hey, is there some way to apply a rule/fact such that terms not matching by unification will be spit out as a new subgoal? For example, consider this:

definition "myProp s ≡ s = {}"

(* some proof *)
lemma myProof: "myProp {}"
  unfolding myProp_def by safe

(* some very similar proof that only needs to rewrite {} ∪ {} to {} *)
(* this is the best I could come up with *)
lemma myProof': "myProp ({} ∪ {})"
proof -
  have 1: "{} ∪ {} = {}" by safe
  show ?thesis by (subst 1, fact myProof)
qed

(* The next thing is what I would like to have *)
lemma myProof'': "myProp ({} ∪ {})"
proof (fact myProof)
  show "{} ∪ {} = {}" by safe
qed

view this post on Zulip Josh Chen (Mar 20 2020 at 01:45):

I'm not aware of such a method, which I think generally runs into the usual problem of multiple possible unifiers.
But if you're happy with a basic heuristic, try this: Unify.thy

I hacked it together as an exercise and I'll probably need something like it soon myself, so I'd appreciate knowing if you find places where it breaks.

view this post on Zulip Kevin Kappelmann (Mar 20 2020 at 09:32):

Cool thanks! I'll give it a go on the actual example leading to that question later

view this post on Zulip Josh Chen (Mar 23 2020 at 12:54):

(deleted, accidental post)

view this post on Zulip Kevin Kappelmann (Mar 23 2020 at 13:52):

if anyone is curious, Josh and I applied above linked tactic to the problem I was facing, but it needs more tuning


Last updated: Aug 15 2022 at 02:13 UTC