Stream: Coq users

Topic: conflict in statements

zohaze (Mar 31 2023 at 03:59):

H : f1 (f2 X[s0,s1] (a :: l)) = [a]
IHl : f1 (f2 X[s0,s1] l) = [a] -> False
Above both are contra statements?

Pierre Castéran (Mar 31 2023 at 06:35):

I would say "In general, no". But it may depend on the context (definitions, declarations) you didn't provide (under the form of a compilable snippet, please). For instance, `f1`may be a constant function.

zohaze (Mar 31 2023 at 08:04):

f1 is not constant ,thank u.

Laurent Théry (Mar 31 2023 at 08:24):

Give us the definition of `f1` `f2` `X` and we will tell you if there is a contradiction.

zohaze (Apr 03 2023 at 17:38):

H : a :: a1 :: t1 <> []
eq1: beq_nat a 2 = false
eq2: beq_nat a1 2 = false
remove 2 (a :: a1 :: remove 2 t1) = [c0].
Is it necessery to perform induction on t1?

Laurent Théry (Apr 03 2023 at 18:06):

what is `c0`?

Pierre Castéran (Apr 03 2023 at 18:20):

Under your hypotheses, you can prove the following equality (using lemmas from library `List`).

``````remove Nat.eq_dec 2 (a :: a1 :: remove Nat.eq_dec 2 t1) = a::a1:: remove Nat.eq_dec 2 tl
``````

Thus it can't be a singleton list.
Note that you forgot the first argument of `remove`. If you want some help, please test the snippets you post.

zohaze (Apr 14 2023 at 07:31):

c0 is natural number that exist in the list. @Pierre Castéran . You said "forgot the first argument of remove" i do't know its meaning. As far as i know remov require nat &list and i have written remove 2 t1 .(both exist). I am getting some different behaviour at this point(fix appears). Plz guide me how i can remove it. List never hold one element. How to fix remove?

Laurent Théry (Apr 14 2023 at 08:15):

which `remove` function are you using?
This is the one of the standard ibrary:

``````Require Import List.

Check remove.
(*
remove
: forall A : Type,
(forall x y : A, {x = y} + {x <> y}) -> A -> list A -> list A
*)
``````

Pierre Castéran (Apr 14 2023 at 08:37):

There is no need to fix Stdlib's `remove`. It works perfectly.

``````Require Import Arith List .
Import ListNotations.

Compute remove Nat.eq_dec 5 [6;5;9;10;5;0].
Compute remove Nat.eq_dec 5 [6;15;9;10;25;0].
Compute remove Nat.eq_dec 5 [5;5;5;5;5].
``````

Now, If you talk about another version of `remove`, you should tell from which library or give its definition.

zohaze (Apr 14 2023 at 10:43):

``````Fixpoint remove_all (v:nat) (s:list nat) :list nat :=
match s with
| [] => []
| h :: t => if beq_nat v h then remove_all v t else h :: remove_all v t
end.
``````

Secondly , is it important to have any information about tl ( H : a :: a1 :: t1 <> []). When i modify ( H : a :: a1 :: t1 <> []) to tl=[] then it works. Otherwise perform pattern matching on tl=[] or h::t'...
tl may be nil or not result should be same(result is False.)

Laurent Théry (Apr 14 2023 at 11:34):

``````Require Import List.
Import ListNotations.

Parameter beq_nat : nat -> nat -> bool.

Fixpoint remove_all (v:nat) (s:list nat) :list nat :=
match s with
| [] => []
| h :: t => if beq_nat v h then remove_all v t else h :: remove_all v t
end.

Goal forall a a1 t1 c0,
beq_nat 2 a = false ->
beq_nat 2 a1  = false ->
remove_all 2 (a :: a1 :: remove_all 2 t1) <> [c0].
Proof.
intros a a1  t1 c0 H1 H2.
simpl.
rewrite H1, H2.
discriminate.
Qed.
``````

zohaze (Apr 15 2023 at 06:02):

Ok, Thankyou.

Last updated: Jun 25 2024 at 15:02 UTC