Stream: Coq users

Topic: simlify list


view this post on Zulip pianke (Mar 16 2023 at 05:17):

H2: match value d [y] with
 | []=>false
 |b::l=>....

First case is false due to the occurence of y in list. To simplify H2 , i should apply induction on [y]. Or un fold vaue function in H2 to show and prove that this function gives false only in case of empty input list. One element of list is y,If i need information of second elements of same list then i have to apply induction again or simply apply destruct? What is the simplest way of simplify above?

view this post on Zulip Pierre Courtieu (Mar 16 2023 at 08:50):

Hi, the answer depends completely on the definition of value. This is precisely why we ask to always give a completely compilable code snippet. If value is a fixpoint decreasing on its second argument, then probably unfold is the way to try, if not, well, I need more.


Last updated: Jun 14 2024 at 20:01 UTC