lean tutorial의 4 장을 통해 작업하고 있습니다.a = b → a + 1 = b + 1을 희박하게 증명하는 방법?
a = b → a + 1 = b + 1과 같은 단순한 동등성을 증명할 수 있고 싶습니다.은 calc 환경을 사용해야합니다. 내가 eq.subst를 사용하는 데 필요한 표준 라이브러리의 자연수에 평등에 대한 몇 가지 관련 보조 정리
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorry
내 추측하지만, I : 즉 I 명시 적으로 증명 용어를 구축하고 싶습니다 잃어 버렸어.
example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b := eq.subst H1 H2
당신은 당신이 함수에 동일한 입력을 제공 할 경우, 출력 값이 너무 동일합니다 의미 congr_arg 보조 정리
lemma congr_arg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) :
a₁ = a₂ → f a₁ = f a₂
를 사용할 수 있습니다 내가 찾을 수있는 가장 가까운 린 예는 이것이다 .
증거는 다음과 같이 진행됩니다
example (a b : nat) (H : a = b) : a + 1 = b + 1 :=
congr_arg (λ n, n + 1) H
참고, 그 린은 증거가 congr_arg _ H로 단순화 할 수 있도록 우리의 기능, λ n, n + 1 것을 추론 할 수있다. congr_arg는 일반적으로 좋은 해결책이지만
감사합니다. 실제로 작동하며 지금부터는 사용 방법을 알게 될 것입니다. 'congr_arg'. 그러나, 나는 'congr_arg'의 타입 선언을 이해하지 못합니다. 미지수는 다음과 같습니다. 1. 유니버스 변수'u v'. 마른 자습서에서 더 다루고 있습니까? 2.'Sort' 키워드. 이것들을 빨리 이해할 수있는 곳이 있습니까? 아니면 그냥 자습서를 참 아야합니까? –
우주 변수는 sect에서 다룹니다. 2.2 [기울기를 증명하는 정리] (https://leanprover.github.io/theorem_proving_in_lean/). [Issue # 1341] (https://github.com/leanprover/lean/issues/1341)은'Sort' 키워드에 대해 설명합니다. * 지금은 *이 미묘한 부분을 무시하고'congr_arg' 보조 정리를'a1 = a2'의 증명으로부터'fa1 = f a2'의 증명을 생성하는 함수로 생각할 수 있습니다. →'β'를 사용합니다.'Sort'는''α''와''β''가 어떤 타입인지 알려줍니다. HTH. –
,이 구체 예는 참 (congr_arg 내부적으로 사용) eq.subst + 고차 통일하여 해결 될 수있다.
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 :=
eq.subst H1 rfl
링크 된 튜토리얼은 * 린 2 *에 대한 것입니다. Lean의 현재 버전에 대한 문서는 http://leanprover.github.io/documentation/에서 찾을 수 있습니다. –
고마워요 @Kha, 자습서의 새롭고 향상된 버전이 포함되어 있습니다. https://leanprover.github.io/theorem_proving_in_lean/ (적어도 구현되지 않은 TODO는 제외) 전환하고 사용하겠습니다. 따라서. –
BTW,이 새로운 버전의 자습서는 매우 멋지며 마우스를 올려 놓았을 때의 용어 유형을 보여줍니다! –