coqの帰納仮説を

Question

私は証明的文脈で仮説を反復的に逆転させるための戦術を定義することに問題があります。この証明を取得し、

H1 : search_tree (node a (node b ll lr) (node c rl rr)) 

と繰り返し仮説もちろん

H1 : search_tree (node a (node b ll lr) (node c rl rr)) 
H2 : search_tree (node b ll lr) 
H3 : search_tree (node c rl rr) 
H4 : lt_tree a (node b ll lr) 
H5 : gt_tree a (node c rl rr) 
H6 : lt_tree b ll 
H7 : gt_tree b lr 
H8 : lt_tree c rl 
H9 : gt_tree c rr 

を含む証明コンテキストを取得するための仮説を反転したいと思います。例えば、私のような仮説を含む証明コンテキストを持っていると仮定逆の戦術を繰り返し適用することで、文脈は簡単です。しかし、時には仮説を反転することによって、異なる仮説を異なるサブゴールに入れ、反転させるかどうかは、反転によって提供される情報の性質に依存する。

明らかな問題は、プルーフコンテキストに対して無差別にパターンマッチングすると、非終端を引き起こすことです。 1がそれらを反転した後、元の仮説を保持したい場合たとえば、次のように動作しません。

Ltac invert_all := 
    match goal with 
    | [ H1 : context [ node ?a ?l ?r ] |- ?goal ] => invert H1; invert_all 
    | _ => idtac 
    end. 

はこれを行う簡単な方法はありますか？明らかな解決策は、既に反転した仮説を積み重ねることです。別の解決策は、特定の深さまで仮説を逆転させることだけです。これはLtacの再帰呼び出しを削除します。それは本当にあなたが何をしたいなら

Answer 1

、私はあなたがすべて持っているそれまでは、これらすべてのサブツリーのリストを返すヘルパーFixpoint subtreelist (st : searchtree): list (...)、およびsubtreelistを呼び出し、その後戦術と再帰的にdestructのリストを証明するために最初にしたい疑いますあなたが望む余分な仮説。

これで幸運です！