使用歸納時保存信息？

我正在使用Coq Proof Assistant來實現（小）編程語言的模型（擴展了Bruno De Fraine，Erik Ernst，MarioSüdholt的Featherweight Java的實現）。在使用induction策略時不斷出現的一件事是如何保留包裝在類型構造函數中的信息。使用歸納時保存信息？

我有一個子打字道具實現爲

Inductive sub_type : typ -> typ -> Prop := 
| st_refl : forall t, sub_type t t 
| st_trans : forall t1 t2 t3, sub_type t1 t2 -> sub_type t2 t3 -> sub_type t1 t3 
| st_extends : forall C D, 
    extends C D -> 
    sub_type (c_typ C) (c_typ D). 

Hint Constructors sub_type.

其中extends是看到的Java類的擴展機制，並typ代表了兩種不同的可用類型，

Inductive typ : Set := 
| c_typ : cname -> typ 
| r_typ : rname -> typ.

的我想要保存的類型信息的示例是在使用induction策略時使用的假設，如

H: sub_type (c_typ u) (c_typ v)

E.g.在

u : cname 
v : cname 
fsv : flds 
H : sub_type (c_typ u) (c_typ v) 
H0 : fields v fsv 
============================ 
exists fs : flds, fields u (fsv ++ fs)

使用induction H.丟棄約u和v的所有信息。該st_refl情況變得

u : cname 
v : cname 
fsv : flds 
t : typ 
H0 : fields v fsv 
============================ 
exists fs : flds, fields u (fsv ++ fs)

正如你可以看到u和v都涉及到typ構造中H，從而給t，丟失的信息。更糟糕的是，由於該Coq無法看到u和v在這種情況下實際上必須相同。

當使用inversion策略H Coq成功看到u和v是相同的。然而，這種策略在此不適用，因爲我需要induction生成的歸納假設來證明st_trans和st_extends個案。

是否有一種策略結合了最好的inversion和induction來生成歸納假設並派生出平等而不破壞有關構造函數中包含的信息？或者，有沒有辦法手動派生我需要的信息？ info inversion H和info induction H都顯示自動應用了很多轉換（尤其是inversion）。這些讓我嘗試了change策略以及let ... in構建，但沒有任何進展。

來源

2010-12-23 mdiin

當您需要使用參數具有特定結構（c_typ u）的依賴類型（sub_type (c_typ u) (c_typ v)）的假設進行歸納時，這是一個常見問題。有一個普遍的技巧，就是有選擇地將結構化參數重寫爲變量，保持環境中的平等。

set (t1 := c_typ u) in H; assert (Eq1 : t1 = c_typ u) by reflexivity; clearbody t1. 
set (t2 := c_typ u) in H; assert (Eq2 : t2 = c_typ u) by reflexivity; clearbody t2. 
induction H. (*often "; try subst" or "; try rewrite Eq1; try rewrite Eq2" *).

由於Coq的8.2，這組共同-斷言clearbody圖案是通過內置的戰術remember term as ident in *goal_occurences*進行。

這是一個愚蠢的引理證明使用這種策略。

Lemma subtype_r_left_equal : 
    forall r1 t2, sub_type (r_typ r1) t2 -> r_typ r1 = t2. 
Proof. 
    intros. 
    remember (r_typ r1) as t1 in H. 
    induction H. 
    congruence. 
    solve [firstorder]. 
    discriminate. 
Qed.

特別提示（從經驗，但它已經有一段時間，所以我不記得細節）：當你正在做的類型系統相當語法推理（這往往是這樣，當你做這些類型的機械證明），可以方便地繼續輸入Set中的判斷。想想打字派生作爲你推理的對象。我記得那些在打字派生中引入平等的方便的例子，這在Prop中並不總是與打字派生一起工作。

隨着你的Problem.v，這裏是一個反身案件的證明。對於傳遞性，我懷疑你的歸納假設不夠強。這可能是您簡化問題方式的副產品，儘管傳遞性往往需要令人驚訝地涉及誘導假設或引理。

Fact sub_type_fields: forall u v fsv, 
    sub_type (c_typ u) (c_typ v) -> fields v fsv -> 
    exists fs, fields u (fsv ++ fs). 
Proof. 
    intros. 
    remember (c_typ u) as t1 in H. 
    remember (c_typ v) as t2 in H. 
    induction H. 
    (* case st_refl *) 
    assert (v = u). congruence. subst v t. 
    exists nil. rewrite <- app_nil_end. assumption. 
    (* case st_trans *) 
    subst t1 t3. 
    (* case st_extends *) 
Admitted.

來源

2010-12-23 21:06:33 Gilles

@Matthias：是否泛化相關的H0。感應H.`幫助？這是我無法提供給Coq自己的東西所能提供的所有東西（您的問題缺少更多的定義，我不願意填寫，我對Java的類型系統不夠熟悉）。 – Gilles 2010-12-24 11:52:38

這並沒有說服Coq做正確的事情。我創建了一個zip文件，其中只包含了使用`Fact`所必需的定義，我無法證明：[Problem.v包含定義和`Fact`，其餘部分是輔助]（http://cs.au。 DK /〜MDI/coq_keeping_type_info_distilled.zip）。我感謝您的幫助。 – mdiin 2010-12-24 12:53:04

我遇到了類似的問題，而Coq 8.3的「依賴感應」策略照顧到了業務。

來源

2011-02-04 15:04:13

我確信CPDT在這個問題上有一些評論，但它並不完全明顯。這裏有一些鏈接：

http://adam.chlipala.net/cpdt/html/Cpdt.Predicates.html節「與隱等式謂詞」表示也許在那裏勒柯克「丟失信息」非常簡單的情況下它也解釋了爲什麼該信息（在自毀，而不是誘導。）丟失：當您破壞應用於非自由變量參數的類型時，首先將這些類型替換爲自由變量（這就是爲什麼Coq丟失信息的原因。）
http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html「避免公理的方法」部分顯示一些避免公理K的技巧，包括吉爾斯描述的「平等把戲」。搜索「使用常見的基於平等的帽子戲法，對非可變參數支持感應輸入家庭」

我認爲這種現象是密切相關的相關模式匹配。

來源

2016-05-01 06:00:32

使用歸納時保存信息？

回答

相關問題