물음표가있는 연산자에 대한 가설은 무엇입니까

Question

저는 지난 몇 주 동안 Coq 증명 보조원과 함께 일해 왔지만 오늘은 특별한 무엇인가를 겪었습니다. 벤자민 피어스 (Benjamin Pierce)의 "Types and programming languages"책의 연습을 통해 작업하고 있습니다. 이 실습 중 하나에서 특정 hoare 셋이 유효하다는 자체 제작 프로그래밍 언어 (Pier in의 연습 문제)에 대한 증명이 필요합니다. 나는이 증명을 거의 끝냈다. 그러나 나는 다음이 유효 함을 증명해야만하는 지점에 갇혀있다. st X <= st Y st는 어떤 상태이고, st X는 그 상태의 Id X에 저장된 값을 반환한다.

내 가설 상태 다음 : 지금

st : state 
H : (st X <=? st Y) = true 

내 질문은 무엇입니까? (st X <=? st Y) = true을 의미하며이 정리를 사용하여 목표를 증명할 수 있습니다 (거의 H와 같음)?

Answer 1

(n <=? m) = true <-> n <= m (가져 오기에 따라 다른 접두어가 필요할 수 있음)는 필요한 것은 apply Nat.leb_le입니다. 자연스러운 질문은, 어떻게 그걸 알아 내겠습니까?

처음에는 Print ident. (본문 표시) 또는 Check ident. (형식 만 표시 - 이론 정리에 유용함)으로 정의에 대한 정보를 얻을 수 있습니다. 그러나 <=?는 식별자없는 대신 그 정의 찾아야 그래서, 표기법입니다 : 다음

Locate "<=?". 
(* Notation 
    "x <=? y" := Nat.leb x y : nat_scope (default interpretation) *) 

을 우리는 관련 정리를 찾을 수 :

Search Nat.leb. 
(* ... (9 other theorems *) 
    Nat.leb_le: forall n m : nat, (n <=? m) = true <-> n <= m 
    ... 
*) 

우리는 또한 중간 단계를 건너 뛸 수 있습니다 보다 구체적인 검색을 수행하십시오. 표기법에 대해서는 따옴표가 필요합니다.

Search "<=?" true. (* ... (three other theorems) Nat.leb_le: forall n m : nat, (n <=? m) = true <-> n <= m *)