Stream: Coq users

Topic: conversion of data type


view this post on Zulip zohaze (Jan 24 2023 at 14:59):

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?

view this post on Zulip 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.

view this post on Zulip 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 .

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

No In_dec can be used to define function.

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.

view this post on Zulip zohaze (Feb 15 2023 at 12:58):

In n1 l ->
In n2 l ->
In n3 l ->
f(n1+n2+n3 ) l.

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

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

Yes, you can prove it by induction on l. Here's a first (improvable) proof.

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.

view this post on Zulip 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?

view this post on Zulip zohaze (Apr 14 2023 at 07:14):

In above (a+b+c) exist in all elements then it give true.

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.

view this post on Zulip Laurent Théry (Apr 14 2023 at 07:29):

your question is not clear, sorry

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre Castéran (Apr 18 2023 at 14:26):

pianke said:

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.

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

So, you can use one of the two following definitions.

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.

and establish a logical relation between F and f.

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.

view this post on Zulip 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?

view this post on Zulip zohaze (Apr 29 2023 at 06:50):

Like this

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.

a b c are locally calculated in F1. In F1 there is condition a>0 b>0 c>0.

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?


Last updated: Jun 14 2024 at 19:02 UTC