Stream: Coq users

Topic: Proof with contradiction in hypothesis


view this post on Zulip Robert Soeldner (Feb 21 2021 at 08:09):

Hi, I currently struggle with the following proof obligation.

  x : Node
  H : mV x = Grey
  H1 : mV x = None
  ============================
  sndi x

From my (limited) understanding, this is already a contradiction since both H : mV x = Grey and H1 : mV x = None can't be true. Any help is highly appreciated.

view this post on Zulip Théo Winterhalter (Feb 21 2021 at 08:14):

Hi. Have you tried rewriting H into H1?

view this post on Zulip Théo Winterhalter (Feb 21 2021 at 08:15):

If Grey and None are both constructors of an inductive type, the discriminate h tactic will conclude the goal if h : Grey = None.

view this post on Zulip Guillaume Melquiond (Feb 21 2021 at 08:15):

If Grey and None are constructors, then they are indeed different. You can rewrite H into H1 and then discriminate over the new equality.

view this post on Zulip Théo Winterhalter (Feb 21 2021 at 08:16):

There is also the discriminate variant which finds the equality on its own.

view this post on Zulip Robert Soeldner (Feb 21 2021 at 08:17):

Thank you both, this was the missing part, which tool me hrs :P Zulip chat is such a help getting started.


Last updated: Jan 31 2023 at 14:03 UTC