2
$\begingroup$

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
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Jun 14 at 14:22
  • $\begingroup$ 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. $\endgroup$
    – Couchy
    Jun 17 at 23:04

1 Answer 1

4
$\begingroup$

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. 
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.