```
Inductive elemts:nat->nat->list nat->Prop:=
|b_0 : forall n l , elemts 0 0 l
|b_3 : forall n m l , elemts 0 3 l
|b_sum : forall(n m:nat), elemts n m l ->elemts (n+m) m l
```

H: elemts n m []

Goal: true= false

When apply inversion H then get three times sub goals true= false (might be because of 3 constructors). What i should do to solve empty list case Or what hypothesis i should add so that by applying inversion H , i solve the goal statement.

from the hypotheses you provided I can't see a way to derive a contradiction

The definition of `elemts`

looks strange. Is it really what you typed? :thinking:

- In the first and second constructor
`n`

and`m`

are not used (hence an error message from Coq). - I see no relation between
`l`

and`n`

,`m`

.

If you remove the useless quantification on `n`

and `m`

in the first two constructors, you just describe the relation

`(m = 0 or m= 3) and n is a multiple of 3, and l is any list`

.

Agree with @Pierre Castéran The current definition can just be simplified to

```
Inductive elemts: nat->nat->Prop:=
| b_0 : elemts 0 0
| b_3 : elemts 0 3
| b_sum : forall n m, elemts n m ->elemts (n+m) m.
```

If you want to define a property that the length of a list is a multiple of 3, maybe this is more reasonable:

```
From Coq Require Import List.
Inductive multiple_of_3 {A: Type}: list A -> Prop:=
| M_empty : multiple_of_3 nil
| M_grow : forall ls a b c,
multiple_of_3 ls ->
multiple_of_3 (a :: (b :: (c :: ls)))
.
```

@Remzi Yang You're right!

The problem with the original question is that there are too many reasonable ways to fix such an erroneous specification.

For instance : characterize the lists of the form `[a0;a1;a2;...;an]`

where `a0=0 or a0=3`

and `a{i+1}=ai+3 for any i<n`

.

At least, the OP should give a sufficient list of examples and counter-examples if the issue is in building a correct formal specification (in math form or as a predicate written in Coq).

Right. We need to make sure what the requirement is.

Hi @pianke Could you please clarify what rules do you want to define?

```
Inductive elemts:nat->nat->list nat->Prop:=
|b_0 : forall n l , elemts n n l
|b_3 : forall n m l , elemts n m l
|b_sum : forall(n m:nat), elemts n m l ->elemts (n+m) m l
```

Only three rules exist. Both elements may be same or not or (n+m)m only. I want to write that on the basis of these rules list l is made Or l obey these rules.

1)How i should write it.

2)As you said ,there is no relation between n m & l. You mean i should write In n l-> In m l in each and every constructor?

3)elemt(nat)= no of elements of l. I want to add the condition elemt>0 so that empty list case could be avoided. How to define elemt(nat) in the rules? So that i could prove this H: elemts n m l & H1: elemt=0 ->False.

```
Inductive elemts:nat->nat->list nat->Prop:=
|b_0 : forall n l elemt, elemt>0 ->In n l -> elemts n n l
|b_3 : forall n m l ,elemt>0 ->In n l->In m l-> elemts n m l
|b_sum : forall(n m:nat), elemt>0 ->In n l->In m l-> elemts n m l -> elemts (n+m) m l
```

I want to ask question about first and second constructor of above function

(i) elemts n n l -> elemts m m l -> elemts n m l

(ii) Rules may be use for three or multiple arguments like elemts n m l-> elemts m k l -> elemts n k l?

```
lemts:nat->nat->list nat->Prop:=
|....
|b_3 : forall n m l , elemts n m l
|.....
```

THis rule makes no sense.....

i have modify |b_3 : forall n m l ,elemt>0 ->In n l->In m l-> elemts n m l , still it make no sense? What about modified form of

elemts. Meaning of b_3 is not this " if n and m exist in l then elemts's second rule (exist) or it could be apply? If does not then how i should write it?

The condition `elemt > 0`

(may be `length l > 0`

instead, I don't see why `elemt`

is not a function applied to `l`

? ) is superfluous:

if `In n l`

holds, obviously `l`

is not empty.

`b_0`

is superfluous too (it's just a special case of `b_3`

).

I don't understand which property `elemts`

is supposed to formalize yet. We cannot talk about `elemts`

's correctness without this information (as precise as possible).

Most of the people who answer questions on this thread are quite busy, writing and maintaining Coq and its libraries, tools in Coq's ecosystem, and/or documentation. Please take the time to post questions:

- specifying what you wanted to define and/or prove
- including code without errors (unless the question is about a non-understood error message)

If you are not sure whether an [inductive] definition implements the property you wanted to define, please take the time to test this definition with a small set of examples/counter-examples.

If the question is about a non completed proof, please give exactly the code you typed.

