Stream: Coq users

Topic: efficient way


view this post on Zulip sara lee (Feb 05 2023 at 17:05):

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.

view this post on Zulip Laurent Théry (Feb 05 2023 at 18:30):

How big is your list? Maybe you could use bool insteal of Prop:

view this post on Zulip Laurent Théry (Feb 05 2023 at 18:30):

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

view this post on Zulip sara lee (Feb 07 2023 at 13:35):

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.

view this post on Zulip Laurent Théry (Feb 08 2023 at 09:18):

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.

view this post on Zulip sara lee (Feb 08 2023 at 15:03):

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.

view this post on Zulip Laurent Théry (Feb 08 2023 at 18:59):

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.

view this post on Zulip sara lee (Feb 15 2023 at 13:10):

Thank you.
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.

view this post on Zulip Laurent Théry (Feb 15 2023 at 13:43):

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 my_list

view this post on Zulip sara lee (Feb 15 2023 at 17:06):

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?

view this post on Zulip Laurent Théry (Feb 15 2023 at 18:19):

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.

view this post on Zulip sara lee (Feb 16 2023 at 16:01):

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?

view this post on Zulip Laurent Théry (Feb 16 2023 at 16:48):

Let us start with the first question

view this post on Zulip Laurent Théry (Feb 16 2023 at 16:48):

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.

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

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.

view this post on Zulip sara lee (Feb 17 2023 at 17:44):

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?

view this post on Zulip Pierre Castéran (Feb 17 2023 at 19:17):

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.

view this post on Zulip zohaze (Feb 22 2023 at 16:52):

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

view this post on Zulip Laurent Théry (Feb 22 2023 at 17:15):

Rephrase your question. It is difficult to understand what you are asking.

view this post on Zulip zohaze (Feb 23 2023 at 14:18):

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

view this post on Zulip Pierre Castéran (Feb 23 2023 at 14:42):

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

view this post on Zulip zohaze (Feb 23 2023 at 16:55):

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

view this post on Zulip Laurent Théry (Feb 23 2023 at 17:15):

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.

view this post on Zulip Pierre Castéran (Feb 24 2023 at 07:38):

@zohaze
Here's another little example more.

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.

view this post on Zulip zohaze (Feb 26 2023 at 17:43):

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.

view this post on Zulip Julien Puydt (Feb 26 2023 at 17:59):

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

view this post on Zulip zohaze (Feb 28 2023 at 13:56):

Thank you.

view this post on Zulip zohaze (Apr 17 2023 at 12:37):

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.

view this post on Zulip Laurent Théry (Apr 17 2023 at 12:55):

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 13 2024 at 01:02 UTC