린(증거 보조 장치)

린은 정리 프로베론과 프로그래밍 언어다.귀납형식을 가진 건축물의 미적분학을 바탕으로 한다.

린 프로젝트는 GitHub에서 주최하는 오픈소스 프로젝트다.레오나르도 드 모우라가 2013년 마이크로소프트 리서치에서 출시했다.^[1]

린은 다른 인터랙티브 정리 프로버들과 구별되는 인터페이스를 가지고 있다.린은 자바스크립트에 컴파일하여 웹브라우저로 접속할 수 있다.유니코드 기호를 기본적으로 지원한다.(이러한 것들은 "×"의 "\time"과 같은 LaTeX와 같은 시퀀스를 사용하여 입력할 수 있다.) 린도 메타 프로그래밍에 대한 폭넓은 지원을 받고 있다.

린은 수학자 토마스 헤일스와^[2] 케빈 버자드로부터 주목을 받았다.^[3]Hales는 그것을 그의 프로젝트인 Formal Obstracts에 사용하고 있다.버자드는 그것을 Xena 프로젝트에 사용한다.세나 프로젝트의 목표 중 하나는 린에 있는 임페리얼 칼리지 런던의 학부 수학 커리큘럼에서 모든 정리와 증거를 다시 쓰는 것이다.

예

린에서 자연수를 정의하는 방법은 다음과 같다.

귀납적 냇 : 유형   영 : 냇   굴복하다 : 냇 → 냇 

여기에 자연수에 대해 정의된 추가 작업이 있다.

정의 덧셈을 : 냇 → 냇 → 냇   n 영     := n   n (굴복하다 m) := 굴복하다(덧셈을 n m) 

이것은 임기 모드의 기울어진 간단한 증명이다.

정리 And_message : p ∧ q → q ∧ p :=     가정하다 h1 : p ∧ q,     ⟨h1.오른쪽, h1.좌측⟩ 

이 같은 증거는 전술로 달성할 수 있다.

정리 And_message (p q : 소품) : p ∧ q → q ∧ p := 시작되다     가정하다 h : (p ∧ q), -- p q가 사실이라고 가정함     경우들 h, -- 연결에서 개별 제안을 추출함     갈라지다, -- 목표를 두 가지 사례로 나누면 p와 q를 별도로 증명한다.     되풀이하여 말하다 { 가정하다 } 종지부를 찍다 

참고 항목

• 교정조수
• 유형 이론
• 종속형
• 콕
• 아그다
• 흉내를 내다

참조

외부 링크

• 린 웹사이트
• 린 커뮤니티 웹사이트
• Natural Number Game - 린을 배우기 위한 대화형 튜토리얼