pianke (Mar 30 2023 at 13:03): pianke (Mar 30 2023 at 13:03):I want to prove function equality of two functions f1 & f2. Whose input arguments are nat and nat list and output is bool.Matching patteren of these functions is input list.
I should move in the following way
1) [] of f1= [] of f2
2) [a] of f1= [a] of f2
3)(a::t) of f1= (a::t) of f2
How to terminate the third case.In hypothesises i have all the conditions under which f1 give true in the case of two elements
in the input list. I have to relate these conditions with f2 for each and every case?
Laurent Théry (Mar 30 2023 at 13:19):looks like you should use the induction hypothesis f1 l = f2 l in order to prove that f1 [a::l] = f2 [a::l]
pianke (Mar 31 2023 at 08:16):Yes. When apply induction then one element appears in the list and hypothesis gives all test conditions true.Then second time
two elements and their hypothesis ....in f1. I want to ask how to terminate . Now list is not empty,true required hypothesis (related to f1) including induction hypothesises. Now i have to use these induction hypothesises to prove f2? Stop induction after two time?
Laurent Théry (Mar 31 2023 at 08:20):how to use the induction depends of the definition of f1 and f2. If you don't give us their definition it is difficult to help you.
Last updated: Oct 13 2024 at 01:02 UTC