How to prove these 2 theorems with the help of the function below?

Question

First, the function [foldc] should be defined, using the supplementary [eqfx].

Definition eq_corx {X : Type} (eqfx : X -> X -> bool) :=
  forall (x y : X), x = y <-> eqfx x y = true.

Definition foldc {X: Type} {eqfx} : @eq_corx X eqfx -> X -> list X ->  nat  :=

With [foldc], I would like to prove these 2 theorems below.

First:

Theorem foldc1  {X : Type} {eqfx} (eqx: eq_corx eqfx): 
  forall (l : list X),
    (forall (x:X), foldc eqfx x l = 0) <-> l = nil.

I tried to prove by induction on l, but I'm stuck.

Second:

Theorem foldc2 {X : Type} {eqfx} : 
    forall (l : list X) (eqx: eq_corx eqfx) (x y : X), 
    x = y <-> foldc eqx y (x::l)  = S (foldc eqx y l).

I tried unfolding [foldc], it didn't help unfortunately.

By the way, this is how [fold_right] is defined, which should help defining [foldc]:

Print fold_right.
fun (A B : Type) (f : B -> A -> A) (a0 : A) =>
fix fold_right (l : list B) : A :=
  match l with
  | [] => a0
  | b :: t => f b (fold_right t)
  end
     : forall A B : Type, (B -> A -> A) -> A -> list B -> A

Answer 1

You may simplify a little your definition of foldc (removing the hypothesis of correctness of eqfx.

Definition foldc {X: Type} (eqfx: X -> X -> bool) :
  X -> list X ->  nat  :=
  fun  x l =>
    fold_right (fun y n => if eqfx x y then n + 1 else n) 0 l.

Then you can prove your first theorem by induction on l. The only non-trivial subgoal which will appear will be of this form:

  l : list X
  IHl : (forall x : X, foldc eqfx x l = 0) <-> l = nil
  H : forall x : X, foldc eqfx x (a :: l) = 0
  ============================
  a :: l = nil

Obviously, H will lead to a contradiction, when specialized to a.

Require Import Lia.

Theorem foldc1  {X : Type} {eqfx} (eqx: eq_corx eqfx): 
  forall (l : list X),
    (forall (x:X), foldc eqfx x l = 0) <-> l = nil.
  induction l.
  - split; trivial.
  -  split; [| discriminate].
     intro H.
     specialize (H a);  cbn in H; replace (eqfx a a) with true in H.
      exfalso;  lia.
      symmetry; red in eqx; now rewrite  <- eq.
Qed.