Coq에서 왜 Atom을 사용하고 어떻게 구성해야합니까?

Question

저는 현재 vellvm에서 변형을 개발하고 있습니다. 나는 코퀴인 초보자입니다. http://www.cis.upenn.edu/~plclub/popl08-tutorial/code/coqdoc/Atom.html

vellvm에서, 원자는 예를 들어, ID 및 라벨로 사용된다

이

은 원자 구현이다.

하나의 llvm 변환에 코드 블록을 삽입하고 싶다면 "atom"유형의 레이블을 지정해야합니다. 어떻게 Atom 레이블을 만들 수 있습니까?

내 질문을 좀 더 일반화하면 다음과 같습니다 : 1) 왜 누군가가 Atom을 사용하려고합니까? 2) 어떻게 구성 할 수 있습니까? 3) 이렇게하면 원자가 코드에서 다르게 사용될 수 있다는 점을 고려하는 데 어려움이 있습니까?

감사합니다.

편집 : 당신이 (Chargueraud 및 Aydemir에 의해) 지적 파일을 보면 ID에 대한 코드 및 레이블

Definition id := atom. (*r identities *) 
Definition l := atom. (*r labels *) 

Answer 1

, 당신은 원자 유형이이 이름을 지정하는 데 사용할 수있는 모든 유형을 나타내는 데 사용됩니다 이해 사물에.

atom_fresh_for_list 함수는 새 아톰을 작성하는 데 사용해야합니다. 이 함수의 유형은 임의의 원자뿐만 아니라 얻은 원자가 인수로 지정한 목록에 없다는 일부 증거를 반환 함을 나타냅니다. 이것은 새로운 것을 만드는 방법입니다 : 모든 오래된 것을리스트에 넣고, 그것과 함께 atom_fresh_for_list 함수를 호출합니다. 결과적으로 유형 {x : atom | ...}. 이것은 정확히 원자가 아닙니다. 더 많은 정보를 가진 원자입니다. 두 번째로, 다음 ... = atom_fresh_for_list 더 ...

을하고 "..."변수 V를 포함

하자 (V, H) : 당신은 서면에 의해 원자의 보류를 얻을 수 있습니다 원자와 당신이 그것을 사용할 수 있습니다. 이 원자가 새로운 것이라는 것을 증명해야한다면, 다른 변수 h를 사용할 수 있습니다.

이브

Answer 2

이브 단지 원자를 구성하는 방법의 예이없는, 부분적으로 대답 할 수 있었다. projT1을 사용해야합니다. 다음은이 코드입니다.

Definition an_atom : atom := (projT1 (atom_fresh_for_list nil)). 

여기서 nil은 모든 목록입니다.