Skip to main content
Proof Assistants Beta

Return to Question

Now the question matches the context, namings, and meaning of the answer, and I also prefer it this way. I tried to pay attention that no significant content gets removed, and also to make it even more meaningful.
Source Link
learner123
learner123
  • 25
  • 4

How to prove in Coq these 2 theorems with [count_fold]the help of the function below?

Here's a countFirst, the function [foldc] should be defined via fold, using the supplementary [eqf][eqfx].

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

Definition count_foldfoldc {X: Type} {eqfeqfx} : @eq_cor@eq_corx X eqfeqfx -> X -> list X ->  nat  :=
  fun _ x l => (fold X nat (fun y n => if eqf x y then n + 1 else n) l 0).

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

First:

Theorem count_fold_nilfoldc1  {X : Type} {eqfeqfx} (eqx: eq_corx eqfx): 
  forall (l : list X) (eq: eq_cor eqf),
     (forall (x:X), count_foldfoldc eqeqfx x l = 0) <-> l = nil.

I have a hint, but not sure if it's for the first, or the second theorem:

I might need to prove a little lemma for one of directions: for example, that n <> S n for any n. Of course, it may also be the case that there is such a lemma in the standard library. What I tried, is to prove by induction on l, but I'm stuck.

Second:

Theorem count_occ_cons_eqfoldc2 {X : Type} {eqfeqfx} : 
    forall (l : list X) (eqeqx: eq_coreq_corx eqfeqfx) (x y : X), 
    x = y <-> count_foldfoldc eqeqx y (x::l)  = S (count_foldfoldc eqeqx y l).

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

