## Stream: Coq users

### Topic: use of lia.

#### zohaze (Apr 15 2023 at 06:04):

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

#### Michael Soegtrop (Apr 15 2023 at 08:13):

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.

#### pianke (Apr 15 2023 at 11:12):

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.

#### Laurent Théry (Apr 15 2023 at 12:29):

This makes no sense....

#### Paolo Giarrusso (Apr 15 2023 at 12:36):

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.

#### Pierre Castéran (Apr 15 2023 at 13:06):

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.

#### pianke (Apr 15 2023 at 19:36):

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.

#### Laurent Théry (Apr 15 2023 at 21:26):

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.

#### Mukesh Tiwari (Apr 15 2023 at 21:27):

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

#### pianke (Apr 16 2023 at 04:50):

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.

#### Laurent Théry (Apr 16 2023 at 08:07):

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

#### Michael Soegtrop (Apr 17 2023 at 09:25):

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