H : f1 (f2 X[s0,s1] (a :: l)) = [a]

IHl : f1 (f2 X[s0,s1] l) = [a] -> False

Above both are contra statements?

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.

f1 is not constant ,thank u.

Give us the definition of `f1`

`f2`

`X`

and we will tell you if there is a contradiction.

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?

what is `c0`

?

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.

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?

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
*)
```

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.

```
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.)

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

Ok, Thankyou.

Last updated: Oct 04 2023 at 21:01 UTC