Email Gateway (Aug 18 2022 at 12:16): Email Gateway (Aug 18 2022 at 12:16):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,
I have problems using pattern-matching with pairs. The thing is that I'm
not able to prove equivalence between an expression
(let (_,_,s) = f n in P s)
and
P (snd (snd (f n)))
Are there any general advices (except, don't use pairing =)).
cheers
christian
Email Gateway (Aug 18 2022 at 12:16):From: Peter Lammich <peter.lammich@uni-muenster.de>
A manual case split does the job.
lemma "(let (_,_,s) = f n in P s) = P (snd (snd (f n)))"
by (cases "f n") auto
No idea whether there's an automatic way.
--
Peter
Christian Sternagel wrote:
--
Peter Lammich, Institut für Informatik
Raum 715, Einsteinstrasse 62, 48149 Münster
Mail: peter.lammich@uni-muenster.de
Tel: 0251-83-32749
Mobil: 0163-5310380
Email Gateway (Aug 18 2022 at 12:16):From: Brian Huffman <brianh@cs.pdx.edu>
You can rewrite "(let (_,_,s) = f n in P s)" using
(simp only: Let_def split_def)
which results in "P (snd (snd (f n)))"
Quoting Christian Sternagel <christian.sternagel@uibk.ac.at>:
Email Gateway (Aug 18 2022 at 12:16):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Thanks for your reply,
in the meantime I found out (thnx to Alexander Krauss) that the
following also does work
lemma "(let (_,_,s) = f n in P s) = P (snd (snd (f n)))"
unfolding Let_def split_def ..
I don't know which (if any) of the two ways is preferable.
christian
Peter Lammich wrote:
Last updated: May 03 2024 at 12:27 UTC