Manuel Eberl (Jul 29 2022 at 11:53): Manuel Eberl (Jul 29 2022 at 11:53):That sounds a bit like someone registered something as a fundef_cong rule that isn't a well-formed fundef_cong rule. You could try looking through the list of fundef_cong rules and see if there's something with a <o in it:
declare [[ML_print_depth = 10000]]
ML ‹
Function_Context_Tree.get_function_congs @{context}
›
Or you could search through the files of your development (and the stuff it depends on) and see if they contain a fundef_cong declaration that looks dodgy.
Jan van Brügge (Jul 29 2022 at 12:25):Indeed, my custom map_cong rule shows up there, but I am pretty sure I never register it as a fundef_cong rule. The theorem itself is generated from ML
Manuel Eberl (Jul 29 2022 at 12:27):What happens if you do this before the function package invocation:
lemmas [fundef_cong del] = my_cong_rule
And what does this custom rule look like and how exactly do you generate it?
Jan van Brügge (Jul 29 2022 at 12:29):deleting the rule works, it lools like this:
|supp ?f1.0| <o |UNIV| ⟹
bij ?f2.0 ⟹
|supp ?f2.0| <o |UNIV| ⟹
|supp ?g1.0| <o |UNIV| ⟹
bij ?g2.0 ⟹
|supp ?g2.0| <o |UNIV| ⟹
?x = ?ya ⟹
(⋀z1. z1 ∈ set1_τ_pre ?ya ⟹ ?f1.0 z1 = ?g1.0 z1) ⟹
(⋀z2. z2 ∈ set2_τ_pre ?ya ⟹ ?f2.0 z2 = ?g2.0 z2) ⟹
(⋀z3. z3 ∈ set3_τ_pre ?ya ⟹ ?f3.0 z3 = ?g3.0 z3) ⟹ (⋀z4. z4 ∈ set4_τ_pre ?ya ⟹ ?f4.0 z4 = ?g4.0 z4) ⟹ map_τ_pre ?f1.0 ?f2.0 ?f3.0 ?f4.0 ?x = map_τ_pre ?g1.0 ?g2.0 ?g3.0 ?g4.0 ?ya
Yeah so I'm not a function package expert, but my guess is that fundef_cong rules are not allowed to have preconditions.
Jan van Brügge (Jul 29 2022 at 12:31):how exactly do you generate it?
basically Goal.prove_sorry, but there is a huge amount of code, not all of it written by me and some also copy pasted from the datatype package. I will investigate where this rule is added to the fundef_cong set
Manuel Eberl (Jul 29 2022 at 12:32):Jan van Brügge said:
how exactly do you generate it?
basically
Goal.prove_sorry, but there is a huge amount of code, not all of it written by me and some also copy pasted from the datatype package. I will investigate where this rule is added to thefundef_congset
That bit is not so interesting; the interesting question is what you do with that thm value afterwards. Presumable you use something like Local_Theory.notes to actually store it in the background theory under some name?
Jan van Brügge (Jul 29 2022 at 12:32):ok, that was easy: (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
Jan van Brügge (Jul 29 2022 at 12:32):yes that was it
Manuel Eberl (Jul 29 2022 at 12:33):Yeah, Local_Theory.notes roughly corresponds to the lemma command, and like with the lemma command, you can give a bunch of attributes to apply to the theorem.
Manuel Eberl (Jul 29 2022 at 12:33):That said, the error message you got was pretty horrible and should be improved.
Manuel Eberl (Jul 29 2022 at 12:34):Perhaps one could even modify the fundef_cong attribute so that it either ignores malformed rules or throws an exception upon the declaration, and not at some later point when the thing is used.
Jan van Brügge (Jul 29 2022 at 12:38):that would probably be good. Thanks for pointing me to fundef_cong
Notification Bot (Jul 29 2022 at 12:38):Jan van Brügge has marked this topic as resolved.
Last updated: Apr 24 2024 at 20:16 UTC