I have multiple solid structures ,their length width and height is represented by S (x y z) . Made list of these like
[ S (x1 y1 z1),S (x2 y2 z2) , S (x3 y3 z3),... S (xs ys zs)].
I am randomly select one structure and want to find its match in the list. I am using In n l (Prop), but problem is that when list become too lengthy then system become too slow ,some time never respond.
How big is your list? Maybe you could use bool insteal of Prop:
Require Import List. Inductive Solid := solid : nat -> nat -> nat -> Solid. Definition eq_solid (s1 s2 : Solid) := let '(solid x1 y1 z1) := s1 in let '(solid x2 y2 z2) := s2 in (Nat.eqb x1 x2 && (Nat.eqb y1 y2 && Nat.eqb z1 z2))%bool. Definition big_list n := repeat (solid 1 2 3) n ++ solid 3 4 5 :: nil. Time Compute existsb (eq_solid (solid 3 4 5)) (big_list 100). Time Compute existsb (eq_solid (solid 3 4 5)) (big_list 1000). Time Compute existsb (eq_solid (solid 3 4 5)) (big_list 10000).
When we should use bool and Prop (related to list length). What should be length in case of bool?
I have hypothesis H0: In S(x22 y22 z22) [ S(x4 y4 z4); S(x21 y21 z21); S(x19 y19 z19).....].No of elements are nearly 1000.
To write it in term of bool, i have to convert H0 in term of Nt.eqb.(as you suggested). But it would be difficult Nt.eqb for so many numbers.
Here it is
Lemma eq_solid_true s1 s2 : eq_solid s1 s2 = true <-> s1 = s2. Proof. destruct s1 as [x1 y1 z1]. destruct s2 as [x2 y2 z2]. simpl. destruct (PeanoNat.Nat.eqb_spec x1 x2) as [->|Dx1x2]; destruct (PeanoNat.Nat.eqb_spec y1 y2) as [->|Dy1y2]; destruct (PeanoNat.Nat.eqb_spec z1 z2) as [->|Dz1z2]; split; try (discriminate || trivial); intros H; inversion H; (now destruct Dx1x2 || now destruct Dy1y2 || now destruct Dz1z2). Qed. Lemma In_exists (s : Solid) (l : list Solid) : existsb (eq_solid s) l = true <-> In s l. Proof. apply iff_trans with (1 := existsb_exists _ _). split. - intros [x [H1x H2x]]. assert (H: s = x) by now apply eq_solid_true. now rewrite H. - intros Hl; exists s; split; try trivial. now apply eq_solid_true. Qed.
Thank you. Sorry question is becoming lengthy. One point that is not clear to me that is , how i should make list of solid? Like list of 1000 solids
[ S(x1 y1 z1); S(x2 y2 z2)....... S(x1000 y1000 z1000)] (error unknown x1y1z1....) OR
[S1,S2....S1000) .Secondly, some time there are 300 elements which i have to put in list and some time 500 elements.Therefore i should use generalize form to make list,like Definition list (n:nat)(S:solid) :=[?]. Third
I have hypothesis H0: In S(x22 y22 z22) [ S(x4 y4 z4); S(x21 y21 z21); S(x19 y19 z19).....]. it has no use here.
If your list does not contain Solid with explicite value (S 4 5 6). You need to write a bit of Ltac
Require Import List Lia. Import ListNotations. Inductive Solid := solid : nat -> nat -> nat -> Solid. Parameter x : nat -> nat. Parameter y : nat -> nat. Parameter z : nat -> nat. Fixpoint iota (m n : nat) : list nat := match n with | 0 => nil | S n' => m :: iota (S m) n' end. Compute iota 3 5. (* Build m :: m + 1 :: n *) Definition range m n := iota m (S n - m). Compute range 3 7. Definition solid_list m n := map (fun n => solid (x n) (y n) (z n)) (range m n). Definition my_list := Eval compute in solid_list 1 50. (* find the index of x in l *) Ltac find_nth x l := match l with  => 0 | (x :: ?l1) => constr:(0) | (_ :: ?l1) => let v := find_nth x l1 in constr:(1 + v) end. Ltac solve_In_tac := match goal with |- In ?x ?l => let n := find_nth x l in let H := fresh "H" in assert (H : x = nth n l x) by trivial; rewrite H at 1; apply nth_In; simpl; lia end. Goal In (solid (x 49) (y 49) (z 49)) my_list. unfold my_list. solve_In_tac. Qed.
In (solid (x 5) (y 6) (z 7)) my_list.( it works)
In (solid (x Sx1) (y Sy1) (z Sz1)) my_list.( but not work in this form). While x1 y1 z1 are nat.
Can you give the exact coq code you are trying. I don't understand why you expect
(solid (x Sx1) (y Sy1) (z Sz1)) to be in
same as above "Goal In (solid (x 49) (y 49) (z 49)) my_list." We can check any solid with x y z from 1-50 in the list.
But when have H: In (solid (x x1) (y y1) (z z1)) my_list. Then what its means? I can't check it unless destruct x1,y1 &z1. In this way i have to apply destruct command every time before applying solve_In_tac. Otherwise it does not solve. How H: In (solid (x x1) (y y1) (z z1)) my_list could be helpful?
If you have
In (solid (x x1) (y y1) (z z1)) my_list, you can do a case analysis, either the solid is at the first element of the list or in the remaining list.
Goal forall x1 y1 z1, In (solid (x x1) (y y1) (z z1)) (my_list ++ solid (x x1) (y y1) (z z1) :: nil) -> False. intros x1 y1 z1 H. destruct (in_inv H) as [Heq|H1]. Show 1. Show 2.
First, thanks. I want to know the meaning of this statement " H: In (solid (x x1) (y y1) (z z1)) my_list." . Its meaning is " What ever the value of x1 y1 z1 is , then solid with these values is present in list ? In this case there are multiple values that may be or may not be present in mylist.
2) In above reply ( In (solid (x x1) (y y1) (z z1)) (my_list ++ solid (x x1) (y y1) (z z1) :: nil) -> False.) How you came to know it will give False.( x0 y0 z0) might be present ,another possibility in case of Succ x2 y2 z2)
3) Definition mylist := list nat.
List.In a1 mylist.
error " mylist has type "Set" while it is expected to have type list ?".
To remove this error i must define nat value in the list ( like mylist= [3;5;78;9]. )These natural numbers are varying therefore
i am representing it in the form mylist( whatever the value present in mylist) , is it possible?
Let us start with the first question
Require Import List. Import ListNotations. Inductive Solid := solid : nat -> nat -> nat -> Solid. Lemma example1 : forall x1 y1 z1, In (solid x1 y1 z1) [solid 1 2 3; solid 4 5 6] -> (x1 = 1 /\ y1 = 2 /\ z1 = 3) \/ (x1 = 4 /\ y1 = 5 /\ z1 = 6). Proof. intros x1 y1 z1 H. destruct (in_inv H) as [Heq|H1]. - injection Heq; intros; left; now repeat split. - destruct (in_inv H1) as [Heq|H2]. + injection Heq; intros; right; now repeat split. + now destruct (@in_nil _ (solid x1 y1 z1)). Qed.
About your third question:
There is a confusion between the
:(type declaration) and
:= (definition) symbols.
You should have typed something like:
Definition my_list : list nat := [3;4;5]. Check my_list. Check list nat.
Regards to both of u. @Pierre Castéran i have problem here. You have written in this way " Definition my_list : list nat := [3;4;5]." But i cannot define the elements in the list like [3;4;5]. Because this list is randomly generated and i have only information that it is a natural number list/solid. Therefore i want to represent it by notation like l1. Definition my_list : list nat := l1.
or Definition my_list : list solid := l1. Then check the presence of one given element in the list.
2) You have used split repeat commands two time for two number of elements. But if there are more than 100 elements then
then i have to use these commands 100 time in this case it will become too lengthy. Is there any short _cut?
Perhaps you should consider
l1as a local variable declared inside a section.
Require Import List Arith Lia. Import ListNotations. Section Any_list. Variable l1: list nat. Lemma In_occ x : count_occ Nat.eq_dec l1 x > 0 <-> In x l1. induction l1. - simpl; lia. - simpl. destruct (Nat.eq_dec a x). + split. * left; congruence. * auto with arith. + split; tauto. Qed. End Any_list. About In_occ. Goal In 3 [1;2;3;4;3;6;1]. rewrite <- In_occ. simpl; auto with arith. Qed.
Definition my_list : list nat := [3;4;5]. This is form about which i am asking. Now one problem is left, that is
Fixpoint f (a n:nat)(l:list nat):list nat:= (Here i am relating output of f with my_list as )
Fixpoint f (a n:nat)(l:list nat):list nat:=my_list and then how i can assign [3;4;5] this or relate all three points
Rephrase your question. It is difficult to understand what you are asking.
I have natural number list (my_list) as output argument of function f ,having elements in particular patteren . Want to use this list as input argument to another function f2.
1) How to declare list (my_list)? (As
Variable my_list:list nat.
Fixpoint f (a n:nat)(l:list nat):my_list:
(In this case error msg: my_list should be Set, Prop or Type.)
2) Now my_list is use as input argument in f2. f2 is defined as
Fixpoint f2 (a1 n1:nat)(l:list nat): list nat:
Now again define
Variable ext_list:list nat.
Now question is about the usage of my_list & ext_list in f2.
Fixpoint f2 (a1 n1:nat)(my_list:list nat): ext_list nat:
3) In theorem writing , i want to use same my_list & ext_list . After writing theorem statement ,i should close section?
4) How i can check the elements of both list (my_list & ext_list)?
If you post an exact copy of what you typed, we could comment and explain the error messages.
There are a few errors I could guess already: typing errors like in
ext_list nat, confusion between definition and declaration).
1) Both (my_list & ext_list) are list nat. I have locally generated a list by command " Variable my_list : list nat ". Then pass it to below function f2 as
Fixpoint f2 (a n:nat)(my_list : list nat) : list nat:
2) Now again output of f2 is list nat. Is there is a way to give a name or way of declartion or access way to this list? I have problem how to write something about this list or how to call it, how to write some property about this list? I have no code,have problem in writing at begining. I am using basic definitions,no idea about declaration. Regards
Does this help?
Require Import List. Import ListNotations. Section Test. Variable my_list : list nat. Fixpoint f (l : list nat) := match l with | a :: b :: l => a :: f l | _ => l end. Compute (f [1; 2; 3; 4]). Definition my_result := f my_list. End Test.
Here's another little example more.
Failcommands illustrate the typing errors.
any_listbecomes an argument of
Require Import Arith List. Import ListNotations. Section MyList. (* A local definition *) Let my_list : list nat := [1;2;3]. (* A declaration *) Variable any_list : list nat. (* typing errors *) Fail Check my_list nat. Fail Check my_list [5;6;7]. (* A definition which depends on any_list *) Definition f : list nat := my_list ++ any_list. Fixpoint g (l: list nat) : list nat := match l with nil => nil | a::tl => any_list ++ (a:: g tl) end. End MyList. (* f is now a function and g has two arguments *) Print f. Compute f [4;5;6]. Compute f (repeat 4 10). Print g. Compute g [0;1;2;3] [4;5;6].
Hope this helps.
Variable any_list : list nat.
Definition any_list:=list nat. Plz tell the difference between two statements.
As far as i know Variable is define inside a section , use locally within section and second one is use globally or from library /data base.
Variable statement assumes there's an objets of this type. The
Definition statement creates a type aliasing:
Section Foo. Variable toto: list nat. Definition tata := list nat. Check toto. (* toto: list nat *) Check tata. (* tata: Type *) End Foo.
I have list l & In al In b l & In c l in hypothesis. Want to prove another function X in the presence of all these. I proved it.But next time i come across different list and all other thing remain same. How i should proceed that in the presence of all hypothese and same X is valid on different l.
You should prove something like
Lemma my_theorem : forall (a b c : nat) (l : list nat), In a l -> In b l -> In c l -> ...
Last updated: Oct 04 2023 at 23:01 UTC