Stream: Coq users

Topic: empty list case


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre Castéran (Apr 27 2023 at 17:16):

The definition of elemts looks strange. Is it really what you typed? :thinking:

If you remove the useless quantification on nand min 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.

view this post on Zulip 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)))
.

view this post on Zulip 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=3and 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).

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.....

view this post on Zulip 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?

view this post on Zulip Pierre Castéran (Apr 29 2023 at 07:21):

The condition elemt > 0 (may be length l > 0 instead, I don't see why elemtis not a function applied to l? ) is superfluous:
if In n l holds, obviously l is not empty.
b_0is 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:

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.

view this post on Zulip 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 .

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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]) ?

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Pierre Castéran (May 01 2023 at 08:52):

You mispelled existsb (from Listlibrary) and used Nat.eq_natinstead 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.

view this post on Zulip 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.

view this post on Zulip 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