I want to find patteren matching in list & list of a function. creat function with input arguments(x y z:nat)(l:list nat)

and list nat as output. This function generates a list of natural numbers in which elements are arrange in a

particular patteren (according to definition of creat).

l2 is list nat . Want to write that l2 is made by same patteren as defined in creat in creat function or l2 have same patteren of creat function. How i should start it? I have checked the function on multiple values it works properly.

could you give a concrete example so we can help you?

I have a list in which numbers are arranged in particular way . For example l1=[2,5,8,11,14]

Fixpoint creat (x y z:nat)(l:list nat):

{......

}

Output of above function gives a list of same patteren as l1 . To prove this, how i should start?

How to relate both (especially input arguments)?

```
Require Import List Arith.
Import ListNotations.
Definition l1 := [2; 5; 8; 11; 15].
Fixpoint make_list (x : nat) (y : nat) (l : list nat) :=
match x with
| 0 => l
| S x1 => y :: (make_list x1 (S (S (S y))) l)
end.
Compute make_list 3 2 [11; 15].
Lemma make_list_li1 : make_list 3 2 [11; 15] = l1.
Proof.
simpl.
unfold l1.
trivial.
Qed.
Lemma make_list_cons : forall n m l,
make_list (S n) m l = make_list n m (m + n * 3 :: l).
Proof.
simpl.
induction n as [|n IH].
- intros m l.
simpl.
now rewrite Nat.add_0_r.
- intros m l.
simpl.
rewrite IH.
now rewrite <- ! Nat.add_succ_comm.
Qed.
```

l1 contents are not fix. It is generated by someone else function but only available information is " whatever elements

exist in l1 follow this property.. (S (S (S y) . As a result l1 could be [3; 6; 9; 12; 15] or [11;14;17;20] or [44,47;50;53]....Therefore, first i have to verify that whatever l1 is according to specified rule.

2)I have defined function (like make_list) to define property on the basis of which list make.(make_list x y z l. Without it no one knows what is l1.)

3) Due to this problem , i am unable to define lemma like below

Lemma make_list_li1 : make_list x y z l = l1.

4) I have defined Variable l1: list nat. Pass this list to

make_list (x y z l1) . Then resultant will be like l1 because formation rule

is same . Is this right way?

ok, something more like this? `is_even`

is my pattern. `make_list`

is my function and I show that my pattern is preserved by `make_list`

```
Require Import List Arith.
Import ListNotations.
Section Test.
Fixpoint is_even (l : list nat) :=
match l with
| [] => true
| a :: l1 => (Nat.even a && is_even l1)%bool
end.
Compute is_even [1; 2; 3].
Compute is_even [2; 4; 6].
Fixpoint make_list (x : nat) (y : nat) (l : list nat) :=
match x with
| 0 => l
| S x1 => y :: (make_list x1 (S (S y)) l)
end.
Compute make_list 3 2 [12; 13].
Lemma even_make_list : forall n m l,
Nat.even m = true -> is_even l = true -> is_even (make_list n m l) = true.
Proof.
induction n as [|n IH].
- intros m l H1 H2.
simpl.
trivial.
- intros m l H1 H2.
simpl.
rewrite H1.
rewrite IH.
+ trivial.
+ simpl.
trivial.
+ trivial.
Qed.
```

```
```

Thanks. I have defined pattern as well as function which make this list. I have hypothesis H:=In n l1. At this point i have two lemmas(two options)

1) Lemma make_list_li1 : make_list 3 2 [11; 15] = l1.

2) Some thing like this lemma

Lemma even_make_list : forall n m l,

Nat.even m = true -> is_even l = true -> is_even (make_list n m l) = true.

with one difference i.e

Lemma even_make_list : forall n m l l3,

Nat.even m = true -> is_even l = true -> is_even (make_list n m l3) = true.(l3->l)

i) is it ok?

ii) Which lemma i should use to apply H , to extract information and to make code simple.

in my case, the information I could extract from `In n l1`

is the following :

```
Lemma even_is_even :
forall n l, is_even l = true -> In n l -> Nat.even n = true.
Proof.
intros n l.
induction l as [|a l IH].
- intros H1 H2.
now destruct (in_nil H2).
- simpl.
intros H3 H4.
destruct H4.
+ rewrite <- H.
now destruct (Nat.even a).
+ apply IH.
* destruct (is_even l).
-- now trivial.
-- now rewrite Bool.andb_false_r in H3.
* now trivial.
Qed.
```

I have two more problems related to above post. Plz reply

1) (f2 a l)=l2

make_list n m l2.

Lemma even_make_list : forall n m l l2,

Nat.even m = true -> is_even l2 = true -> is_even (make_list n m (f2 a l)) = true. Is correct way of writing in the light of above reply?

(I am using two lists here)

2) l2 is subset of l. There is one problem that l2 is even not the whole l. How to solve