By the way, this is how [fold][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

Definition fold (A B: Type) f l b:= @fold_right B A f b l.

How to prove in Coq these 2 theorems with [count_fold]?

Here's a count function defined via fold, using the supplementary [eqf].

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

Definition count_fold {X: Type} {eqf} : @eq_cor X eqf -> X -> list X ->  nat  :=
  fun _ x l => (fold X nat (fun y n => if eqf x y then n + 1 else n) l 0).

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

First:

Theorem count_fold_nil  {X : Type} {eqf} : 
  forall (l : list X) (eq: eq_cor eqf),
     (forall (x:X), count_fold eq x l = 0) <-> l = nil.

I have a hint, but not sure if it's for the first, or the second theorem:

I might need to prove a little lemma for one of directions: for example, that n <> S n for any n. Of course, it may also be the case that there is such a lemma in the standard library. What I tried, is to prove by induction on l, but I'm stuck.

Second:

Theorem count_occ_cons_eq {X : Type} {eqf} : 
    forall (l : list X) (eq: eq_cor eqf) (x y : X), 
    x = y <-> count_fold eq y (x::l)  = S (count_fold eq y l).

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

By the way, this is how [fold] is defined:

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

Definition fold (A B: Type) f l b:= @fold_right B A f b l.

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
added 4 characters in body
Source Link
taylor.2317
taylor.2317
  • 1.3k
  • 8
  • 36

Here's a count function defined via fold, using the supplementary [eqf].

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

Definition count_fold {X: Type} {eqf} : @eq_cor X eqf -> X -> list X ->  nat  :=
  fun _ x l => (fold X nat (fun y n => if eqf x y then n + 1 else n) l 0).

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

First:

Theorem count_fold_nil  {X : Type} {eqf} : 
  forall (l : list X) (eq: eq_cor eqf),
     (forall (x:X), count_fold eq x l = 0) <-> l = nil.

I have a hint, but not sure if it's for the first, or the second Theoremtheorem:I

I might need to prove a little lemma for one of directions: for example, that n <> S n for any n. Of course, it may also be the case that there is such a lemma in the standard library. What I tried, is to prove by induction on l, but I'm stuck.

Second:

Theorem count_occ_cons_eq {X : Type} {eqf} : 
    forall (l : list X) (eq: eq_cor eqf) (x y : X), 
    x = y <-> count_fold eq y (x::l)  = S (count_fold eq y l).

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

By the way, this is how [fold] is defined:

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

Definition fold (A B: Type) f l b:= @fold_right B A f b l.

Here's a count function defined via fold, using the supplementary [eqf].

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

Definition count_fold {X: Type} {eqf} : @eq_cor X eqf -> X -> list X ->  nat  :=
  fun _ x l => (fold X nat (fun y n => if eqf x y then n + 1 else n) l 0).

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

First:

Theorem count_fold_nil  {X : Type} {eqf} : 
  forall (l : list X) (eq: eq_cor eqf),
     (forall (x:X), count_fold eq x l = 0) <-> l = nil.

I have a hint, but not sure if it's for the first, or the second Theorem:I might need to prove a little lemma for one of directions: for example, that n <> S n for any n. Of course, it may also be the case that there is such a lemma in the standard library. What I tried, is to prove by induction on l, but I'm stuck.

Second:

Theorem count_occ_cons_eq {X : Type} {eqf} : 
    forall (l : list X) (eq: eq_cor eqf) (x y : X), 
    x = y <-> count_fold eq y (x::l)  = S (count_fold eq y l).

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

By the way, this is how [fold] is defined:

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

Definition fold (A B: Type) f l b:= @fold_right B A f b l.

Here's a count function defined via fold, using the supplementary [eqf].

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

Definition count_fold {X: Type} {eqf} : @eq_cor X eqf -> X -> list X ->  nat  :=
  fun _ x l => (fold X nat (fun y n => if eqf x y then n + 1 else n) l 0).

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

First:

Theorem count_fold_nil  {X : Type} {eqf} : 
  forall (l : list X) (eq: eq_cor eqf),
     (forall (x:X), count_fold eq x l = 0) <-> l = nil.

I have a hint, but not sure if it's for the first, or the second theorem:

I might need to prove a little lemma for one of directions: for example, that n <> S n for any n. Of course, it may also be the case that there is such a lemma in the standard library. What I tried, is to prove by induction on l, but I'm stuck.

Second:

Theorem count_occ_cons_eq {X : Type} {eqf} : 
    forall (l : list X) (eq: eq_cor eqf) (x y : X), 
    x = y <-> count_fold eq y (x::l)  = S (count_fold eq y l).

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

By the way, this is how [fold] is defined:

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

Definition fold (A B: Type) f l b:= @fold_right B A f b l.
deleted 25 characters in body
Source Link
taylor.2317
taylor.2317
  • 1.3k
  • 8
  • 36

Here's a count function defined via fold, using the supplementary [eqf].

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

Definition count_fold {X: Type} {eqf} : @eq_cor X eqf -> X -> list X ->  nat  :=
  fun _ x l => (fold X nat (fun y n => if eqf x y then n + 1 else n) l 0).

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

First:

Theorem count_fold_nil  {X : Type} {eqf} : 
  forall (l : list X) (eq: eq_cor eqf),
     (forall (x:X), count_fold eq x l = 0) <-> l = nil.

I have a hint, but not sure if it's for the first, or the second Theorem:I might need to prove a little lemma for one of directions: for example, that n <> S n for any n. Of course, it may also be the case that there is such a lemma in the standard library. What I tried, is to prove by induction on l, but I'm stuck.

Second:

Theorem count_occ_cons_eq {X : Type} {eqf} : 
    forall (l : list X) (eq: eq_cor eqf) (x y : X), 
    x = y <-> count_fold eq y (x::l)  = S (count_fold eq y l).

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

By the way, this is how [fold] is defined:

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

Definition fold (A B: Type) f l b:= @fold_right B A f b l.

Thank you in advance.

Here's a count function defined via fold, using the supplementary [eqf].

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

Definition count_fold {X: Type} {eqf} : @eq_cor X eqf -> X -> list X ->  nat  :=
  fun _ x l => (fold X nat (fun y n => if eqf x y then n + 1 else n) l 0).

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

First:

Theorem count_fold_nil  {X : Type} {eqf} : 
  forall (l : list X) (eq: eq_cor eqf),
     (forall (x:X), count_fold eq x l = 0) <-> l = nil.

I have a hint, but not sure if it's for the first, or the second Theorem:I might need to prove a little lemma for one of directions: for example, that n <> S n for any n. Of course, it may also be the case that there is such a lemma in the standard library. What I tried, is to prove by induction on l, but I'm stuck.

Second:

Theorem count_occ_cons_eq {X : Type} {eqf} : 
    forall (l : list X) (eq: eq_cor eqf) (x y : X), 
    x = y <-> count_fold eq y (x::l)  = S (count_fold eq y l).

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

By the way, this is how [fold] is defined:

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

Definition fold (A B: Type) f l b:= @fold_right B A f b l.

Thank you in advance.

Here's a count function defined via fold, using the supplementary [eqf].

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

Definition count_fold {X: Type} {eqf} : @eq_cor X eqf -> X -> list X ->  nat  :=
  fun _ x l => (fold X nat (fun y n => if eqf x y then n + 1 else n) l 0).

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

First:

Theorem count_fold_nil  {X : Type} {eqf} : 
  forall (l : list X) (eq: eq_cor eqf),
     (forall (x:X), count_fold eq x l = 0) <-> l = nil.

I have a hint, but not sure if it's for the first, or the second Theorem:I might need to prove a little lemma for one of directions: for example, that n <> S n for any n. Of course, it may also be the case that there is such a lemma in the standard library. What I tried, is to prove by induction on l, but I'm stuck.

Second:

Theorem count_occ_cons_eq {X : Type} {eqf} : 
    forall (l : list X) (eq: eq_cor eqf) (x y : X), 
    x = y <-> count_fold eq y (x::l)  = S (count_fold eq y l).

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

By the way, this is how [fold] is defined:

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

Definition fold (A B: Type) f l b:= @fold_right B A f b l.
Rollback to Revision 4
Source Link
Couchy
Couchy
  • 2.3k
  • 2
  • 9
  • 39
added 2 characters in body
Source Link
learner123
learner123
  • 25
  • 4
deleted 1 character in body
Source Link
learner123
learner123
  • 25
  • 4
deleted 1045 characters in body; edited tags; edited title
Source Link
learner123
learner123
  • 25
  • 4
Post Undeleted by Couchy
Post Deleted by learner123
added 56 characters in body
Source Link
learner123
learner123
  • 25
  • 4
edited title
Link
learner123
learner123
  • 25
  • 4
added 360 characters in body
Source Link
learner123
learner123
  • 25
  • 4
Source Link
learner123
learner123
  • 25
  • 4