I was playing around with an example from the Isabelle/HOL tutorial to get a better understanding on the correspondence between Isar and Tactics proofs.
This is a version which works:
lemma rtrancl_converseD: "(x,y) ∈ (r ^-1 )^* ⟹ (y,x) ∈ r^* "
proof (induct y rule: rtrancl_induct)
case base
then show ?case ..
next case (step y z)
then have "(z, y) ∈ r" using rtrancl_converseD by simp
with `(y,x)∈ r^*` show "(z,x) ∈ r^*" using [[unify_trace_failure]]
apply (subgoal_tac "1=(1::nat)")
apply (rule converse_rtrancl_into_rtrancl)
apply simp_all
done
qed
I want to instantiate converse_rtrancl_into_rtrancl
which proofs (?a, ?b) ∈ ?r ⟹ (?b, ?c) ∈ ?r^* ⟹ (?a, ?c) ∈ ?r^*
.
But without the seemingly nonsensical apply (subgoal_tac "1=(1::nat)")
line this errors with
Clash: r =/= Transitive_Closure.rtrancl
Failed to apply proof method⌂:
using this:
(y, x) ∈ r^*
(z, y) ∈ r
goal (1 subgoal):
1. (z, x) ∈ r^*
If I fully instantiate the rule apply (rule converse_rtrancl_into_rtrancl[of z y r x])
this becomes Clash: z__ =/= ya__
.
This leaves me with three questions: Why does this specific case break? How can I fix it? And how can I figure out what went wrong in these cases since I can't really understand what the unify_trace_failure message wants to tell me.
rule
-tactics are usually sensitive to the order of premises. The order of premises inconverse_rtrancl_into_rtrancl
and in your proof state don't match. Switching the order of premises in the proof state usingrotate_tac
will make them match the rule, so that you can directly applyfact
like this:Or, if you want to include some kind of
rule
tactic, this would look like this:(I personally don't use apply scripts ever in my everyday work. So apply-style gurus might know more elegant ways of handling this kind of situation. ;) )
Regarding your
1=(1::nat)
/simp_all
fix:The whole goal can directly be solved by
simp_all
. So, attempts with adding stuff like1=1
probably did not really tell you a lot about how much the other methods contributed to solving the proof.However, the additional assumption seems to actually help Isabelle match
converse_rtrancl_into_rtrancl
correctly. (Don't ask me why!) So, one could indeed circumvent the problem by adding this spurious assumption and then eliminating it withrefl
again like:This does not look particularly elegant, of course.
The
[[unify_trace_failure]]
probably only really helps if one is familiar with the internal workings of Nipkow's higher-order unification algorithm. (I'm not.) I think the hint for the future here would really be that one must look closely at the order of premises for some tactics (rather than at the unifier debug output).