## Stream: Coq users

### Topic: both r equal

#### 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 04 2023 at 20:01 UTC