CODEWITHSUNDEEP
coq
Frank Sheng
Frank Sheng

Reputation: 205

How to express inheritance in Coq？

How can I get the all parents of a element in Coq? I define a set in Coq as follows:

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

There are many instances such as:

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

Now, I want to get the parents element of 3, i.e. [1,2]. I write a function:

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.

I can only get the direct parent [2] of 3, How can I get the all parents such as [1,2] in this example?

Upvotes: 0

Views: 141

Answers (1)

Jason Gross
Jason Gross

Reputation: 6128

You seem to be asking about how to compute the closure of a function under repeated function application. The key to the problem is to find a way to ensure termination, i.e., a way to determine the maximum number of times the function might be called. In this case, an easy upper bound is List.length l; an element cannot have more transitive-parents than there are generations. Using this insight, we can define a function that takes a list of numbers, and outputs a list of those numbers together with all of their parents, and then we apply this function List.length l times to itself, starting with parents of 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] *)

Upvotes: 4

Related Questions