conversion of data type · Coq users

if x is member of a list then it will be equivalent to In x l? Output data type of In predicate is proposition and member function has bool output. Could we prove their equivalence/ convert them?

Laurent Théry (Jan 24 2023 at 15:05):

Check the theorem in_dec, you need to be able to decide equality on the elements of the list.

zohaze (Jan 25 2023 at 08:37):

in_dec is {In n l} + {~In n l}. But still answer will be in proposition. I want to ask, if in Coq code lemma statement and its proof (related to In n l present /exist) then could i replace it with a function which check the presence of n in list? Only benefit i want to get is the bool data type at output instead of prop .

Laurent Théry (Jan 25 2023 at 09:18):

Require Import List Arith.

(* Test if i is in l *)
Definition test i (l : list nat) :=
match In_dec Nat.eq_dec i l with
 left _ => true
| right _ => false
end.

(* Compute the intersection of 2 lists *)
Definition inter (l1 l2 : list nat) := filter (fun i => test i l1) l2.

Definition l1 := 3 :: 5 :: 7 ::8 :: 9 :: nil.
Definition l2 := 2 :: 5 :: 9 :: nil.

Compute inter l1 l2.

zohaze (Feb 15 2023 at 12:58):

f function is inductively defined function and output is Prop. I want to ask
1) May i convert it into boolen output directly (like)
f(n1+n2+n3 ) l=true
2) I have to re-define f in recursive form (so that its output is bool)?

Laurent Théry (Feb 15 2023 at 13:47):

Nop you can't translate Prop to bool directly. What people sometime do is to have a function f : nat -> Prop for proof and define a bool version g : nat -> bool for computation and then prove forall x, f x <-> g x = true. Others work directly only with g.

zohaze (Feb 15 2023 at 17:18):

Yes, i am doing the same thing. Now defining bool version. f is inductively defined. I am asking ,now i should use recursive definitions to define g ? New i have to define equivalent of f definition in the form of bool ? So that function behaviour remains the same.

Pierre Castéran (Feb 15 2023 at 18:01):

It could have been better if you had posted the code you are working on (the function f for instance)
(for us to save time and give an appropriate answer).

Here is an artificial example, where Pis an inductive predicate and pa recursive Boolean function.

Import ListNotations.

Inductive P (a b c: nat) : list nat ->  Prop :=
  here : forall x l, x = a+b+c -> P a b c (x:: l)
| next : forall x l, P a b c l -> P a b c (x::l).

Goal P 1 2 3 [4;5;6;7].
 do 2 right; now left.
Qed.

Fixpoint p a b c (l: list nat) : bool :=
  match l with
  | nil => false
  | x::tl => if Nat.eqb (a+b+c) x then true else p a b c tl
  end.

Compute p 1  2 3 [4;5;6;7].

Lemma p_OK : forall a b c l, P a b c l <-> p a b c l= true.

zohaze (Feb 16 2023 at 16:20):

Lemma p_OK : forall a b c l, P a b c l <-> p a b c l= true. is necessery after defining the function in both forms.

Pierre Castéran (Feb 16 2023 at 16:55):

Lemma p_OK : forall a b c l, P a b c l <-> p a b c l = true.
Proof.
  induction l; simpl;split; intro H.
  - inversion H.
  - discriminate.
  - case_eq (a+b+c =? a0).
      + easy.
      + inversion_clear H.
       * subst a0; rewrite Nat.eqb_refl; discriminate.
       * now rewrite IHl in H0.
  -  case_eq (a + b + c =? a0).
     + intro H0;  left; rewrite Nat.eqb_eq in H0; auto.
     + intro H0; rewrite H0 in H; right; now rewrite  IHl.
Qed.

zohaze (Mar 11 2023 at 12:53):

Natural number list is maintaing some patteren arrangement. The property on the basis of which list is made can be express by
using recursive function. In this case property expression is like a boolean exprssion of patteren maintained by list or how list is made.
hold_p l = true -> hold_p (p a b c l) = true. Is this possible way of expessing list property?

zohaze (Apr 14 2023 at 07:14):

Mylist=[c1,c2,c3,c4...].
I am checking the presence of all elements of the list in different lists l1,l2,l3.. (recursively).Like
In c1 l1 In c2 l2 In c3 l3 ... then it gives true. When bool data type is true then this condition is fullfilled by all elements of list.
Now i am selecting two elements c2 & c3 and have hypothesis H0: In c2 l2 H1: In c3 l3 .Then how i could write as you written
(if Nat.eqb (a+b+c) x then true else p a b c tl)? In prdicate gives Prop but i have converted it into bool for easyness.

Laurent Théry (Apr 14 2023 at 07:29):

pianke (Apr 17 2023 at 11:56):

In first constructor add three numbers then add in l. What is the meaning of second constructor?
| next : forall x l, P a b c l -> P a b c (x::l).
2)When i run the code at point where apply easy command .At this point i got this error "Tactic failure: Cannot solve this goal."
What alternate command i should apply?
3) is there any differnce between eauto and easy command?

Pierre Castéran (Apr 17 2023 at 12:42):

@pianke Do you refer to the code I posted on Feb 15th and/or 16th ?
It was only an example on the property " the list lcontains at least an element equal to a+b+c ". It works if you import Arith, List andListNotations before.
If easydoesn't work on your Coq installation, you may try reflexivity or trivial.

pianke (Apr 18 2023 at 12:27):

1) I have already included these libraries. When apply reflexivity instead of easy, this command is accepted by Coq but it do nothing. Same for trivial.

2) Yes. 15Feb post. I need conversion therefore i am taking your given example as a reference . But all elements of list should be sum of three numbers. Then why there is need of "| next : forall x l, P a b c l -> P a b c (x::l).".Just explain meaning of writing this constructor.

Pierre Castéran (Apr 18 2023 at 14:26):

Sorry, but I didn't see the sentence "But all elements of list should be sum of three numbers" in the previous posts (not precise enough).
So my proposition implemented another proposition "there exists in l an element equal to a+b+c".

Definition f a b c l: bool := forallb (fun x => x =? a + b +c) l.

Definition F a b c l: Prop := Forall (fun x => x = a + b + c) l.

This is an example of the issues which happen when questions are incomplete or too informal.
We spend a lot a time to guess what it is about, and may give a useless answer because there may be various ways to interpret a question.

zohaze (Apr 26 2023 at 07:11):

No change means ,after applying command there is no change in code (no simplification). This is all about conversion,In my case there is difference in the used arguments/variables in function definition inductive form and in bool form. Could i proceed in present form or i have to redefine function in boolean form with equal arguments?

zohaze (Apr 29 2023 at 06:50):

Lemma p_OK : forall a b c l, P a b c l <-> p a b c l = true"
but difference of input arguments exist.
F1 x y l = f1 a b c x y l.

But in f1 there is no condition on a>0 b>0 only on c >0.
Problem is here.
When unfold f1 then i get following msg during recursive call of f1 (fix a0 b0 c0....). How i remove it and make it simple? Function testing gives correct results because c is the multiplication of a and b.Therefore if c>0 then a and b are also greater than 0. Plz help me how i could solve this?

Stream: Coq users

Topic: conversion of data type

zohaze (Jan 24 2023 at 14:59):