Email Gateway (Aug 18 2022 at 12:18): Email Gateway (Aug 18 2022 at 12:18):From: Amine Chaieb <chaieb@in.tum.de>
Hi Perry,
The problem here the usual Suc/0 vs. numerals representation of things.
Function prod is written by pattern matching and its clauses are
normally aded to the simplifier. Now these match terms in your subgoals
only if they have the 0/Suc _ pattern. Obviously 3 is not such a
pattern, since it is internally some binary bit string.
One magic set of simp rules you can use here is "nat_number" which will
turn 3 into Suc (Suc (Suc 0)) after which, you can proceed the
simplification.
The same problem disturbs the proof of your second goal where you need a
subgoal saying that nat i = Suc (nat (i - 1)) since i >0, after this
your statement should be proved by simp.
In such cases, and only when I really need this, I derive a lemma saying
that prod n ... = (if n = 0 then ... else f (n) * prod (n - 1) ...)
this is better for evaluation by the simplifier.
Furthermore you can see the value of a function using value (just
interactive).
There are also methods which basically "prove" by evaluation.
Hope it helps,
Amine.
Perry James wrote:
Email Gateway (Aug 18 2022 at 12:18):From: Tobias Nipkow <nipkow@in.tum.de>
Furthermore you can see the value of a function using value (just
interactive).
Just to be clear on this one:
value "prod 3 1 (%x. x)"
yields "6".
Tobias
Last updated: May 03 2024 at 08:18 UTC