Isabelle / HOL에 대한 초보자 질문이 있습니다.
다음과 같은 기본형을 증명하고 싶습니다.
lemma shows "{(x,y) . x ∈ {0..<n} ∧ y ∈ {0..<n} ∧ x = y} = {(x,x). x < n}"
그러나 증명 상태는 다음과 같습니다.
proof (prove) goal (1 subgoal): 1. {(x, y). x ∈ {0..<n} ∧ y ∈ {0..<n} ∧ x = y} = {(xa, x). x < n}
xa가 나타나는 이유는 무엇이며 올바른 (간결한) 방식으로 세트를 어떻게 정의 할 수 있습니까?
(x,y)세트에서 이해가 {(x,y). ....}되는 변수 이름을 바인딩 . 를 작성할 때 두 번째 변수 가 첫 번째 그림자 가 되는 두 개의 변수 {(x,x). x < n}를 바인딩 합니다.xx
{(x,x). x < n}실제로 람다 용어에 대한 좋은 구문입니다. 내부적으로는 Collect (case_prod (λx. λx. x < n)). 이런 식으로 용어를 보면 그림자가 더 분명합니다.
문제를 해결하려면 첫 번째와 두 번째 바운드 변수가 동일해야한다는 정보를 명시 적으로 표현해야합니다. 즉, {(x1,x2). x1 = x2 ∧ x1 < n}.
참고로 보여 주려는 기본형은 사실이 아닙니다. (예를 들어, n될 수 있습니다 int.) 당신이 원하는 경우 n로 nat, 당신은 예를 들어,이 명시 적으로 확인해야이 같은 목표의 유형을 제공함으로써 {(x,y). x ∈ {0..<(n::nat)} ∧ y ∈ {0..<n} ∧ x = y} = {(x1,x2). x1 = x2 ∧ x1 < n}.
특히 초보자라면 기본형 헤드에 구문을 사용하여 명시 적으로 자유 변수를 도입하는 것이 좋습니다 lemma Name: fixes n :: ‹nat› assumes ‹...› shows ‹...›.
이 기사는 인터넷에서 수집됩니다. 재 인쇄 할 때 출처를 알려주십시오.
침해가 발생한 경우 연락 주시기 바랍니다[email protected] 삭제
몇 마디 만하겠습니다