pianke (Mar 16 2023 at 05:17): 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?
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: Oct 13 2024 at 01:02 UTC