Email Gateway (Aug 18 2022 at 10:59): Email Gateway (Aug 18 2022 at 10:59):From: Peter Lammich <peter.lammich@uni-muenster.de>
I have the following problem with the transitivity reasoning setup:
given some partial order [<\le>] on a function datatype, I want to do
transitivity reasoning. So I declare the transitivity lemma as [trans].
The problem is now, that everything works until I have a reflexivity
step. In this case, the goal gets eta-expanded at the next 'also',
causing the transitivity reasoner to fail.
My question is:
Is there a workaround, and if the workaround is to add some extra
transitivity rules, how do they have to look like ?
I added a rule "(%u. a u) = (%u. b u) ==> P b ==> P a", with this rule,
the reasoning worked sometimes (of the =-step is the first one in the
reasoning chain), but the also command takes some time and produces
some very strange output, repeatedly meantioning "unification bound
exceeded".
Here the example:
constdefs
ah_leq :: "('m \<Rightarrow> 'm set) \<Rightarrow> ('m \<Rightarrow>
'm set) \<Rightarrow> bool" (infix "[\<le>]" 50)
"h1 [\<le>] h2 == \<forall>m. h1 m \<subseteq> h2 m"
interpretation ah_leq: partial_order["op [\<le>]"]
apply (rule partial_order.intro)
apply (unfold ah_leq_def)
apply (auto intro!: ext)
done
declare ah_leq.below.trans[trans]
lemma fixes h :: "'m \<Rightarrow> 'm set" shows "False" proof -
have "h[\<le>]h" sorry
also have "h = h'" sorry
also (* Here we have calculation: (\<lambda>u. h' u) [\<le>]
(\<lambda>u. h' u)*) have "h' [\<le>] h''" sorry
also <- This fails
My current workaround is to avoid =-steps, and only use [\<le>] in the
reasoning chain.
Regards and thanks for any hints,
Peter
Email Gateway (Aug 18 2022 at 10:59):From: Makarius <makarius@sketis.net>
Eta-expansion should not be a problem here, because higher-order
unifications works module eta (and alpha and beta). You should be able to
compose these facts manually, using something like
thm ah_leq.trans [OF fact1 fact2]
The reason why 'also' fails is different: due to the reflexivity step in
the chain, there is no progress in the calculation. Such facts are
filtered out from the sequence of possible results -- an empty sequence is
left over.
The deeper reason why this is done is higher-order unification again:
certain pathological cases of substitution result in no-progress steps.
The filtering scheme nicely circumvents this. So you merely loose
reflexivity (which is not very interesting anyway), but gain many useful
applications of substitution (of equalities or inequalities).
Makarius
Last updated: May 03 2024 at 12:27 UTC