Email Gateway (Aug 22 2022 at 18:00): Email Gateway (Aug 22 2022 at 18:00):From: Joshua Chen <joshua.chen@uni-bonn.de>
Dear all,
I'm finding that
lemma assumes "A: U(i) &&& (x: A ==> b(x): B(x))" shows
"x:A ==> b(x): B(x)" using assms by (rule conjunctionD2)
works, but
lemma assumes "A: U(i) &&& (!!x. x: A ==> b(x): B(x))"
shows "!!x. x:A ==> b(x): B(x)" using assms by (rule
conjunctionD2)
fails.
Why does this happen?
Best wishes,
Josh
Email Gateway (Aug 22 2022 at 18:02):From: Makarius <makarius@sketis.net>
(This looks like Type-Theory reasoning, but the notation also happens to
work in the context of Main or ZF.)
The Pure conjunction (with notation &&&) is for internal use, e.g. to
represent simultaneous results in intermediate situations. Its rule
violate certain disciplines of object-logic rule composition, e.g. as
explained in the "implementation" manual, section 2.4.
Operationally, the proof step "using assms by (rule conjunctionD2)"
starts out with the following rule compositions (before failing):
apply (rule conjunctionD2 [OF assms])
You can inspect applied fact as usual:
thm conjunctionD2 [OF assms]
This reveals a fact that is not in HHF normal form: it does not work
together with the usual "lifting" of rules into the subgoal structure.
Here is a structured Isar proof to illustrate the situation further, and
to provide a workaround:
lemma
assumes "A: U(i) &&& (!!x. x: A ==> b(x): B(x))"
shows "!!x. x:A ==> b(x): B(x)"
proof -
fix x
assume *: "x:A"
show "b(x): B(x)"
proof -
{ note conjunctionD2 [OF assms] }
from this [OF *] show ?thesis .
qed
qed
The curly braces delimit a local block: the exported fact at its closing
is always put into HHF normal form, thus it becomes possible to apply
"this" properly to the pending problem.
The conclusion of the experiment is that &&& should not be used in
regular proofs -- it does not fit into the standard policies.
What application did you have in mind in the first place?
Makarius
Last updated: Apr 26 2024 at 20:16 UTC