Coq中如何表达继承？

Question

如何在 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]等所有父？

Answer 1

你好像问的是在重复函数应用下如何计算函数的闭包。问题的关键是找到一种确保终止的方法，即确定函数可能被调用的最大次数的方法。在这种情况下，一个简单的上限是 List.length l；一个元素的传递父代数不能超过代数。利用这种洞察力，我们可以定义一个函数，它接受一个数字列表，并输出这些数字及其所有父项的列表，然后我们将此函数应用于自身 List.length l 次，从 [=13 开始=] 共 c 个：

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] *)

Coq中如何表达继承？

How to express inheritance in Coq？

coq