如何在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中表示继承？

回答

相关问题