it? (May i solve it like 1) No of arguments should be same on both side?

if l2 is a subset of l you should be able to prove `is_even l = true -> is_even (f2 a l) = true `

Thank u 4 reply. Plz,correct my statement, i am thinking there should be l2 instead of l,otherewise it will cause problem .For example

l= [1;2;3;4;6;8;10;12]

l2= [4;6;8;10;12]

Then this part will true "is_even (make_list n m (f2 a l)) = true."

is_even l = true will be false because l contains some odd numbers also.

Therefore i am asking i should write l2 . Then both sides will be equal. If i do that then there occurs input argument mismatch(l &l2. Especially when apply induction on l.)

2) In the presence of all above lemmas and hypothesises ,i attach another property with list l. That is every member of the list will be multiple of 2 instead of zero.

Then continue from here

Lemma even_is_even :

forall n l, is_even l = true -> In n l -> Nat.even n = true->mutiple n=true.

1) What do you know about `l`

?

2) So l containts only pair elements?

l is nat list .Some elements of this list hold the property ,which we are discussing evenness ( numbers are even.)

I have 3 hypothesises l In n l multiple 2 l=true.

First i have shown make of l then its evenness then n is even. Next i have to show n is multiple of 2. How to relate above.

Two lemmas which you have suggested (make_list & is even ) i have done . Then show n is even. What next lemma i should write that n is even so it is multiple of two.(In n l -> Nat.even n = true-> multiple 2 l =true).

what is the definition of `multiple n l`

?

Sorry , it is multiple 2 l . Every even number(m) is multiple of two means when we will divide this number by 2 then remainder will be zero. Nat.eqb remainder (divide m/2) 0=true. Just want to relate two properties in lemma statement.

Maybe you have to prove that to be even is the same than to be a multiple of 2:

```
Lemma even_mod2 n : Nat.even n = Nat.eqb (n mod 2) 0.
Proof.
induction n as [n IH] using lt_wf_ind.
destruct n as [|n].
- trivial.
- destruct n as [|n].
+ trivial.
+ replace (S (S n)) with (n + 1 * 2) at 2 by ring.
rewrite Nat.mod_add.
rewrite <- IH.
* trivial.
* auto with arith.
* auto with arith.
Qed.
```

I want to reply ur question of 5th march.

1) Any n which is present in l which have the evenness property, when given to function multiple n l then same n will give true also. (because n is even, i have proved in above lemma n is even. All n means same element present in l & is even ).

I have 2 hypothesises i) l have evenness property ii) In n l (Goal multiple n l=true.)

I want to ask the sequence of lemmas to prove above.

2) In previous post you have suggested two lemmas(make of list & proof of n is even). Uptill now i have proved n is even .I want to ask if i attach/add any other property like multiple with same list elements or all elements of l are not odd then how i should write lemma? I have problem in linking one propery obeyed by n and one another property hold by same n. just give one or two ways of writing this statement.

3) I have replaced it with 2 but it could be any even number (n) from l.

4) Your reply both are same or list l have both properties means same? There proof will be same?

Again what is the definition of `multiple n l`

?

```
Fixpoint multiple (l:list nat):bool:=
match l with
|[]=>true
|h::t=> if Nat.eqb (remainder (divide h/2)) 0 then multiple t else false
end
```

H1: l (* suppose to have some segment of even numbers)

H2: In n l (* use this to write n is even *)

Goal: multiple l = true. (* This goal statement is proveable because of even segment in l*)

To prove this goal statement how i can use hypothesises ?

In your definition `(remainder (divide h/2)))`

does not seem valid. Is that exactly your Coq definition?

Two other remarks

- what is the
`n`

in H2 for? If l iis some segment of even numbers,`multiple l = true`

holds. No needs of`n`

. - How
`suppose to have some segment of even numbers`

is expressed in your Coq file?

1) No it is mathematical form (i have defined divide function then remainder function then check their outputs.It requires one argument of nat type & l and gives true or false)

l=[2,4,6,8,10]. This l is the output of another function which generates even number list. Therefore i suppose , have a list of even numbers. Contents of list are varying on each execution but they are even every time. I have defined the making of list

Lemma even_make_list : forall n m l,

Nat.even m = true -> is_even l = true -> is_even (make_list n m l) = true.

Now n m are arguments of make_list. If have H: In m l or In n l. It means m n are even. Then i have defined another propety of even numbers(multiple n)

2)You have asked what is n ? n or m is same number about which i said it is even. I have used same vaiable . Since it is even it should follow second property (multiple). Multiple does not hold i have to prove this.

H1 l=[2,4,6,8,10] (n could be 2,4,6,8,10)

H2: In n l ->

Goal multiple n l=true (same l n (element of l) . To prove this statement what steps i should take?

Last updated: Oct 04 2023 at 19:01 UTC