Re: [isabelle-dev] Problem with simproc enat_eq_cancel
On Fri, 1 Mar 2013, Andreas Lochbihler wrote: theory Scratch imports ~~/src/HOL/Library/Extended_Nat begin definition epred :: enat = enat where epred n = n - 1 lemma epred_iadd1: a ~= 0 == epred (a + b) = epred a + b apply(simp add: epred_def) I would have expected that the call to simp at least unfolds epred_def, but it raises the following error: *** Proof failed. *** (a + b - 1 = a - 1 + b) = (a + (b + - 1) = a + (- 1 + b)) *** 1. (a + b - 1 = b + (a - 1)) = (a + (b + - 1) = a + (b + - 1)) *** The error(s) above occurred for the goal statement: *** (a + b - 1 = a - 1 + b) = (a + (b + - 1) = a + (- 1 + b)) *** At command apply The simp trace with simp_debug enabled ends as follows: [1]Trying procedure Extended_Nat.enat_eq_cancel on: a + b - 1 = a - 1 + b simp_trace_depth_limit exceeded! These simprocs were introduced by Brian Huffman here: changeset: 45775:6c340de26a0d user:huffman date:Wed Dec 07 10:50:30 2011 +0100 files: src/HOL/Library/Extended_Nat.thy description: add cancellation simprocs for type enat We should Brian give time to comment on it (there is no need for real-time reactivity on isabelle-dev). He did all these renovations of the old simprocs, and this one seems to be derived from the same tradition. At the bottom of the ML sources, I recognize slightly odd things that I did myself in the mid 1990-ies, together with Larry. So in the worst case, I will look again eventually. By the way, why does the failure in the simproc yield a proof error at all? Usually, simp does not raise Proof failed if it gets stuck somewhere. This plain ERROR stems from Goal.prove here: http://isabelle.in.tum.de/repos/isabelle/annotate/d5b5c9259afd/src/Provers/Arith/extract_common_term.ML#l71 There is already a (* FIXME avoid handling of generic exceptions *) that is not as general to include ERROR as well. We used to have this odd odd catch-all programming style in the distant past, but you can never be sure if the patterns are sufficient or necessary. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem with simproc enat_eq_cancel
On Wed, Mar 6, 2013 at 7:18 AM, Makarius makar...@sketis.net wrote: On Fri, 1 Mar 2013, Andreas Lochbihler wrote: *** Proof failed. *** (a + b - 1 = a - 1 + b) = (a + (b + - 1) = a + (- 1 + b)) *** 1. (a + b - 1 = b + (a - 1)) = (a + (b + - 1) = a + (b + - 1)) *** The error(s) above occurred for the goal statement: *** (a + b - 1 = a - 1 + b) = (a + (b + - 1) = a + (- 1 + b)) *** At command apply The simp trace with simp_debug enabled ends as follows: [1]Trying procedure Extended_Nat.enat_eq_cancel on: a + b - 1 = a - 1 + b simp_trace_depth_limit exceeded! These simprocs were introduced by Brian Huffman here: changeset: 45775:6c340de26a0d user:huffman date:Wed Dec 07 10:50:30 2011 +0100 files: src/HOL/Library/Extended_Nat.thy description: add cancellation simprocs for type enat We should Brian give time to comment on it (there is no need for real-time reactivity on isabelle-dev). I just pushed a changeset to testboard that should fix the problem (abdcf1a7cabf). The issue was that the enat simprocs used the library function Arith_Data.dest_sum : term - term list to split sums; it treats subtraction x - y as equivalent to x + - y, which is not valid for enat. He did all these renovations of the old simprocs, and this one seems to be derived from the same tradition. Actually, the enat cancellation simprocs are not done in my new conversion-based style; these are just new instances of Larry's old extract-common-term simproc functor (Provers/Arith/extract_common_term.ML). - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Problem with simproc enat_eq_cancel
Dear all, in the repository (8a635bf2c86c) and in Isabelle2013, there seems to be something wrong with the enat_eq_cancel simproc in Extended_Nat. Can someone please look into this? Here's a minimal example: theory Scratch imports ~~/src/HOL/Library/Extended_Nat begin definition epred :: enat = enat where epred n = n - 1 lemma epred_iadd1: a ~= 0 == epred (a + b) = epred a + b apply(simp add: epred_def) I would have expected that the call to simp at least unfolds epred_def, but it raises the following error: *** Proof failed. *** (a + b - 1 = a - 1 + b) = (a + (b + - 1) = a + (- 1 + b)) *** 1. (a + b - 1 = b + (a - 1)) = (a + (b + - 1) = a + (b + - 1)) *** The error(s) above occurred for the goal statement: *** (a + b - 1 = a - 1 + b) = (a + (b + - 1) = a + (- 1 + b)) *** At command apply The simp trace with simp_debug enabled ends as follows: [1]Trying procedure Extended_Nat.enat_eq_cancel on: a + b - 1 = a - 1 + b simp_trace_depth_limit exceeded! When I disable the simproc, I am able to prove the lemma: using [[simproc del:enat_eq_cancel]] apply(cases a b rule: enat.exhaust[case_product enat.exhaust]) apply(simp_all add: epred_def eSuc_def one_enat_def zero_enat_def split: enat.splits) done By the way, why does the failure in the simproc yield a proof error at all? Usually, simp does not raise Proof failed if it gets stuck somewhere. Best, Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem with simproc enat_eq_cancel
On 01.03.2013 15:10, Andreas Lochbihler wrote: By the way, why does the failure in the simproc yield a proof error at all? Usually, simp does not raise Proof failed if it gets stuck somewhere. I guess this means that the simproc raises Proof failed which merely propagates through the simplifier. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
