## Stream: Coq users

### Topic: empty list case

#### pianke (Apr 27 2023 at 16:27):

``````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.

#### Huỳnh Trần Khanh (Apr 27 2023 at 16:31):

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

#### Pierre Castéran (Apr 27 2023 at 17:16):

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`.

#### Remzi Yang (Apr 28 2023 at 02:19):

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)))
.
``````

#### Pierre Castéran (Apr 28 2023 at 06:39):

@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).

#### Remzi Yang (Apr 28 2023 at 06:44):

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

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

#### pianke (Apr 28 2023 at 17:03):

``````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
``````

#### zohaze (Apr 28 2023 at 17:29):

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?

#### Laurent Théry (Apr 28 2023 at 22:11):

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

THis rule makes no sense.....

#### pianke (Apr 29 2023 at 06:31):

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?

#### Pierre Castéran (Apr 29 2023 at 07:21):

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.

#### pianke (Apr 29 2023 at 08:12):

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 .

#### Remzi Yang (Apr 29 2023 at 08:25):

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

#### pianke (Apr 29 2023 at 08:44):

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.

#### Remzi Yang (Apr 29 2023 at 09:00):

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]) ?

#### Pierre Castéran (Apr 29 2023 at 09:45):

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).
``````

#### pianke (Apr 29 2023 at 13:41):

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?

#### pianke (May 01 2023 at 08:10):

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?

#### Pierre Castéran (May 01 2023 at 08:52):

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.
``````

#### zohaze (May 02 2023 at 13:59):

@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.

#### Pierre Castéran (May 04 2023 at 07:04):

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: Oct 04 2023 at 23:01 UTC