zohaze (Sep 20 2021 at 23:44): 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"?
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.
so, all is a list of all possible elements.
Last updated: Sep 26 2023 at 11:01 UTC