Email Gateway (Aug 19 2022 at 16:58): Email Gateway (Aug 19 2022 at 16:58):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
theory Dummy
imports Main
begin
lemma " { 0..n::nat} = n*(n+1) div 2" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix n assume "?P n"
from this show "?P (Suc n)" by simp
qed
verifies the formula for this sum as expected, especially the simplifier solves the ”?P 0” case:
{0..0} = 0 * (0 + 1) div 2
However, when I pose that lemma directly, the simplifier cannot prove it:
lemma "{0..0} = 0 * (0 + 1) div 2"
apply simp
results in
{0..0} = 0 * 1 div 2
What is the difference between the two case?
Email Gateway (Aug 19 2022 at 16:58):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Gergely,
as usually: "Whatch your types!" ;)
This is exactly the reason why I typically prefer "Suc" over "_ + 1"
(then I'm sure that I have "nat"s and not just arbitrary numrals).
cheers
chris
Email Gateway (Aug 19 2022 at 16:58):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Buday,
Am Dienstag, den 20.01.2015, 14:25 +0100 schrieb Buday Gergely:
Hi,
theory Dummy
imports Mainbegin
lemma " { 0..n::nat} = n*(n+1) div 2" (is "?P n")
There is clearly something missing, I get a
Type unification failed: Clash of types "nat" and "_ set"
error. On the equation's left we have a set on the right a natural
number.
proof (induction n)
show "?P 0" by simp
next
fix n assume "?P n"
from this show "?P (Suc n)" by simp
qedverifies the formula for this sum as expected, especially the simplifier solves the ”?P 0” case:
{0..0} = 0 * (0 + 1) div 2
However, when I pose that lemma directly, the simplifier cannot prove it:
lemma "{0..0} = 0 * (0 + 1) div 2"
apply simpresults in
{0..0} = 0 * 1 div 2
What is the difference between the two case?
- Gergely
Email Gateway (Aug 19 2022 at 16:58):From: Lawrence Paulson <lp15@cam.ac.uk>
The problem that you are giving to Isabelle is more general than you imagine. Inserting an explicit type constraint “::nat” somewhere should make it all work.
Larry
Email Gateway (Aug 19 2022 at 16:58):From: "Elsa L. Gunter" <egunter@illinois.edu>
Dear Johannes,
I can't answer Gergely's question, but for you, you browser has
stripped a leading \<Sigma> from in front of the set.
---Elsa
Email Gateway (Aug 19 2022 at 16:59):From: David Cock <david.cock@inf.ethz.ch>
Check your operator precedence. From memory setsum_and friends need
parentheses. Occasionally distinct terms will print the same i.e.
pretty-print and parse are not perfect inverses.
David
Last updated: Nov 21 2024 at 12:39 UTC