Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Strange "Tactic failed" error in lift_definiti...


view this post on Zulip Email Gateway (Jan 10 2021 at 10:38):

From: Florian Märkl <isabelle-users@florianmaerkl.de>
Hello,

I just encountered some strange behavior when using the (code_dt) flag
of lift_definition as in this example:

typedef imc = "{mc :: nat. True ∧ True}" by simp
setup_lifting type_definition_imc
lift_definition (code_dt) lift_imco :: "nat ⇒ imc option" is Some by simp

This throws the following error at the "by simp" of the lift_definition
(even sorry does the same):

Tactic failed
The error(s) above occurred for the goal statement⌂:
rel_fun (eq_onp (pred_option (λmc. True ∧ True))) (eq_onp (λmc. True ∧
True)) (case_option (Rep_imc undefined) (λx2. x2)) (case_option (Rep_imc
undefined) (λx2. x2))

I'm not really sure what it is trying to tell me, the only suspicious
thing I can spot are the two "undefined"s in the goal.
What's funny is that if I make the predicate for the imc type just
"True" instead of "True ∧ True", it works. Is that a bug or maybe just a
limitation of how the lifting works there?

For a bit of context, I am using something similar to this in a project
where I have to construct an abstract type with invariants directly from
its base representation. I do this by checking the invariants on the
base type and returning an option type of the abstract type that will be
None whenever the invariants are not fulfilled. I also need (code_dt) to
generate code from it.
There, my typedef initially looked something like this:

typedef imc = "{mc :: nat. invar_a mc ∧ invar_b mc ∧ ...}

I just fixed it there by wrapping the conjunction in a single definition
so it's not a blocker for me but I would still be interested whether
there is a solution or if it's a bug.


Last updated: Jul 15 2022 at 23:21 UTC