Stream: Coq users

Topic: co-existence

view this post on Zulip 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 2 hypothesis is false because of H1(r1=k1) & In r1(k2:: t).How i could prove it false?

view this post on Zulip zohaze (Apr 08 2023 at 03:42):

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

view this post on Zulip Laurent Théry (Apr 08 2023 at 08:51):

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

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

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

view this post on Zulip 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 not contradictory, it just means IH3 is useless : we cannot derive anything from it.

view this post on Zulip zohaze (Apr 14 2023 at 06:45):

ok.

Last updated: Apr 20 2024 at 03:40 UTC