Email Gateway (Aug 19 2022 at 14:28): Email Gateway (Aug 19 2022 at 14:28):From: Joachim Breitner <breitner@kit.edu>
Hi,
I’m quite fond of "also ... also ... finally" chains, as they tend to
remove a lot of distracting technicalities from a proof.
When working with HOLCF proofs, I would like to do proofs like this:
notepad
begin
fix a b c d f g
have "a ⊑ f ⋅ b" sorry
also have "b ⊑ g ⋅ c" sorry
also have "c ⊑ d" sorry
finally
have "a ⊑ f ⋅ (g ⋅ d)".
end
I currently do that by hard-coding all the variants of the trans rule
that I need:
lemma [trans]: "a ⊑ f ⋅ b ⟹ b ⊑ c ⟹ a ⊑ f ⋅ c"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]: "a ⊑ f ⋅ b ⟹ f ⊑ g ⟹ a ⊑ g ⋅ b"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]: "a ⊑ f ⋅ (g ⋅ b) ⟹ b ⊑ c ⟹ a ⊑ f ⋅ (g ⋅ c)"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]: "a ⊑ f ⋅ b ⋅ c ⋅ d ⟹ b ⊑ b' ⟹ a ⊑ f ⋅ b' ⋅ c ⋅ d"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]: "a ⊑ f ⋅ b ⋅ c ⋅ d ⟹ c ⊑ c' ⟹ a ⊑ f ⋅ b ⋅ c' ⋅ d"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]: "a ⊑ f ⋅ (g ⋅ b) ⋅ c ⋅ d ⟹ g ⊑ g' ⟹ a ⊑ f ⋅ (g' ⋅ b) ⋅ c ⋅ d"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]: "a ⊑ f ⋅ b ⋅ (g ⋅ c ⋅ d) ⋅ e ⟹ d ⊑ d' ⟹ a ⊑ f ⋅ b ⋅ (g ⋅ c ⋅ d') ⋅ e"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
This works, but is rather inflexible and does not scale. And note that
all those trans rules are solved by the same set of rules.
How can I improve that?
One thing I tried was to use
lemma strong_trans[trans]:
"a ⊑ f x ⟹ x ⊑ y ⟹ cont f ⟹ a ⊑ f y " sorry
This way, the calculation above become
cont (Rep_cfun f) ⟹ cont (λa. f⋅(g⋅a)) ⟹ a ⊑ f⋅(g⋅d)
so using "by simp" instead of "." finishes this. But I find this
annoying (I really like to finish with "finally ?something.").
Is there a way to have the side-condition already checked by "trans" (by
solving it with "intro cont2cont", for example), so that that they never
show up to the user?
That rule also breaks antisymmetry proofs like
notepad
begin
fix a b c :: "'a ::cpo"
have "a ⊑ b" sorry
also have "b ⊑ c" sorry
also have "c ⊑ a" sorry
finally
have "a = c".
end
as the calculation at the end will be the unhelpful theorem
cont (λa. a) ⟹ cont (λa. a) ⟹ a ⊑ a.
can I avoid that?
Thanks
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:28):From: Makarius <makarius@sketis.net>
On Wed, 14 May 2014, Joachim Breitner wrote:
One thing I tried was to use
lemma strong_trans[trans]:
"a ⊑ f x ⟹ x ⊑ y ⟹ cont f ⟹ a ⊑ f y " sorryThis way, the calculation above become
cont (Rep_cfun f) ⟹ cont (λa. f⋅(g⋅a)) ⟹ a ⊑ f⋅(g⋅d)
so using "by simp" instead of "." finishes this. But I find this
annoying (I really like to finish with "finally ?something.").
If the final "by simp" (or "by simp_all") for accumulated side-conditions
does the job, why not use it? If all Isar calculations were to end with
"." I could have omitted that flexibility in the language.
Formally, you did not explain the annoyance nor why you like to do it only
like that. There can be technical problems in some situations, but if
that is the case here it needs to be made specific.
Is there a way to have the side-condition already checked by "trans" (by
solving it with "intro cont2cont", for example), so that that they never
show up to the user?
That is just the standard question about all structure proof elements: Is
it sufficient to have some fixed scheme of rule application that is
parameterized by facts from the library? Or is there a need to allow
arbitrary tool implementations in that slot (in Isabelle/ML). 15 years
ago the question was on the table, and the answer was that plain rules for
'also' are usually sufficient.
That rule also breaks antisymmetry proofs like
notepad
begin
fix a b c :: "'a ::cpo"
have "a ⊑ b" sorry
also have "b ⊑ c" sorry
also have "c ⊑ a" sorry
finally
have "a = c".
endas the calculation at the end will be the unhelpful theorem
cont (λa. a) ⟹ cont (λa. a) ⟹ a ⊑ a.
can I avoid that?
Did you try to specify some particular rules for particular 'also' steps?
There is a notation with round parenthese described in the isar-ref
manual.
Makarius
Email Gateway (Aug 19 2022 at 14:28):From: Joachim Breitner <breitner@kit.edu>
Dear Makarius,
Am Mittwoch, den 14.05.2014, 20:56 +0200 schrieb Makarius:
On Wed, 14 May 2014, Joachim Breitner wrote:
One thing I tried was to use
lemma strong_trans[trans]:
"a ⊑ f x ⟹ x ⊑ y ⟹ cont f ⟹ a ⊑ f y " sorryThis way, the calculation above become
cont (Rep_cfun f) ⟹ cont (λa. f⋅(g⋅a)) ⟹ a ⊑ f⋅(g⋅d)
so using "by simp" instead of "." finishes this. But I find this
annoying (I really like to finish with "finally ?something.").If the final "by simp" (or "by simp_all") for accumulated side-conditions
does the job, why not use it? If all Isar calculations were to end with
"." I could have omitted that flexibility in the language.
I’m not sure. Last time I tried it I was not satisfied for some reason,
although that reason did not show up when preparing the small example
for my mailing list mail. Maybe I should simply re-evaluate that option.
Formally, you did not explain the annoyance nor why you like to do it only
like that. There can be technical problems in some situations, but if
that is the case here it needs to be made specific.
I think my annoyance is purely aesthetically, and – picky as I get – the
aesthetics of the intermediate calculations. To me, the "cont" side
conditions above feel out of place, as they hold already by the types
and simple rule of composition.
Also, to the reader, a "by simp" at the end could potentially do many
things, where a "finally show ?thesis." tells the reader that nothing
fancy is happening at the end.
But as I said, its mostly code aesthetics: worth asking if there is a
nicer way – not worth worrying about if there is not.
as the calculation at the end will be the unhelpful theorem
cont (λa. a) ⟹ cont (λa. a) ⟹ a ⊑ a.
can I avoid that?
Did you try to specify some particular rules for particular 'also' steps?
There is a notation with round parenthese described in the isar-ref
manual.
Thanks, I didn’t know that before (and I must have overread that part in
the docs). I think I’ll play around with that.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:28):From: Makarius <makarius@sketis.net>
In some sense the side conditions are deferred to the very end, and thus
displaced. The final "by simp" can make this feel a bit wobbly, since it
dilutes the application of the last fact, with the solving of the side
conditions.
This can be refined: a "." merely abbreviates "by this", and the latter
can have a terminal method for the solving of the remainder:
...
finally show ?thesis by this simp_all
or
...
finally show ?thesis by this auto
The proof method "this" does not appear very often under its proper name
in Isar proofs, but it is a perfectly normal structured method like
"rule".
Makarius
Email Gateway (Aug 19 2022 at 14:28):From: Joachim Breitner <breitner@kit.edu>
Hi,
that’s a good suggestion. I now use
finally show ?thesis by this (intro cont2cont)+
everywhere, and (at least to the adept reader), this signals „The
conclusion of the calculation is used unmodified, while the accumulated
side conditions are all of the form "cont something" and solved using
the usual cont2cont rules.
This even composes well with the few cases where I had
finally show ?thesis by (rule foobar)
which now simply become
finally show ?thesis by (rule foobar) (intro cont2cont)+
(I am a big fan of "intro"; I find it the most predictable method beyond
single-stepping with rule and subst).
Greetings,
Joachim
signature.asc
Last updated: Apr 26 2024 at 12:28 UTC