simp/auto/clarify에서 사용 된 파일 찾기

간단한 방법, 자동 방법 등에서 사용되는 보조 정리를 어떻게 찾을 수 있습니까?simp/auto/clarify에서 사용 된 파일 찾기

한 구체적인 경우에, 나는 같은 목표를 가지고 :

lemma "x ∉ dom S ⟹ Something" 
apply auto

및 auto을 적용한 후 내가 얻을 : ¬ Something ⟹ ∃y. S x = Some y합니다. 왜 전체 목표가 이렇게 바뀌 었는지 알아 내고 싶습니다. 그래서 재 작성에서 각 규칙을 삭제할 수 있습니다.

나는 이미 using [[simp_trace_new mode=full]] apply auto과 using [[simp_trace]] apply auto을 시도했지만, 정확히 auto이이 변환을 수행 한 원인에 대한 정보를 찾지 못했습니다.

출처

2017-03-01 peq

'auto'과'clarify' 당신의 보조 정리에 대한 몇 가지 고전적인 추론을하고 추적 할 수있는 쉬운 방법이있을 것 같지 않습니다 : 당신의 예에서

는 다음을 수행 할 것입니다. 또한'x ∉ dom S ⟹ Something'과'¬ Something ⟹ ∃y. S x = 일부 y '는 논리적으로 동일합니다. 보조 정리의 두 번째 형식으로 작업 할 수없는 이유는 무엇입니까? – ammbauer

전제로 'x ∉ dom S'를 사용하는 몇 가지 다른 단순화 규칙이 있으므로 오른쪽으로 이동하면 다른 단순화 규칙을 더 이상 사용할 수 없습니다. 나는 이제 모든 것을'S x = None'으로 바꿨지 만, 제 질문은 사용 된 보조 정리를 더 많이 보는 방법입니다. 고전적 추론에 대한 힌트를 주셔서 감사합니다. 나는 그것에 대해 생각하지 않았습니다. – peq

쉬운 방법이없는 것 같습니다. 메일 링리스트에서 이유를 물어볼 수 있습니다. – ammbauer

seL4 proof repo에서 얻을 수있는 apply_trace 명령이 있습니다.

lemma "x ∉ dom S ⟹ something" 
apply_trace auto 
(* It will show in the output box: 
used theorems: 
iffD2: ?P = ?Q ⟹ ?Q ⟹ ?P 
swap: ¬ ?P ⟹ (¬ ?R ⟹ ?P) ⟹ ?R 
domIff: (?a : dom ?m) = (?m ?a ~= None) 
not_None_eq: (?x ~= None) = (∃ y. ?x = Some y) 
*)

출처

2018-02-03 11:35:04

simp/auto/clarify에서 사용 된 파일 찾기

답변

관련 문제