Email Gateway (Aug 19 2022 at 10:39): Email Gateway (Aug 19 2022 at 10:39):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I use coinduction rules of the format as in the following example:
typedecl foo
consts unfoo :: "foo => foo"
lemma foo_coinduct[consumes 1, case_names foo]:
fixes f g :: "'a => foo"
assumes "P x"
"!!x. P x ==>
(EX x'. unfoo (f x) = f x' & unfoo (g x) = g x' & P x')
| unfoo (f x) = unfoo (g x)"
shows "f x = g x"
sorry
With the rule, I show equality of two functions are equal on some set
specified by the coinduction invariant predicate P. The second premise
expresses that P is actually an invariant under the destructors.
Frequently, the functions f and g depend on multiple parameters. To that
end, I derive from foo_coinduct one rule where x is split into two
parameters. I found that split_format (complete) almost does that:
lemmas foo_coinduct2 =
foo_coinduct[where x="(a, b)", split_format (complete)]
[| P a b;
!!a b. P a b
==> (EX x'. unfoo (f a b) = (case x' of (x, xa) => f x xa) &
unfoo (g a b) = (case x' of (x, xa) => g x xa) &
(case x' of (x, xa) => P x xa))
| unfoo (f a b) = unfoo (g a b) |]
==> f a b = g a b
The ugly thing about this are the "case x' of (x, xa) =>" bits. If
split_format (complete) would split the EX quantifier, too, they would
be gone. Of course, I can so do manually as follows, but this looses the
consumes and case_names declarations:
lemmas foo_coinduct2 =
foo_coinduct[where x="(a, b)", split_format (complete),
unfolded split_paired_Ex prod.cases]
Are there better ways to achieve my goal? Would it be sensible to extend
split_format such that it also splits EX and ALL quantifiers if needed?
These ugly case splits for EX and ALL happen also when there is free
uncurried function variable as in
notepad begin
{ fix f :: "('a * 'b) => bool"
have "EX x. f x" sorry }
thm this[split_format (complete)]
end
If there is consent that EX and ALL should also be split, I could try to
adapt split_format accordingly. A quick grep across the distribution and
the AFP shows that split_format (complete) is so far only used for a few
induction rules.
Any opinions?
Andreas
Last updated: Nov 21 2024 at 12:39 UTC