pianke (Feb 23 2023 at 18:02): pianke (Feb 23 2023 at 18:02):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.
Laurent Théry (Feb 23 2023 at 22:11):could you give a concrete example so we can help you?
pianke (Feb 24 2023 at 18:04):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)?
Laurent Théry (Feb 24 2023 at 18:32):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?
Laurent Théry (Feb 25 2023 at 09:17):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.
Laurent Théry (Feb 25 2023 at 17:15):in my case, the information I could extract from In n l1 is the following :
Laurent Théry (Feb 25 2023 at 17:15):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?
Laurent Théry (Mar 04 2023 at 10:14):if l2 is a subset of l you should be able to prove is_even l = true -> is_even (f2 a l) = true
pianke (Mar 04 2023 at 15:45):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.
Laurent Théry (Mar 04 2023 at 18:40):1) What do you know about l?
2) So l containts only pair elements?
pianke (Mar 05 2023 at 05:58):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).
Laurent Théry (Mar 05 2023 at 09:59):what is the definition of multiple n l ?
pianke (Mar 08 2023 at 03:55):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.
Laurent Théry (Mar 08 2023 at 07:37):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?
Laurent Théry (Mar 09 2023 at 12:28):Again what is the definition of multiple n l?
pianke (Mar 11 2023 at 08:16):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 ?
Laurent Théry (Mar 11 2023 at 08:57):In your definition (remainder (divide h/2))) does not seem valid. Is that exactly your Coq definition?
Two other remarks
n in H2 for? If l iis some segment of even numbers, multiple l = true holds. No needs of n.suppose to have some segment of even numbers is expressed in your Coq file? pianke (Mar 11 2023 at 12:09):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