運用戰術分號鏈的本地子目標在勒柯克

假定我們有定義運用戰術分號鏈的本地子目標在勒柯克

Inductive sillyA : nat -> Prop := 
| sA0 : sillyA 0 
| sA1 : sillyA 1. 

Inductive sillyB : nat -> Prop := 
| sB0 : sillyB 0 
| sB1 : sillyB 1. 

Inductive sillyC (n : nat) : Prop := 
| sC0 : sillyA n -> sillyC n 
| sC1 : sillyA n -> sillyC n.

，並想證明

Theorem silly : forall n, sillyC n -> sillyB n.

通過案例分析的簡單證明是

intros. inversion H; inversion H0. 
apply sB0. apply sB1. 
apply sB0. apply sB1.

但這裏有一個明顯的重複apply sB0. apply sB1.。

問題：除了定義新的戰術符號外，最好的方法是什麼？

使用T; [T1 | ... Tn]不能幫助，因爲

intros. inversion H; inversion H0; 
[apply sB0 | apply sB1].

有錯號碼的戰術，和正確的形式

intros. inversion H; inversion H0; 
[apply sB0 | apply sB1 | apply sB0 | apply sB1].

是不是有所改善的。我們需要的是一種類似於T; [T1 | ... Tn]的策略，但僅將[T1 | ... Tn]僅應用於由緊接的前面的策略T生成的子策略，而不是整個分號鏈。如果我們有這樣的招數T; <T1 | ... Tn>，我們可以進一步縮短上面

intros. inversion H; inversion H0; 
<apply sB0 | apply sB1>.

這是可能的證明？

來源

2014-11-03 user287393

分組將做到這一點：

Theorem silly : forall n, sillyC n -> sillyB n. 
intros. inversion H; (inversion H0; [apply sB0 | apply sB1]).

來源

2014-11-03 04:24:41 jbapple

你介意回答極少跟進？我處於戰術'T'，'Ta'和'Tb'分爲2個子目標的情況。我想先申請'T'，將'Ta'應用於從T'開頭的第一個子目標，'Tb'到第二個子目標。然後對第一個子目標應用策略'T1'，從*'Ta'和'Tb'，然後'T2'到第二個子目標。所以沒有';'證明是'T.助教。 T1。 T2。 TB。 T1。 T2.'這也可以通過分組來重構嗎？我能得到的最好的是'T; [（Ta; [T1 | T2]）| （Tb; [T1 | T2]）]'，而我希望得到'T; （[Ta | Tb]; [T1 | T2]）「（它不起作用，但你明白了。） – user287393 2014-11-03 08:20:03

」它不起作用，但你明白了。我不得不說，我不知道。我建議你發佈一個新的問題，並且你還會學習其他的術語，如'repeat'，'try'和'||'，這些都可能有所幫助。 – jbapple 2014-11-04 03:42:27

運用戰術分號鏈的本地子目標在勒柯克

回答

相關問題