```
H1: f (a :: b ::c::f2 a b l) = [d]
H2: f2 a b l = true ->
f (a :: b ::c::f2 a b l) <> [d]
```

I am using lia to close contradiction but it does not works. I have H2.

I am not sure why you believe lia should be able to solve this - lia is for "Linear Integer Arithmetic" and this goal doesn't have much to do with integer arithmetic. lia has become quite powerful in the past and solves a lot of goals it is not really advertised to solve, but one shouldn't expect it could solve just any goal.

There are a few issues with your goal:

- it does not type check because you are using
`f2 a b l`

as a list of something in H1 and as a bool in H2 - you would need
`f2 a b l = true`

- without this there is no contradiction between H1 and H2.

As usual my recommendation is to post code that compiles as is - it saves time for you and others.

H2: f2 a b l3 = true ->

f (a :: b ::c::f2 a b l) <> [d] & f2 a b l3 = true in hypothesis. Both l are same l3 is different.

This makes no sense....

FWIW, I _have_ seen `lia`

do some intuitionistic reasoning, but more proper tactics for that are `tauto`

, `intuition lia`

(or installing and using `itauto`

). But I agree with Michael's points.

IMHO, the main problem is that we are asked to look at goals that could never exist (e.g. the type inconsistency with `f2`

mentionned by Michael). I'm OK to explain a non-understood error message, or try to help in a difficult formalization or proof step, but only if I can try to make the code run.

I will say: I admire your patience in even trying.

Thanks to all for comment and reply. I have no knowledge as all of you have. But why statement have no sense.

H1: f (a :: b ::c::f2 a b l) = [d]

H2: f2 a b l3 = true ->

f (a :: b ::c::f2 a b l) <> [d]

Same statement( f (a :: b ::c::f2 a b l) = [d]) & <d> in the presence of (f2 a b l3 = tru) . And i have this in hypothesis also.It is some thing exfalso.

it makes no sense because `a :: b :: c :: f2 a b l`

means that `f2`

produces a list and`f2 a b l3 = true`

means `f2`

returns a boolean.

@pianke So you have a working code somewhere and you are trying to prove something about it and the goal you posted is a part of it, I am assuming. People here are busy and can’t offer you a lot unless your question makes sense. @Michael Soegtrop already asked you to post a code so if you do, you will get a lot of answers.

ok. Found mistake. @ Laurent Thery.( f3 a b l3 = true ,which has no relation with others) or even remove it. Then which command i should use.

ok @pianke, so next time when you ask for something try to ask your question with some valid Coq code. For example,

How can I prove this?

```
Require Import List.
Import ListNotations.
Parameter f : list nat -> list nat.
Parameter f2 : nat -> nat -> list nat -> list nat.
Parameter f3 : nat -> nat -> list nat -> bool.
Goal forall a b c d l l3
(H1: f (a :: b ::c::f2 a b l) = [d])
(H2: f3 a b l3 = true -> f (a :: b ::c::f2 a b l) <> [d])
(H3: f3 a b l3 = true), False.
```

then we can anseer

```
Goal forall a b c d l l3
(H1: f (a :: b ::c::f2 a b l) = [d])
(H2: f3 a b l3 = true -> f (a :: b ::c::f2 a b l) <> [d])
(H3: f3 a b l3 = true), False.
Proof.
intros a b c d l l3 H1 H2 H3.
now destruct H2.
Qed.
```

Here is an alternative to the method suggested by @Laurent Théry : which might give more insight into what is going on:

```
intros a b c d l l3 H1 H2 H3.
apply H2.
exact H3.
exact H1.
```

The point is that `a <> b`

is an abbreviation for `a = b -> False`

. So you can apply `H2`

to `False`

and then get the equality `H1 as goal`

- and the premise `H3`

.

`destruct H2`

here as the same effect as `apply H2`

(but is IMHO less obvious) and `now`

just says "whatever comes after the tactic is trivial". So `now apply H2`

also works.

Last updated: Jun 18 2024 at 09:02 UTC