zohaze (Apr 15 2023 at 06:04): 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:
f2 a b l as a list of something in H1 and as a bool in H2f2 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.
Paolo Giarrusso (Apr 15 2023 at 13:16):I will say: I admire your patience in even trying.
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 f2produces a list andf2 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.
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: Oct 13 2024 at 01:02 UTC