Coq：fが誘導コンストラクタである場合にのみf_equal戦術を適用する

Question

f_equal誘導コンストラクタを含む等価プルーフには、戦術が無条件に役立ちます。 a :: s = a' :: sはこのような目標になり、a = a'になります。

任意の機能で使用することは、別の話です。 4 mod 2 = 2 mod 2は4 = 2に減少しますが、これは明らかに不合理です。

自動的f_equal（または類似）を適用する方法があります場合、私は、例えば、それは情報を失わない場合にのみ思ったんだけど誘導コンストラクタ。ここで

Answer 1

はLTACのビットで誘導コンストラクタへf_equalを専門とする方法です：

Ltac f_equal_ind := 
    match goal with 
    | [ |- ?G ] => 
    tryif 
     (tryif assert (~ G); [ injection |] 
     then fail else idtac) 
    then 
     fail "Not an inductive constructor" 
    else 
     f_equal 
    end. 

Require Import List. 
Import ListNotations. 

Goal forall (a a' : nat) s, a :: s = a' :: s. 
intros. 
f_equal_ind. 
Abort. 

Require Import Arith. 

Goal 4 mod 2 = 2 mod 2. 
Fail f_equal_ind. 

(* The command has indeed failed with message: 
    In nested Ltac calls to "f_equal_ind" and "f_equal_ind", last call failed. 
    Tactic failure: Not an inductive constructor. *) 

私は結果は特に関与していると簡単な方法があった場合、私は驚かないだろうと言わなければなりません。私の考えは、否定された原始的な平等を期待するinjectionを使用して、原始的な平等に取り組んでいるかどうかをテストすることです。入れ子になったtryifは、assert (~ G); [ injection |]の部分がテストのためのものであるため、これが作成したサブゴールを保持したくないためです。