가설을 반복하는 coq 전술을 구현하려면 어떻게해야합니까?</p> <pre><code>Parameter C: Prop. Definition blah := C. </code></pre> <p>내가 자동으로 목표의 모든 가정에 <code>blah</code>을 펼치는 전술을 구현하고 싶습니다 : 내 일반적인 질문에 대한

Question

으로 최소한의 예를 들어, 우리는 다음과 같은 있다고 가정합니다.

Ltac my_auto_unfold := repeat match goal with 
    | [ H: ?P |- ?P ] => unfold blah in H 
end. 


Theorem g: blah -> blah -> blah. 
Proof. 
intros. 
my_auto_unfold. 

그러나 하나 개의 가설이 펼쳐 blah했다 :

나는이 시도.

Answer 1

나는 progress 전술을 찾고 있을지도 모른다고 생각합니다. 이렇게하면 :

두 가설 모두에서 펼쳐질 것입니다. 다음을 수행 할 수도 있습니다.

Ltac in_all_hyps tac := 
    repeat match goal with 
      | [ H : _ |- _ ] => progress tac H 
      end. 

이 패턴을 일반화합니다. 이것은 각 가설에서 여러 번 전술을 실행할 수 있습니다.

---

당신은 순서대로, 한 번에 모든 가설을 통해 실행하려면

,이 (당신이 EVAR 컨텍스트를 보존하고 증거 용어 바보 같은 물건을 추가 할 할 경우 특히) 상당히 어렵습니다.

Parameter C: Prop. 
Definition blah := C. 

Definition BLOCK := True. 

Ltac repeat_until_block tac := 
    lazymatch goal with 
    | [ |- BLOCK -> _ ] => intros _ 
    | [ |- _ ] => tac(); repeat_until_block tac 
    end. 
Ltac on_each_hyp_once tac := 
    generalize (I : BLOCK); 
    repeat match goal with 
     | [ H : _ |- _ ] => revert H 
     end; 
    repeat_until_block 
    ltac:(fun _ 
      => intro; 
      lazymatch goal with 
      | [ H : _ |- _ ] => tac H 
      end). 

Theorem g: blah -> blah -> fst (id blah, True). 
Proof. 
    intros. 
    on_each_hyp_once ltac:(fun H => unfold blah in H). 

아이디어는 당신이 목표에 위치를 (표시 더미 식별자를 삽입하는 것입니다 : 여기에 (당신의 전술을 가정하는 것을 목표로 혼란을하지 않는) 것을 할 수있는 빠른 - 및 - 더러운 방법입니다 즉, 얼마나 많은 변수가 도입 될 수 있는지 표시하기 위해), 모든 문맥을 목표로 되돌려 놓습니다. 그러면 방금 소개 한 각 가설에 대한 전술을 실행하면서 문맥 가설을 한 번에 다시 도입 할 수 있습니다.

Answer 2

스 니펫의 문제는 [ H: ?P |- ?P ]이이 경우 항상 일치한다는 것입니다. 처음으로 H : blah과 일치하며 두 번째로는 H : C과 일치합니다. C는 공백에서 전환 가능하며 펼쳐서 아무 것도 바뀌지 않으므로 repeat을 중단합니다.

나는 당신이 그렇게 원하는 경우도

Theorem g: blah -> blah -> blah. 
Proof. 
    intros. 
    match goal with 
    | [ |- ?p] => my_auto_unfold p 
    end. 
    auto. Qed. 

를 작성할 수

Ltac my_auto_unfold nam := repeat lazymatch goal with 
    | [ H : nam |- _ ] => unfold nam in H 
end. 

Theorem g: blah -> blah -> blah. 
Proof. 
intros. 
my_auto_unfold blah. auto. Qed. 

작성합니다.