if x is member of a list then it will be equivalent to In x l? Output data type of In predicate is proposition and member function has bool output. Could we prove their equivalence/ convert them?

Check the theorem `in_dec`

, you need to be able to decide equality on the elements of the list.

in_dec is {In n l} + {~In n l}. But still answer will be in proposition. I want to ask, if in Coq code lemma statement and its proof (related to In n l present /exist) then could i replace it with a function which check the presence of n in list? Only benefit i want to get is the bool data type at output instead of prop .

No `In_dec`

can be used to define function.

```
Require Import List Arith.
(* Test if i is in l *)
Definition test i (l : list nat) :=
match In_dec Nat.eq_dec i l with
left _ => true
| right _ => false
end.
(* Compute the intersection of 2 lists *)
Definition inter (l1 l2 : list nat) := filter (fun i => test i l1) l2.
Definition l1 := 3 :: 5 :: 7 ::8 :: 9 :: nil.
Definition l2 := 2 :: 5 :: 9 :: nil.
Compute inter l1 l2.
```

In n1 l ->

In n2 l ->

In n3 l ->

f(n1+n2+n3 ) l.

f function is inductively defined function and output is Prop. I want to ask

1) May i convert it into boolen output directly (like)

f(n1+n2+n3 ) l=true

2) I have to re-define f in recursive form (so that its output is bool)?

Nop you can't translate Prop to bool directly. What people sometime do is to have a function `f : nat -> Prop`

for proof and define a bool version `g : nat -> bool`

for computation and then prove `forall x, f x <-> g x = true`

. Others work directly only with `g`

.

Yes, i am doing the same thing. Now defining bool version. f is inductively defined. I am asking ,now i should use recursive definitions to define g ? New i have to define equivalent of f definition in the form of bool ? So that function behaviour remains the same.

It could have been better if you had posted the code you are working on (the function `f`

for instance)

(for us to save time and give an appropriate answer).

Here is an artificial example, where `P`

is an inductive predicate and `p`

a recursive Boolean function.

```
Import ListNotations.
Inductive P (a b c: nat) : list nat -> Prop :=
here : forall x l, x = a+b+c -> P a b c (x:: l)
| next : forall x l, P a b c l -> P a b c (x::l).
Goal P 1 2 3 [4;5;6;7].
do 2 right; now left.
Qed.
Fixpoint p a b c (l: list nat) : bool :=
match l with
| nil => false
| x::tl => if Nat.eqb (a+b+c) x then true else p a b c tl
end.
Compute p 1 2 3 [4;5;6;7].
Lemma p_OK : forall a b c l, P a b c l <-> p a b c l= true.
```

Lemma p_OK : forall a b c l, P a b c l <-> p a b c l= true. is necessery after defining the function in both forms.

Yes, you can prove it by induction on `l`

. Here's a first (improvable) proof.

```
Lemma p_OK : forall a b c l, P a b c l <-> p a b c l = true.
Proof.
induction l; simpl;split; intro H.
- inversion H.
- discriminate.
- case_eq (a+b+c =? a0).
+ easy.
+ inversion_clear H.
* subst a0; rewrite Nat.eqb_refl; discriminate.
* now rewrite IHl in H0.
- case_eq (a + b + c =? a0).
+ intro H0; left; rewrite Nat.eqb_eq in H0; auto.
+ intro H0; rewrite H0 in H; right; now rewrite IHl.
Qed.
```

Natural number list is maintaing some patteren arrangement. The property on the basis of which list is made can be express by

using recursive function. In this case property expression is like a boolean exprssion of patteren maintained by list or how list is made.

hold_p l = true -> hold_p (p a b c l) = true. Is this possible way of expessing list property?

In above (a+b+c) exist in all elements then it give true.

Mylist=[c1,c2,c3,c4...].

I am checking the presence of all elements of the list in different lists l1,l2,l3.. (recursively).Like

In c1 l1 In c2 l2 In c3 l3 ... then it gives true. When bool data type is true then this condition is fullfilled by all elements of list.

Now i am selecting two elements c2 & c3 and have hypothesis H0: In c2 l2 H1: In c3 l3 .Then how i could write as you written

(if Nat.eqb (a+b+c) x then true else p a b c tl)? In prdicate gives Prop but i have converted it into bool for easyness.

your question is not clear, sorry

In first constructor add three numbers then add in l. What is the meaning of second constructor?

| next : forall x l, P a b c l -> P a b c (x::l).

2)When i run the code at point where apply easy command .At this point i got this error "Tactic failure: Cannot solve this goal."

What alternate command i should apply?

3) is there any differnce between eauto and easy command?

@pianke Do you refer to the code I posted on Feb 15th and/or 16th ?

It was only an example on the property " the list `l`

contains at least an element equal to `a+b+c`

". It works if you import `Arith`

, `List`

and`ListNotations`

before.

If `easy`

doesn't work on your Coq installation, you may try `reflexivity`

or `trivial`

.

1) I have already included these libraries. When apply reflexivity instead of easy, this command is accepted by Coq but it do nothing. Same for trivial.

2) Yes. 15Feb post. I need conversion therefore i am taking your given example as a reference . But all elements of list should be sum of three numbers. Then why there is need of "| next : forall x l, P a b c l -> P a b c (x::l).".Just explain meaning of writing this constructor.

pianke said:

1) I have already included these libraries. When apply reflexivity instead of easy, this command is accepted by Coq but it do nothing. Same for trivial.

2) Yes. 15Feb post. I need conversion therefore i am taking your given example as a reference . But all elements of list should be sum of three numbers. Then why there is need of "| next : forall x l, P a b c l -> P a b c (x::l).".Just explain meaning of writing this constructor.

Sorry, but I didn't see the sentence "But all elements of list should be sum of three numbers" in the previous posts (not precise enough).

So my proposition implemented another proposition "there exists in l an element equal to a+b+c".

So, you can use one of the two following definitions.

```
Definition f a b c l: bool := forallb (fun x => x =? a + b +c) l.
Definition F a b c l: Prop := Forall (fun x => x = a + b + c) l.
```

and establish a logical relation between `F`

and `f`

.

This is an example of the issues which happen when questions are incomplete or too informal.

We spend a lot a time to guess what it is about, and may give a useless answer because there may be various ways to interpret a question.

No change means ,after applying command there is no change in code (no simplification). This is all about conversion,In my case there is difference in the used arguments/variables in function definition inductive form and in bool form. Could i proceed in present form or i have to redefine function in boolean form with equal arguments?

Like this

```
Lemma p_OK : forall a b c l, P a b c l <-> p a b c l = true"
but difference of input arguments exist.
F1 x y l = f1 a b c x y l.
```

a b c are locally calculated in F1. In F1 there is condition a>0 b>0 c>0.

But in f1 there is no condition on a>0 b>0 only on c >0.

Problem is here.

When unfold f1 then i get following msg during recursive call of f1 (fix a0 b0 c0....). How i remove it and make it simple? Function testing gives correct results because c is the multiplication of a and b.Therefore if c>0 then a and b are also greater than 0. Plz help me how i could solve this?

Last updated: Jun 14 2024 at 19:02 UTC