Stream: Coq users

Topic: induction & matching pattern


view this post on Zulip zohaze (Nov 08 2021 at 18:12):

I have defined recursive function f. In this function pattern matching occurs on two parameters (a:nat & b<?c:bool relation) and have a>>c . Q1)No of time recursive function is being call is equal to smaller value of pattern matching(c) or output elements of function are equal to c? Q2)To prove output is equal to c what constraint I should have ? Q3) First perform induction on a then destruct c or (b<? c) for simplification?


Last updated: Jan 28 2023 at 06:30 UTC