Email Gateway (Aug 19 2022 at 12:31): Email Gateway (Aug 19 2022 at 12:31):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isabelle developers,
I usually find the commands code_thms and export_code very useful while I work on setting
up the code generator. In combination with the BNF codatatype command, however, they
sometimes abort with "Proof failed." It reliably happens if the iterator or recursor for
the codatatype is reachable in the code dependency graphs and I have forgotten to provide
code equations for them. Here's a minimal example for Isabelle2013-1:
theory Scratch imports "~~/src/HOL/BNF/BNF" begin
codatatype foo = Foo | Bar foo
code_datatype Foo Bar
code_thms foo_unfold
At code_thms, I get "Proof failed." and a huge goal state talking about the internal BNF
construction for the the foo instead of the usual list of theorems that I would like to
inspect. The same happens at export_code and value [code].
I know that code generation for codatatypes is not yet set up in Isabelle2013-1, so it is
kind of my own fault that I have forgotten to declare the relevent code equations.
Nevertheless, why does the code generator even try to prove anything at all? And how can
this fail?
Best,
Andreas
Email Gateway (Aug 19 2022 at 12:31):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
I did not inspect the code, but I guess it happens since internal proofs
are forked, which are only forced when the code generator is invoked.
Maybe the BNF gurus can tell you more.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:31):From: Dmitriy Traytel <traytel@in.tum.de>
That would imply that with
ML {* parallel_proofs := 0 *}
the error should occur at the codatatype command already. This is not
the case.
After some minimization it turns out that this has nothing to do with
codatatypes at all:
consts c :: "nat ⇒ bool"
consts b :: "bool"
definition "X = {(Kl :: nat set, lab) |Kl lab. ((∀kl∈Kl. b) ∧ (∀kl. kl ∉
Kl ⟶ b)) ∧ c lab}"
code_thms X
What is code_thms actually trying to prove?
Dmitriy
Email Gateway (Aug 19 2022 at 12:31):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
On 16.11.2013 13:14, Dmitriy Traytel wrote:
Am 16.11.2013 09:57, schrieb Florian Haftmann:
Hi Andreas,
theory Scratch imports "~~/src/HOL/BNF/BNF" begin
codatatype foo = Foo | Bar foo
code_datatype Foo Bar
code_thms foo_unfoldAt code_thms, I get "Proof failed." and a huge goal state talking about
the internal BNF construction for the the foo instead of the usual list
of theorems that I would like to inspect. The same happens at
export_code and value [code].
I did not inspect the code, but I guess it happens since internal proofs
are forked, which are only forced when the code generator is invoked.
Maybe the BNF gurus can tell you more.
That would imply that withML {* parallel_proofs := 0 *}
the error should occur at the codatatype command already. This is not
the case.After some minimization it turns out that this has nothing to do with
codatatypes at all:consts c :: "nat ⇒ bool"
consts b :: "bool"
definition "X = {(Kl :: nat set, lab) |Kl lab. ((∀kl∈Kl. b) ∧ (∀kl. kl ∉
Kl ⟶ b)) ∧ c lab}"
code_thms XWhat is code_thms actually trying to prove?
Interesting. The code generator internally only does rewriting and
instantiation, no backward proofs, except for case certificates
(Pure/Isar/code.ML):
fun case_cong thy case_const (num_args, (pos, _)) =
let
val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
val (ws, vs) = chop pos zs;
val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
val Ts = binder_types T;
val T_cong = nth Ts pos;
fun mk_prem z = Free (z, T_cong);
fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]);
in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl tac end;
But this should hold regardless of the logical properties of the case
combinator.
Have you tried to obtain a traceback?
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:32):From: Dmitriy Traytel <traytel@in.tum.de>
I tried to do it now (see below). It points to the
set_comprehension_simproc that is installed as a code preprocessor in
Product_Type:
setup {*
Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
[Raw_Simplifier.make_simproc {name = "set comprehension", lhss =
[@{cpat "Collect ?P"}],
proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
*}
Dmitriy
Exception trace - Proof failed.
1. \<And>a ba aa baa. (aa, baa) \<in> (\<lambda>Kl. Kl)
(\<lambda>Kl. Kl) {Kl. \<forall>kl\<in>Kl. b} \<times> UNIV \<inter>
(\<lambda>Kl. Kl) (\<lambda>Kl. Kl) {Kl. \<forall>kl. kl \<notin> Kl
\<longrightarrow> b} \<times> UNIV \<inter> UNIV \<times> (\<lambda>lab.
lab) Collect c \<Longrightarrow> c baa
The error(s) above occurred for the goal statement:
{(Kl, lab) |Kl lab. ((\<forall>kl\<in>Kl. b) \<and> (\<forall>kl. kl
\<notin> Kl \<longrightarrow> b)) \<and> c lab} =
(\<lambda>(Kl, lab). (Kl, lab)) ((\<lambda>Kl. Kl) (\<lambda>Kl. Kl)
{Kl. \<forall>kl\<in>Kl. b} \<times> UNIV \<inter> (\<lambda>Kl. Kl)
(\<lambda>Kl. Kl) {Kl. \<forall>kl. kl \<notin> Kl \<longrightarrow>
b} \<times> UNIV \<inter> UNIV \<times> (\<lambda>lab. lab) ` {lab. c lab})
(line 10 of "/home/traytel/Scratch3.thy")
Goal.prove_common(7)result(1)
Goal.prove_common(7)
Set_Comprehension_Pointfree.conv(2)
Set_Comprehension_Pointfree.code_simproc(2)
Raw_Simplifier.rewritec(4)proc_rews(1)
Raw_Simplifier.rewritec(4)
Raw_Simplifier.bottomc(3)botc(3)
Raw_Simplifier.bottomc(3)try_botc(1)(1)
Code.eqn_conv(2)
Conv.fconv_rule(2)
List.map(2)()
Library.singleton(1)(1)
List.map(2)()
Basics.#>(1)(1)
Code_Preproc.obtain_eqns(3)
Code_Preproc.ensure_fun(5)
Code_Preproc.extend_arities_eqngr(5)
Code_Thingol.code_depgr(2)
Code_Thingol.code_thms(1)
Toplevel.apply_tr(3)(1)
Last updated: Nov 21 2024 at 12:39 UTC