Seul Baek (Nov 11 2018 at 17:17):
I'm encountering cases where I have a decidable prop
p that is also true (which I know because the decidability proof term
t : decidable p evaluates to
is_true ... when checked with the vm) but
exact dec_trivial fails to discharge the goal, with the message
exact tactic failed, type mismatch, given expression has type true but is expected to have type as_true (p)
Are there specific conditions under which this happens? I'm guessing that some definitions in the decidability proof term is not unfolding, but I'm not sure why.
This is really strange because it used to work for the exact cases that's broken now. This started happening after I reinstalled mathlib. I wonder if that has anything to do with it.
Seul Baek (Nov 11 2018 at 19:15):
More precisely : are there specific kinds of of definitions that might occur in a
t : decidable p that might prevent
as_true p from evaluating to
true? I'm trying
exact dec_trivial with various other decidable props, and it seems to have no problem reducing
as_true p to
truefor most choices of
p, so I'm wondering what's causing the difference.
Bryan Gin-ge Chen (Nov 11 2018 at 20:20):
Can you give a minimum (non)working example that illustrates the problem?
Seul Baek (Nov 11 2018 at 20:35):
In the first example
example : ∃ (x : int), (x = x) := begin lia.reify, lia.trim, lia.qelim, exact dec_trivial, exact dec_trivial, end
the second use of
exact dec_trivial fails now, although it used to work.
I'm trying to find a more minimal example that does not require a whole library to reproduce, but I'm having trouble isolating the exact point where it fails
Seul Baek (Nov 11 2018 at 20:46):
I think it would be easier to pinpoint the problem if I can see how far lean evaluates
as_true p before failing to match it with
true. Are there options for displaying this?
Mario Carneiro (Nov 11 2018 at 21:10):
what are the goals there?
Mario Carneiro (Nov 11 2018 at 21:11):
Proofs are irreducible, meaning that definitions by well founded recursion will fail to reduce when using
Seul Baek (Nov 11 2018 at 21:30):
I didn't use
well_founded in any of the definitions, if that's what you mean
Seul Baek (Nov 13 2018 at 00:40):
Oh I see what you mean. There was a non-structural recursion hiding in one of the defs
Seul Baek (Nov 13 2018 at 00:44):
Hunting these down isn't exactly fun though... a lot of time poring over the text output. Is there some option that displays all defs in a file/folder that use well-founded recursion?
Last updated: May 15 2021 at 00:39 UTC