Email Gateway (Aug 18 2022 at 17:54): Email Gateway (Aug 18 2022 at 17:54):From: Anja Gerbes <agerb@gmx.de>
Good evening,
I am working with Isabelle, but in the following lemmas I cannot solve the problem. Can you tell me how I can complete the proof of the following lemma?
lemma subst_no_occ:
shows "\<not> occ (Var v) t
\<Longrightarrow> Var v \<noteq> t
\<Longrightarrow> t \<triangleleft> [(v,s)] = t"
and "\<not> occ_list (Var v) ts
\<Longrightarrow> (\<And>u. u \<in> set ts
\<Longrightarrow> Var v \<noteq> u)
\<Longrightarrow> apply_subst_list ts [(v,s)] = ts"
apply (induct rule: trm.inducts)
apply (simp_all)
...
done
If I would find a solution, how could I prove this lemma in Isabelle, then I could continue working on this and expand the following Lemma:
lemma MGU_Var[intro]:
assumes no_occ: "\<not>occ (Var v) t"
shows "MGU [(v,t)] (Var v) t"
proof (intro MGUI exI)
show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
apply (cases "Var v = t")
apply (auto simp:subst_no_occ)
proof -
fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>"
then have "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>"
proof -
fix s have "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th
apply (induct s)
apply (auto)
qed
qed
qed
Unfortunately I can not verify that my assumption is correct, because there must first be proved Lemma no_subst_occ for it. It would be very kind of you, if you could help me in this case.
For a better understanding of the unification algorithm and further lemma is stated that I was able to prove already. I can send it to you if you want it.
Greetings Anja
Email Gateway (Aug 18 2022 at 17:55):From: Lars Noschinski <noschinl@in.tum.de>
On 20.07.2011 20:19, Anja Gerbes wrote:
I am working with Isabelle, but in the following lemmas I cannot solve the problem. Can you tell me how I can complete the proof of the following lemma?
lemma subst_no_occ:
shows "\<not> occ (Var v) t
\<Longrightarrow> Var v \<noteq> t
\<Longrightarrow> t \<triangleleft> [(v,s)] = t"
and "\<not> occ_list (Var v) ts
\<Longrightarrow> (\<And>u. u \<in> set ts
\<Longrightarrow> Var v \<noteq> u)
\<Longrightarrow> apply_subst_list ts [(v,s)] = ts"
apply (induct rule: trm.inducts)
apply (simp_all)
...
done
If proofs get more complex, it is often a good idea, to use structured
proofs instead of apply scripts (see the Isar Tutorial for an
introduction, if you've have never worked with structured proofs).
So start your proof with
proof (induct rule: trm.inducts)
You can use Isabelle / Show Me / Cases in Proof General, to see which
cases are there. It turns out, two of them are really easy:
proof (induct rule: trm.inducts)
case Var then show ?case by simp
next
case Nil_trm then show ?case by simp
next
Now, the two cases Fn and Cons_trm seem to be harder; neither simp nor
auto can solve these directly; at least, as long as you don't give
additional lemmas. At this point, you have multiple options, amongst others:
- Split the proof into smaller steps, which might be easier to solve
- Use find_theorems to find a useful lemma, which might already
exist, but is not known to the various automatic solvers
- Often quite useful: Try sledgehammer to find proofs automatically.
Often the proof found by sledgehammer can also help you to identify
lemmas which enable the simplifier to find a proof.
Let's have a look at Cons_trm.
next
case Cons_term then show ?case
apply simp
Still some goal left. How can we proceed? Hm, there is an "if" in the
hypotheses:
~(if occ (Var v) trm then True else occ_list (Var v) list)
By default, the simplifier only expands an "if", if it can simplify the
condition to either true or false. So it might help, if we tell Isabelle
to do a case distinction on the condition:
apply (cases "occ (Var v) trm")
apply simp_all
No subgoals!
Nice, that helped. Instead of using cases, We can also tell the
simplifier to split the if and just use
by (simp add: split_if)
instead. Now, how can we solve the last goal? Maybe "split_if" also
helps us here?
next
case Fn then show ?case
apply (simp add: split_if)
No, does not seem to suffice. What's left?
⟦(⋀u. u ∈ set list ⟹ Var v ≠ u) ⟹ apply_subst_list list [(v, s)] = list;
¬ list_ex (op = (Var v)) list ∧
(¬ list_ex (op = (Var v)) list ⟶ ¬ occ_list (Var v) list)⟧
⟹ apply_subst_list list [(v, s)] = list
Let's try brute force and invoke "sledgehammer". If I run sledgehammer
on my version of Isabelle, it finds the following proof (might be
different in the Isabelle 2011 release):
by (metis (full_types) list_ex_iff)
This is a perfectly valid proof, but often you can gain knowledge about
Isabelle's library, if you take this proof to find a new proof with the
simplifier. So replace the proof we have till now with
by (simp add: list_ex_iff split_if)
qed
We're lucky, it works like a charm! Now, that we have found a proof, we
can turn it into a really compact one: Each of our subgoals was solved
with simp, so we replace the whole proof...qed block by
by (induct rule: trm.inducts) (auto simp: list_ex_iff split_if)
(auto is much like the simplifier, but uses some more techniques and
applies to all goals).
So, we now have found a really compact proof. But such a short, nice
proof is often the result of some lengthy process. If you are proficient
in Isabelle's library, you are considerably faster, but such knowledge
comes only with experience.
And when you request help from others, it really helps, if you narrow
your problem down. Instead of presenting the whole problem, just present
the subgoal you are not able to solve; but provide enough context, that
one can recreate what you have done. Exact questions have a much better
chance to be answered.
If I would find a solution, how could I prove this lemma in Isabelle, then I could continue working on this and expand the following Lemma:
If you are sure that a lemma holds but you don't want to prove it right
now, you can use "sorry" to fake a proof (as long as you are in
quick'n'dirty mode). But of course, this always bears the risk that you
build your later work on sand, not on a solid fundament ...
Greetings and HTH, Lars
Email Gateway (Aug 18 2022 at 17:55):From: Lars Noschinski <noschinl@in.tum.de>
On 22.07.2011 10:53, Johannes Hölzl wrote:
Hey, A nice description how proving in Isabelle actually works!
Thanks!
Just a small note about split_if:
Am Donnerstag, den 21.07.2011, 19:04 +0200 schrieb Lars Noschinski:
Nice, that helped. Instead of using cases, We can also tell the
simplifier to split the if and just useby (simp add: split_if)
instead. Now, how can we solve the last goal? Maybe "split_if" also
helps us here?next
case Fn then show ?case
apply (simp add: split_if)No, does not seem to suffice. What's left?
It should work with
(simp split: split_if)
i.e. it is not a normal simp rule but added to the splitter.
In this case it also works for the simplifier. Actually, I had to go to
the old HOL manual, to find out, why one would usually use the splitter
for this. In our case, the if is in the assumption, so one would need
(simp split: split_if_asm)
here instead. But I'm quite fuzzy on the semantics of the split
parameter -- why would split_if be applied to the conclusion and
split_if_asm to the hypotheses? Is there somewhere a high-level
description of the splitter?
BTW: Is the isar-ref documentation about the split method correct? It
does not seem (and need) to accept the "(asm)" option?
[...]
Let's try brute force and invoke "sledgehammer". If I run sledgehammer
on my version of Isabelle, it finds the following proof (might be
different in the Isabelle 2011 release):by (metis (full_types) list_ex_iff)
This is a perfectly valid proof, but often you can gain knowledge about
Isabelle's library, if you take this proof to find a new proof with the
simplifier. So replace the proof we have till now withby (simp add: list_ex_iff split_if)
This should be "(auto simp add: list_ex_iff split_if)"
qed
I don't have your theories but I assume (simp add: list_ex_iff) is
enough? Otherwise (simp add: list_ex_iff split: split_if) would be
required.
[I attached theory I used] No, this does not suffice. And while
(auto simp: list_ex_iff split: split_if_asm)
is probably the more correct solution, mine suffices to prove this goal.
-- Lars
Scratch.thy
Last updated: Apr 26 2024 at 01:06 UTC