在勒柯克

感應一套感應子我有三個構造內置的感應設置：在勒柯克

Inductive MF : Set := 
| D : MF 
| cn : MF -> MF -> MF 
| dn : Z -> MF -> MF.

我想以某種方式定義一個新的感應集B，在B MF的僅包含一個子集從D和dn獲得的元素。此外，如果需要，B中的所有內容都應解釋爲MF型。

我試圖限定第一B，然後MF如下：

Inductive B : Set := 
| D : B 
| dn : Z -> B -> B. 

Inductive MF : Set := 
| m : B -> MF 
| cn : MF -> MF -> MF 
| Dn : Z -> MF -> MF. 
Axiom m_inj : forall (a b : B), m a = m b -> a = b. 
Coercion m : B >-> MF. 
Axiom dnDn : forall (a : B)(i : Z), (m (dn i a)) = (Dn i (m a)).

這裏的問題是，我必須構造（DN和Dn）應該是可互換的相對於在B中的元件這使我在進一步發展中存在很多問題，爲了達到預期的行爲，我必須不斷添加公理。

來源

2016-02-09 EHM

請注意，您必須證明isB mf坐落在您的設置無關的證明，否則勒柯克不會知道投影mf是單射。通常情況下，你想在MF平等意味着在您的子類B平等。

我建議以下變化：

Require Import Bool ZArith Eqdep_dec. 

Inductive MF : Set := 
    | D : MF 
    | cn : MF -> MF -> MF 
    | dn : Z -> MF -> MF. 

Inductive isB : MF -> Prop := 
    | DIsOK : isB D 
    | dnIsOK : forall z mf, isB mf -> isB (dn z mf). 

Fixpoint isBb (mf : MF) : bool := 
    match mf with 
    | D  => true 
    | dn _ mf => isBb mf 
    | _  => false 
    end. 

Lemma mfP mf : reflect (isB mf) (isBb mf). 
Proof. 
apply iff_reflect; split. 
+ elim mf; auto; simpl; intros mf1 ihmf1 mf2 ihmf2. 
    - now intros hisB; inversion hisB. 
    - now inversion ihmf2; rewrite mf2. 
+ now elim mf; simpl; try repeat (auto||constructor||congruence). 
Qed. 

Record B := mkB 
    { mf : MF 
    ; prf : isBb mf = true 
    }. 

Coercion mf : B >-> MF. 

(* From http://cstheory.stackexchange.com/questions/5158/prove-proof-irrelevance-in-coq *) 
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. 
Proof. 
intros; apply Eqdep_dec.eq_proofs_unicity; intros. 
now destruct (Bool.bool_dec x y); tauto. 
Qed. 

Lemma valB b1 b2 : mf b1 = mf b2 -> b1 = b2. 
Proof. 
destruct b1, b2; simpl; intros ->. 
now rewrite (bool_pirrel (isBb mf1) prf0 prf1). 
Qed.

數學-COMP庫中有超過布爾謂詞亞型偉大和系統的支持，你可能想給它一去，如果你發現自己處理很多亞型。

來源

2016-02-09 19:24:44 ejgallego

對不起，這麼晚回覆。我已經離線了一段時間。感謝您的詳細解答。我想我必須閱讀更多關於證據不相關的內容，因爲我不太熟悉它。我甚至沒有想到它。 – EHM

不客氣！證明不相關的想法很簡單：設想一個證明'p：存在k，P k'。在Coq中，證明是程序，所以實際上，我們可以在這裏有不同的程序'p'來實現期望的引理'存在k，P k'。然而，這意味着給出我們的引理'p1 p2的兩個證明：存在...'，我們不能證明'p1 = p2'。然而，在很多情況下，我們想要這樣做，因爲我們自己並不關心證據，只關心房產。這是證明不相關的時候。對於某些類證明，如上所述，可以派生出來，對於其他類，您需要使用公理。 – ejgallego

再次感謝！這聽起來像一個有趣的話題。我會牢記這一點。 – EHM

您可以將B定義爲包裝MF元素的記錄以及僅使用D和dn構建的證明。爲此，您需要首先定義一個謂詞isB : MF -> Prop，描述MF的元素，它們是B s。

Require Import ZArith. 

Inductive MF : Set := 
    | D : MF 
    | cn : MF -> MF -> MF 
    | dn : Z -> MF -> MF. 

Inductive isB : MF -> Prop := 
    | DIsOK : isB D 
    | dnIsOK : forall z mf, isB mf -> isB (dn z mf). 

Record B := mkB 
    { mf : MF 
    ; prf : isB mf 
    }. 

Coercion mf : B >-> MF.

來源

2016-02-09 11:23:58 gallais

這工作得很好！非常感謝你。 – EHM

回答

相關問題