## Stream: Coq users

### Topic: co-existence

#### zohaze (Apr 07 2023 at 03:39):

``````H: chk r1 r2 (k1 :: k2 :: t)=true
H1: r1=k1
H2: r2=k2

IH3: k2::t<>[] ->
chk r1 r2 (k2:: t)=true->
In r1(k2:: t)->
In r2(k2:: t)->
f3 r2(k2:: t)=true->
f4 r2(k2:: t)=true.
``````

Co-existence of above 4 hypothesis is false because H1(r1=k1) & In r1(k2:: t).How i could prove it false?

#### zohaze (Apr 08 2023 at 03:42):

Plz, some one help me in proving H1 & IH3 are contra statement?

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

we don´t know was `f3` `f4` `chk` are. How can we help you....

#### Pierre Castéran (Apr 08 2023 at 09:28):

We asked several times for snippets in Coq we could download and replay, not trying to guess missing information.

#### zohaze (Apr 08 2023 at 11:07):

Yes, you have pointed out many times. But i have represented the functions by f1,f2..just to keep code simple. Secondly,
H1: r1=k1 & In r1(k2:: t) [in IH3] are not possible at a time (point of contradiction is clear here). Third whatever f3 & f4 it gives true on the basis of wrong assumption.Therefore it results in true=false. If i am wrong then just give comment on H1: r1=k1 & In r1(k2:: t) [in IH3] or how these f2 f3 play their role ? Thank u.

#### Laurent Théry (Apr 08 2023 at 13:24):

The fact that `In r1 (k2 :: t)` is not possible in `IH3` simply says that `iH3` is of the form `False -> ..`. So `IH3` is no contradictory, it just means `IH3` is useless : we cannot derive anything from it.

#### zohaze (Apr 14 2023 at 06:45):

ok.

Last updated: Oct 04 2023 at 21:01 UTC