Email Gateway (Aug 18 2022 at 16:01): Email Gateway (Aug 18 2022 at 16:01):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi all,
using the function package, I'd like to define a function whose
definition contains a number of Let expressions. In the generated
induction rule, a term "Let t (%x. y)" yields the induction hypothesis
"!!x. x = t ==> P (y x)"
However, I would like to get "P (y t)" directly. How do I have to change
the congruence rule for Let to achieve this?
I tried two alternatives with fundef_cong:
"[| M = N; f N = g N |] ==> Let M f = Let N g" raises an exception:
*** exception THM 1 raised (line 421 of "drule.ML"): COMP
*** At command "function".
"[| M = N; f M = g N |] ==> Let M f = Let N g" eliminates the
quantifier, but produces far to many induction hypotheses.
What is the right congruence rule for this?
Andreas
Email Gateway (Aug 18 2022 at 16:02):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Andreas Lochbihler wrote:
Andreas,
This seems easy enough using the functions in ch 5 of the Reference Manual
val iax = "!!x. x = t ==> P (y x)" : Thm.thm
val ax' = forall_elim_var 0 iax ;
val ax' = "?x = t ==> P (y ?x)" : Thm.thm
refl RS ax' ;
val it = "P (y t)" : Thm.thm
Cheers,
Jeremy
Email Gateway (Aug 18 2022 at 16:02):From: Alexander Krauss <krauss@in.tum.de>
Hi Andreas,
using the function package, I'd like to define a function whose
definition contains a number of Let expressions. In the generated
induction rule, a term "Let t (%x. y)" yields the induction hypothesis
"!!x. x = t ==> P (y x)"
However, I would like to get "P (y t)" directly. How do I have to change
the congruence rule for Let to achieve this?I tried two alternatives with fundef_cong:
- "[| M = N; f N = g N |] ==> Let M f = Let N g" raises an exception:*** exception THM 1 raised (line 421 of "drule.ML"): COMP
*** At command "function".
- "[| M = N; f M = g N |] ==> Let M f = Let N g" eliminates the
quantifier, but produces far to many induction hypotheses.What is the right congruence rule for this?
Actually, I had expected that the first rule works. I need to dig into
this again. The rule that should definitely work is the following
"f M = g N ==> Let M f = Let N g"
It has the same effect on the induction rule as unfolding all lets. Can
you try if it works for your function?
Jeremy Dawson wrote:
This seems easy enough using the functions in ch 5 of the Reference Manual
val iax = "!!x. x = t ==> P (y x)" : Thm.thm
val ax' = forall_elim_var 0 iax ;
val ax' = "?x = t ==> P (y ?x)" : Thm.thm
refl RS ax' ;
val it = "P (y t)" : Thm.thm
The ind.hyp. Andreas is referring to appears nested inside the induction
rule, where it cannot be easily manipulated by hand...
Alex
Email Gateway (Aug 18 2022 at 16:02):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Alex,
Actually, I had expected that the first rule works. I need to dig into
this again. The rule that should definitely work is the following"f M = g N ==> Let M f = Let N g"
It has the same effect on the induction rule as unfolding all lets. Can
you try if it works for your function?
No, it doesn't. This produces the same effect like the congruence rule
"[| M = N; f M = g N |] ==> Let M f = Let N g", it produces too many
induction hypotheses.
For example, with your congruence rule declared as fundef_cong, the
following equation in the definition of compE2 generates this induction
case:
"compE2 L ins pcs (if (e) e\<^isub>1 else e\<^isub>2) =
(let els = compE2 L ins pcs e\<^isub>2;
thn = compE2 L ins ((length els + 1) # pcs) e\<^isub>1;
cnd = compE2 L ins ((length thn + length els + 2) # pcs) e;
test = IfFalse (int (length thn) + 2);
thnex = Goto (int (length els) + 1)
in cnd @ [test] @ thn @ [thnex] @ els)"
!!L ins pcs e e\<^isub>1 e\<^isub>2.
[| ?P L ins pcs e\<^isub>2;
?P L ins ((length (compE2 L ins pcs e\<^isub>2) + 1) # pcs)
e\<^isub>1;
?P L ins pcs e\<^isub>2;
?P L ins
((length
(compE2 L ins
((length (compE2 L ins pcs e\<^isub>2) + 1) # pcs)
e\<^isub>1) +
length (compE2 L ins pcs e\<^isub>2) +
2) #
pcs)
e;
?P L ins pcs e\<^isub>2;
?P L ins ((length (compE2 L ins pcs e\<^isub>2) + 1) # pcs)
e\<^isub>1;
?P L ins pcs e\<^isub>2;
?P L ins ((length (compE2 L ins pcs e\<^isub>2) + 1) # pcs)
e\<^isub>1;
?P L ins pcs e\<^isub>2; ?P L ins pcs e\<^isub>2 |]
==> ?P L ins pcs (if (e) e\<^isub>1 else e\<^isub>2);
This seems easy enough using the functions in ch 5 of the Reference
Manual
[...]
The ind.hyp. Andreas is referring to appears nested inside the induction
rule, where it cannot be easily manipulated by hand...
Well, I managed to transform it, but it is not a satisfactory solution:
lemma meta_all_eq_conv:
"!!P b. (!!a. a = b ==> PROP P a) == PROP P b"
"!!P c. (!!a b. a = c ==> PROP P a b) == PROP P c b"
"!!P d. (!!a b c. a = d ==> PROP P a b c) == PROP P d b c"
"!!P e. (!!a b c d. a = e ==> PROP P a b c d) == PROP P e b c d"
thm compE2_compEs2.induct[unfolded meta_all_eq_conv]
I need one rewrite rule for every nesting level of let expressions.
Andreas
Email Gateway (Aug 18 2022 at 16:03):From: Jeremy Dawson <jlcaadawson@netspeed.com.au>
Yes, I see. How deeply is it nested ? If it is simply a hypothesis to
the theorem, rather than being nested more deeply, could you get what
you need in this way ?
val th = "(!!x. x = t ==> ?P (?y x)) ==> ?Q" : Thm.thm
val th' = rule_by_tactic (hyp_subst_tac 1) th ;
val th' = "(!!x. ?P (?y t)) ==> ?Q" : Thm.thm
Regards,
Jeremy
Email Gateway (Aug 18 2022 at 16:06):From: Alexander Krauss <krauss@in.tum.de>
Hi Andreas,
After playing the complete example that you provided off-list, I think I
now understood the problem.
The let binding itself contains recursive calls. Using the above
congruence rule is equivalent to inlining all lets for the purpose of
the analysis. This automatically duplicates recursive calls, if the
let-bound variable occurs more than once. I think there is no way to
avoid this using congruence rules.
The transformation you would like to see could in fact be done as a
post-processing step on the induction rule. Would you (and other users)
think it is a good idea to inline assumptions of the form "x = t" in
general?
Alex
Email Gateway (Aug 18 2022 at 16:06):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Alex,
Inlining might increase the size of the induction rule exponentially, so it
definitely is not optimal in all cases, i.e. you want to include an option to
deactivate this. In my cases, this increase does not happend in the induction
rule because contains fewer occurrences of the let-bound variable than the
defining equations. If postprocessing is needed anyway, I would recommend to
provide an attribute which perform this. Then, it might also be available for
other rules (e.g. the .cases rule for (co)inductive predicates/sets).
Since the function package does not generate sensible case names for the
induction rule (even without the sequential and every equation being given a
name), I have to do some postprocessing with attributes anyway, so I would not
mind adding an explicit postprocessing attribute there. Unfortunately, inside a
local context, IIRC, such an attribute would be reexecuted whenever the context
is opened.
Thanks for looking into this,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC