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

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

• Have you tried proving your theorems on paper? What makes you think they are true? As a hint: when unfolding count_fold, you get stuck on some eqf x y. In general, this does not help, but if you are stuck on eqf x x then by your hypothesis on eqf, this should be true, which would unblock the computation. Equivalently, try and prove what count_fold eq x (x::l) is equal to. Jun 14 at 14:22
• I reverted the question because it was a lot less clear than the original question. In particular, your edit lacked any context and left out the definition of eq_corx. I'm not sure why you felt you needed to rename things that way. Feel free to rename things but please try to not make things more confusing in the process.
– Couchy
Jun 17 at 23:04

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.