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:
f2 a b las a list of something in H1 and as a bool in H2
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
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
f2produces 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
False and then get the equality
H1 as goal- and the premise
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 04 2023 at 23:01 UTC