Ok. At end answer of " I don't understand which property elemts is supposed to formalize yet". List l holds natural numbers which follow these 3 rules. " instead, I don't see why elemtis not a function applied to l?" applied to l means define relation of n presence in l in stead of In n l.like In n(f2 l)->

elemts n m l.( f2 check the property of n in l). I have to define this property for first rule also. Thank you so much .

List l holds natural numbers which follow these 3 rules.

Ok. So let's try to clarify this step by step. If we want to define a rule on `list nat`

, the type of the rule should be `list nat -> Prop`

, right?

And If you want the empty list to follow the rule, we need a constructor for the empty list.

So for now, we can have our code as

```
Inductive elemts: list nat -> Prop :=
| E_empty : elemts []
...
```

The next step is to add more constructors to `elemts`

for your requirement

Thank u ,thank u. 1) let's try to clarify this step by step. If we want to define a rule on list nat,..."

Yes, apply it on nat list . Want to check the presence of any n m in this list. There is possibility both elements are same .I will solve it by rule 1.

n m are two different elements of this list ,then solve by 2 .In case of more than two only possibility is rule 3. Therefore i have written f:nat->nat->list nat:Prop.

I do't know meaning of apply function l. Its meaning including testing function to test to test n is part of l or not.

Ok. Although I am still a little confused, I guess I've gotten the direction.

So our goal is to check if both `m`

and `n`

are in the list, right?

I don't check the Coq std lib, but we can build from scratch.

So start from the very beginning, let first try to define the relation that number `m`

is in the list.

```
Inductive inList (m: nat): list nat -> Prop :=
| In_head : forall ls, inList m (m :: ls) (* if the head of the list is m, then the m is in the list*)
| In_tail : forall n ls, inList m ls -> inList m (n :: ls) (* Any list whose tail contains m, also contains m *)
.
```

Then to define m, n in list, it is straightforward

```
Definition BothInList m n ls := inList m ls /\ inList n ls.
```

in case of more than two only possibility is rule 3

Could you please give a concrete example of this (such as 1, 2, 3 in [1, 2, 3, 4]) ?

If we remove a few redundancies :

```
Inductive elemts:nat->nat->list nat->Prop:=
|b_3 : forall n m l ,In n l->In m l-> elemts n m l
|b_sum : forall(n m:nat) l, In n l->In m l-> elemts (n+m) m l.
```

We obtain a predicate equivalent to:

```
Definition elemts' (n m : nat) (l: list nat) :=
(In n l /\ In m l) \/
(exists p, n = p + m /\ In m l /\ In p l).
```

Is missing relation between numbers and list is this one

```
Inductive elemts:nat->nat->list nat->Prop:=
|b_0 : forall n l , elemts n n l
|b_3 : forall n m l ,In n l->In m l->In n(f2 m)-> elemts n m l
|b_sum : forall(n m:nat) l, In n l->In m l->In n (f4 m)-> elemts (n+m) m l.
```

Is proveable

H: elemts n m l

H1: No of element of l=0 ->False. What more missing information is here?

For setting link between elements and list , may i modify rule 1 as

1) |b_0 : forall n l , existb (eq_nat n) l -> elemts n n l.

2) To avoid message "existb not exist in current envirnoment" (although included Bool library). What i should do?

You mispelled `existsb`

(from `List`

library) and used `Nat.eq_nat`

instead of `Nat.eqb`

.

```
Require Import List.
Locate existsb.
Goal forall x l, existsb (Nat.eqb x) l = true <-> In x l.
intros x l; rewrite existsb_exists; split.
intros [y [Hy Hy']]; rewrite Nat.eqb_eq in Hy'; now subst.
intro Hx; exists x; split; [trivial | now rewrite Nat.eqb_refl].
Qed.
```

@Remzi There are 2 possibilities n=m & n<>m.

1) Now want to define a function f with two nat and list nat as input arguments , with two constructors 1 & 2. constr1 deals with the case of equality n=m & constr2 with n<>m. Now how to link above with this one?

2) If simply write In n l & In m l ,then simplification of In predicate automatically check In n l \/ In m l.(In_head and In_tail). Or in definition of f , first i have to check n m equality . |b_0 : forall n l , Nat.eqb n m -> elemts n n l

|b_0 : forall n l , In n l-> In m l-> Nat.eqb n m -> elemts n n l

3)There are two constructors both deals with In n l-> In m l and their equality.There is no empty list case.

How to colse [] case.

I'm still quite confused.

Do you want to

1) define a function `f: nat -> nat -> list nat -> bool`

?

2) define a predicate `P: nat -> nat -> list nat -> Prop`

?

3) both of them, and prove `forall n m l, f n m l = true <-> P n m l`

?

In 1) or 2), it is better to describe what you want do define (case by case) what you want (mathematically or in the form of correctly typed Coq code).

It's only once you have a correct specification of what you want to define that we can discuss about constructors, case analysis, recursion, etc.

Last updated: Jun 20 2024 at 12:02 UTC