Stream: Coq users

Topic: use of lia.


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

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

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

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

view this post on Zulip Laurent Théry (Apr 15 2023 at 12:29):

This makes no sense....

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

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

view this post on Zulip Paolo Giarrusso (Apr 15 2023 at 13:16):

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

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

view this post on Zulip Laurent Théry (Apr 15 2023 at 21:26):

it makes no sense because a :: b :: c :: f2 a b l means that f2produces a list andf2 a b l3 = true means f2 returns a boolean.

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

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

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

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