Stream: Coq users

Topic: conflict in statements


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

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

view this post on Zulip zohaze (Mar 31 2023 at 08:04):

f1 is not constant ,thank u.

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

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

view this post on Zulip Laurent Théry (Apr 03 2023 at 18:06):

what is c0?

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

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

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

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

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

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

view this post on Zulip zohaze (Apr 15 2023 at 06:02):

Ok, Thankyou.


Last updated: Jun 25 2024 at 15:02 UTC