Stream: Coq users

Topic: ✔ Prove heads of equal lists are equal


view this post on Zulip Roland Coeurjoly (Jun 08 2022 at 19:48):

I have the following context

2 goals (ID 731)

  a : Node
  children0 : list Node
  head : Node
  tail : list Node
  H : head :: tail = a :: children0
  ============================

How can I prove that a = head and tail=children0?
Note that we know that a and head are the heads of their respective lists, because they are of type Node.
Node is a inductive type I have defined.
I have tried intuition and constructor, without success.

view this post on Zulip Gaëtan Gilbert (Jun 08 2022 at 19:50):

injection H

view this post on Zulip Roland Coeurjoly (Jun 08 2022 at 19:59):

thanks @Gaëtan Gilbert it worked!

view this post on Zulip Notification Bot (Jun 08 2022 at 19:59):

Roland Coeurjoly has marked this topic as resolved.


Last updated: Feb 01 2023 at 13:03 UTC