Email Gateway (Aug 19 2022 at 08:54): Email Gateway (Aug 19 2022 at 08:54):From: Joachim Breitner <breitner@kit.edu>
Hi,
Am Donnerstag, den 04.10.2012, 10:57 +0200 schrieb Jasmin Blanchette:
Could you specify precisely which version of Nominal2 and of Isabelle you're using? I'm using the latest of both and get this error from Nominal2:
I am using 87d1e815aa59 for Nominal2, but it is reproducible with the
tarball from http://isabelle.in.tum.de/nominal/download; both on the
Isabelle2012 release.
That certainly sounds strange. Are the goals really identical, or is
one using metaequality and the other object-level equality?
Well, they looked identical... until Andreas told me about
using [[eta_contract=false]]
and now one (the working) has
⋀p∷perm. p ∙ (λa∷'a fset. fset a) = (λa∷'a fset. fset a)
and the other has
⋀p∷perm. p ∙ fset = fset
Sorry for the interruption, please carry on, nothing to see here,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 08:55):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Joachim,
Well, there is something to see here. Ideally, "metis" would behave the same modulo eta. I'll add this to my TODO list (and come back to it after a paper deadline).
Thanks for the report!
Regards,
Jasmin
Email Gateway (Aug 19 2022 at 09:03):From: Joachim Breitner <breitner@kit.edu>
Hi,
consider this theory, which uses Nominal2
theory strangemetis
imports "Nominal/Nominal/Nominal2"
begin
lemma "x ♯ d ⟹ x ♯ fset d"
using [[show_sorts]] [[show_consts]]
apply (erule fresh_fun_eqvt_app[rotated])
apply (rule eqvtI)
apply (rule eq_reflection)
by (metis fset_eqvt permute_fun_def permute_minus_cancel(1))
lemma "x ♯ d ⟹ x ♯ fset d"
apply (erule fresh_fun_eqvt_app[rotated])
using [[show_sorts]] [[show_consts]]
unfolding eqvt_def
apply rule
by (metis fset_eqvt permute_fun_def permute_minus_cancel(1))
Before the call to metis, the proof state is identical, at least as far
as I could get jedit to tell me about it:
proof (prove): step 4
goal (1 subgoal):
Nevertheless, in the first lemma, metis finds the proof sufficiently
fast, while in the second, it does not find any proof. As this is
probably not the intended behavior I was told to report that here.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 09:04):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Joachim,
consider this theory, which uses Nominal2
Could you specify precisely which version of Nominal2 and of Isabelle you're using? I'm using the latest of both and get this error from Nominal2:
*** Error (line 251 of "/Users/blanchet/misc/nominal2/Nominal/nominal_dt_alpha.ML"):
*** Type error in function application.
*** Function: Inductive.add_inductive_i :
*** inductive_flags ->
*** ((binding * typ) * mixfix) list ->
*** (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory -> inductive_result * local_theory
*** Argument: {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = ..., ...} :
*** {coind: bool,
*** no_ind: bool, no_elim: bool, verbose: bool, alt_name: binding, fork_mono: bool, skip_mono: bool, quiet_mode: bool}
*** Reason:
*** Can't unify {coind: bool, no_ind: bool, no_elim: bool, verbose: bool, alt_name: binding, skip_mono: bool, quiet_mode: bool}
*** to {coind: bool,
*** no_ind: bool, no_elim: bool, verbose: bool, alt_name: binding, fork_mono: bool, skip_mono: bool, quiet_mode: bool}
*** (Different number of fields)
*** At command "use" (line 27 of "/Users/blanchet/misc/nominal2/Nominal/Nominal2.thy")
Nevertheless, in the first lemma, metis finds the proof sufficiently
fast, while in the second, it does not find any proof. As this is
probably not the intended behavior I was told to report that here.
That certainly sounds strange. Are the goals really identical, or is one using metaequality and the other object-level equality?
Jasmin
Last updated: Apr 26 2024 at 01:06 UTC