如何在Coq中表示繼承？

如何獲取Coq中所有父元素？我在Coq的定義一組如下：如何在Coq中表示繼承？

Inductive Gen : Set := 
| BGen : nat -> nat -> Gen.

有許多實例，例如：

Definition g1 = BGen 1 2. 
Definition g2 = BGen 2 3.

現在，我想獲得的3父母元件，即[1,2]。我寫一個函數：

Fixpoint parents (c : nat) (l : list Gen) := 
match l with 
| [] => [] 
| (BGen p c') :: l' => if beq_nat c c' 
        then [p] 
        else parents c l' 
end.

我只能得到直接父的3 [2]，我怎樣才能讓所有的家長，如[1,2]在這個例子嗎？

來源

2017-10-20 Frank Sheng

爲什麼如果你找到了匹配而不是返回'p' *而返回'[p]'，而且還可以在列表的其餘部分找到其他匹配項？ – gallais

@gallais這可以通過用[p] :: parents c l'替換[p]來完成。但是，只有c的父母可以通過使用這個函數找到，我不能得到c的所有父母。 –

啊！看來我誤解了你的目標：你不僅要父母，還要父母的父母等？基本上你想建立一個閉包？ – gallais

您似乎在問如何在重複函數應用下計算函數的閉包。問題的關鍵是找到一種確保終止的方法，即確定函數被調用的最大次數的方法。在這種情況下，一個簡單的上限是List.length l;一個元素不能具有比幾代人更多的傳遞父母。使用這種洞察力，我們可以定義一個函數，號碼列表，並與所有父母的共同輸出這些數字的列表，然後我們List.length l次應用此功能本身，首先是parentsc的：

Require Import Coq.Lists.List. Import ListNotations. 
Require Import Coq.Sorting.Mergesort. Import NatSort. 
Scheme Equality for nat. 
Inductive Gen : Set := 
| BGen : nat -> nat -> Gen. 

Definition g1 := BGen 1 2. 
Definition g2 := BGen 2 3. 


Fixpoint parents (l : list Gen) (c : nat) := 
    match l with 
    | [] => [] 
    | (BGen p c') :: l' => if nat_beq c c' 
         then [p] 
         else parents l' c 
    end. 

Fixpoint deduplicate' (ls : list nat) := 
    match ls with 
    | [] => [] 
    | x :: [] => [x] 
    | x :: ((y :: ys) as xs) 
    => if nat_beq x y 
     then deduplicate' xs 
     else x :: deduplicate' xs 
    end. 
Definition deduplicate (ls : list nat) := deduplicate' (sort ls). 

Definition parents_step (l : list Gen) (cs : list nat) := 
    deduplicate (cs ++ List.flat_map (parents l) cs). 

Fixpoint all_parents' (l : list Gen) (cs : list nat) (fuel : nat) := 
    match fuel with 
    | 0 => cs 
    | S fuel' 
    => all_parents' l (parents_step l cs) fuel' 
    end. 
Definition all_parents (l : list Gen) (c : nat) := 
    deduplicate (all_parents' l (parents l c) (List.length l)). 

Definition gs := (g1::g2::nil). 

Compute all_parents gs 3. (* [1; 2] *)

來源

2017-10-23 06:27:20

是的，這就是我想要的。 –

如何在Coq中表示繼承？

回答

相關問題