standard library에 있는 lemma 를 활용해도 되나요?

[shwlinux]

Coq.Arith.Plus ( http://www.lix.polytechnique.fr/coq/stdlib/Coq.Arith.Plus.html )와 같은 곳에 정의 되어 있는 다양한 lemma들을 활용해도 되나요?

물론 예를 들어 n + m = m + n 을 증명할 때

rewrite -> plus_comm. reflexivity.

와 같이 사용하면 안되겠지만,

증명하는데 도움이 되는 lemma라면 사용해도 괜찮은지 궁금합니다.

[jeehoonkang]

@shwlinux To use those lemmas, you should import the module. However, it is not allowed to import any module other than D.

[shwlinux]

네 알겠습니다! 이미 다른 것들 임포트해서 과제 제출했는데 다시 수정해서 제출하겠습니다

[markshin]

D를 제외한 다른 모듈을 import 하는게 안 된다고 하셨는데 만약에 8번을 푸는데 7번에서 증명한 것이 필요한 경우 Require Export P07.

이렇게 사용하는것은 괜찮나요?

[jeehoonkang]

아니되옵니다.

[Sooram]

그럼 7번에서 증명했던 것을 8번에서 lemma로 그대로 복사해서 사용해도 되나요?

[jeehoonkang]

@Sooram 되옵니다.

[nimooj]

@jeehoonkang 조교님, 그럼 예를 들어 1번에서 증명한 theorem을 나머지 문제들을 풀 때 복사해서 사용해도 된다는 말씀이시죠?

[jeehoonkang]

@nimooj 예..!

[nimooj]

@jeehoonkang 감사합니다:)