Stream: Coq users

Topic: Existence in list


view this post on Zulip zohaze (Sep 20 2021 at 23:44):

In Coq how I can write this statement" Z(nat) number of elements are not member of list"?

view this post on Zulip Andrey Klaus (Sep 21 2021 at 07:39):

I'm not sure I see you right. But for the first approximation I would do something like

From Coq Require Import List.
Import ListNotations.

Fixpoint eqb_nat (a b : nat) : bool :=
  match a, b with
  | O, O => true
  | S a', S b' => eqb_nat a' b'
  | _, _ => false
  end.

Fixpoint InLst (lst : list nat) (x : nat) : bool :=
  match lst with
  | [] => false
  | x'::xs' => if eqb_nat x x' then true else InLst xs' x
  end.

Fixpoint Z (all lst: list nat) : nat :=
  match all with
  | [] => 0
  | x::xs => let nx := if InLst lst x then 1 else 0 in nx + Z xs lst
  end.

view this post on Zulip Andrey Klaus (Sep 21 2021 at 07:40):

so, all is a list of all possible elements.


Last updated: Feb 04 2023 at 21:02 UTC