conflict in statements · Coq users

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, f1may be a constant function.

zohaze (Mar 31 2023 at 08:04):

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

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

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

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.

Stream: Coq users

Topic: conflict in statements

zohaze (Mar 31 2023 at 03:59):