重寫戰術未能找到模式匹配

在勒柯克短期內發生，我有在以下情況下應用rewrite戰術問題：重寫戰術未能找到模式匹配

Section Test. 

Hypothesis s t  : nat -> nat. 
Hypothesis s_ext_eq_t : forall (x : nat), s x = t x. 

Definition dummy_s : nat -> nat := 
    fun n => match n with 
     | O => 42 
     | S np => s np 
     end. 

Definition dummy_t : nat -> nat := 
    fun n => match n with 
     | O => 42 
     | S np => t np 
     end. 

Goal forall (n : nat), dummy_s n = dummy_t n. 
Proof. 
    intro n. unfold dummy_s. unfold dummy_t.

在這個階段，當地的情況和當前的目標看起來像是如下：

1 subgoals, subgoal 1 (ID 6) 

s : nat -> nat 
t : nat -> nat 
s_ext_eq_t : forall x : nat, s x = t x 
n : nat 
============================ 
match n with 
| 0 => 42 
| S np => s np 
end = match n with 
     | 0 => 42 
     | S np => t np 
     end

現在，應該是可以應用的rewrite戰術由t np取代的s np的發生的目的，從而能夠解決使用目標。然而，

rewrite s_ext_eq_t.

給

Toplevel input, characters 0-18: 
Error: Found no subterm matching "s ?190" in the current goal.

我在做什麼錯？一個可以進入的情況下rewrite通過

destruct n. 
    (* n = 0 *) 
    reflexivity. 
    (* n > 0 *) 
    rewrite s_ext_eq_t. 
    reflexivity. 
Qed.

，但我面對的，幾個這樣的自毀是必要的實際情況是適用的，我不知道是否rewrite或它的變體是能夠做到這自動。

補遺上述情況證明通過充分理由遞歸具有期望的固定點屬性中定義的函數時自然地發生：

假設A: Type和R: A -> A -> Prop是一個良基關係，即我們有Rwf: well_founded R。然後，給定一個類型的家庭P: A -> Type我們可以通過遞歸在R構造部分

Fix : forall (x : A), P a

，以給出一個函數的遞歸步驟

F : forall x:A, (forall y:A, R y x -> P y) -> P x

見https://coq.inria.fr/library/Coq.Init.Wf.html然而，就表明Fix確實有定點屬性

forall (x : A), Fix x = F (fun (y:A) _ => Fix y)`

我們需要提供一個見證

F_ext : forall (x:A) (f g:forall y:A, R y x -> P y), 
      (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.

即我們必須表明，F不使用任何從給定的f: forall y:A, R y x -> P y但其值別的。當然，在任何具體的情況下，這應該是微不足道的驗證，但是當一個人試圖證明它時，就會遇到一個我上面介紹的最小例子：一個人面臨兩個代碼副本的巨大平等對於遞歸步驟，一次使用f，另一次使用g。你的假設告訴f和g是延伸平等的，所以應該能夠重寫它們。然而，在遞歸步驟的代碼中，可能會有大量的模式匹配和新的變量在本地上下文中是沒有意義的，因此它會是（不必要的）？在生成之前幾十次非常繁瑣允許申請rewrite。

來源

2015-04-18 Hanno

我覺得'np'不是一個子項，因爲np是一個模式變量，所以'rewrite'不起作用。使用'destruct'可以創建重寫的具體子項，所以我會盡可能使用它：'destruct n; auto.'或者，如果你假設'功能擴展性'，那麼你可以做'要求導入功能擴展性。用t代替s; auto使用functional_extensionality.'但你可能不想引入額外的公理。所以有可能有更好的方法來做到這一點... – larsr

@larsr：謝謝你的評論。然而，我仍然想知道是否已經或者可以實施一種策略來自動化這個銷燬過程，從而允許在目標的任何子表達式*上使用「重寫」，即使它在當前沒有很好的類型當地情況。 – Hanno

如上文的評論中提到，它是不可以直接在match語句的分支進行重寫，因爲np不是在頂級的環境範圍。就Coq的理論而言，您的陳述的證明必須在某個時刻破壞n。

雖然我不知道自動化此類問題的任何戰術，這是不是太硬拿出解決您的問題沒有太多的痛苦了一些自定義LTAC代碼：

Ltac solve_eq := 
    try reflexivity; 
    match goal with 
    | |- match ?x with _ => _ end 
     = match ?x with _ => _ end => 
    destruct x; auto 
    end. 

Goal forall (n : nat), dummy_s n = dummy_t n. 
Proof. 
    intro n. unfold dummy_s. unfold dummy_t. 
    solve_eq. 
Qed.

如果您外延平等結果是出現在你的上下文中的假設，那麼應該能夠解決這個形狀的許多目標;如果不是，則可能需要向提示數據庫添加額外的引理。

來源

2015-04-19 18:33:00

謝謝 - 抱歉，我很晚回答！ – Hanno

重寫戰術未能找到模式匹配

回答

相關問題