When does dec_trivial fail for decidable and true props?

Stream: general

[Seul Baek]

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]

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]

Can you give a minimum (non)working example that illustrates the problem?

[Seul Baek]

https://github.com/skbaek/qe/blob/master/src/tests.lean

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]

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]

what are the goals there?

[Mario Carneiro]

Proofs are irreducible, meaning that definitions by well founded recursion will fail to reduce when using dec_trivial or rfl

[Seul Baek]

I didn't use well_founded in any of the definitions, if that's what you mean

[Seul Baek]

Oh I see what you mean. There was a non-structural recursion hiding in one of the defs

[Seul Baek]

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?