Email Gateway (Aug 18 2022 at 12:58): Email Gateway (Aug 18 2022 at 12:58):From: Chris Capel <pdf23ds@gmail.com>
I'm trying to define an inductive set of type "token list set", where
"token" is just some datatype. Initially I had definitions along the
lines of this:
datatype token = C1 nat | C2 nat
inductive_set P where
base: "[C1 1, C2 2] : P" |
other: "ws @ [C1 x, C2 y] @ zs : P ==> ws @ [C1 x, C1 m, C2 n, C2 y] @ zs : P"
This is a clear, correct way of defining it. However, it's not at
all easy to work with when proving membership, whether forwards or
backwards, because of the need to break of the list one is unifying
with before applying the rule. So I tried changing it to this:
inductive_set P where
base: "[C1 1, C2 2] : P" |
other: "[| base : P; take 2 (drop n base) = [C1 x, C2 y] |] ==>
insert_list [C1 m, C2 n] base (n + 1) : P"
("insert_list x y n" puts x into y at n.) This definition, besides
being less clear, doesn't actually work, as "= [x, y]" doesn't perform
pattern matching. Instead, the equality asserts that (take a b) = [x,
y] for any x and y, which is obviously not true.
Is there a better way to do this? Is there maybe a way to get the
second example to work?
Chris Capel
Email Gateway (Aug 18 2022 at 12:58):From: Tobias Nipkow <nipkow@in.tum.de>
Your second definition looks correct to me. But it is probably not much
easier to use than the first. I would stick to the first definition and
write structured proofs where you rearrange the list into the required
form (one simp step will do that) before apply the rule.
Tobias
Chris Capel schrieb:
Email Gateway (Aug 18 2022 at 12:58):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Chris Capel wrote:
I'm trying to define an inductive set of type "token list set", where
"token" is just some datatype. Initially I had definitions along the
lines of this:datatype token = C1 nat | C2 nat
inductive_set P where
base: "[C1 1, C2 2] : P" |
other: "ws @ [C1 x, C2 y] @ zs : P ==> ws @ [C1 x, C1 m, C2 n, C2 y] @ zs : P"This is a clear, correct way of defining it. However, it's not at
all easy to work with when proving membership, whether forwards or
backwards, because of the need to break of the list one is unifying
with before applying the rule. So I tried changing it to this:inductive_set P where
base: "[C1 1, C2 2] : P" |
other: "[| base : P; take 2 (drop n base) = [C1 x, C2 y] |] ==>
insert_list [C1 m, C2 n] base (n + 1) : P"("insert_list x y n" puts x into y at n.) This definition, besides
being less clear, doesn't actually work, as "= [x, y]" doesn't perform
pattern matching. Instead, the equality asserts that (take a b) = [x,
y] for any x and y, which is obviously not true.??? Aren't x and y implicitly universally quantified over the _whole_ rule ?
That is (since they don't appear after the ==>, they are implicitly
_existentially_ quantified where they appear).
BTW, you seem to be overloading 'n'.
Is there a better way to do this? Is there maybe a way to get the
second example to work?What exactly happens when you try the second way?
Jeremy
Chris Capel
Email Gateway (Aug 18 2022 at 12:59):From: Chris Capel <pdf23ds@gmail.com>
On Sun, Feb 8, 2009 at 15:13, Jeremy Dawson <jeremy@rsise.anu.edu.au> wrote:
Chris Capel wrote:
inductive_set P where
base: "[C1 1, C2 2] : P" |
other: "[| base : P; take 2 (drop n base) = [C1 x, C2 y] |] ==>
insert_list [C1 m, C2 n] base (n + 1) : P"("insert_list x y n" puts x into y at n.) This definition, besides
being less clear, doesn't actually work, as "= [x, y]" doesn't perform
pattern matching. Instead, the equality asserts that (take a b) = [x,
y] for any x and y, which is obviously not true.??? Aren't x and y implicitly universally quantified over the _whole_ rule ?
That is (since they don't appear after the ==>, they are implicitly
_existentially_ quantified where they appear).
I believe so, but I'm not sure. I didn't mean to imply otherwise. My
point was that unification doesn't instantiate them.
BTW, you seem to be overloading 'n'.
Oops. My actual theory does not do this. :)
Is there a better way to do this? Is there maybe a way to get the
second example to work?What exactly happens when you try the second way?
Well, with some more testing I've seen that this will work (i.e. it's
correct), but the problem is I have to manually instantiate x and y,
whereas ideally they would be instantiated by unification. That was
the same problem with the first formulation--manual instantiation of
stuff that you would wish wasn't necessary. However, maybe, as per
Tobias, I need to learn to do structured proofs.
Chris Capel
Last updated: May 03 2024 at 08:18 UTC