The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

The "fun (x,y,z) = (x',y',z') -> fun1 a = a' /\ fun2 b =b'" direction
would only be true if none of the other match cases in fun produce 
(x',y',z').  

I would proceed by unfolding fun in the hypothesis and eliminating both
"fun1 a" and "fun2 b" keeping their equalities (hence using case_eq or
destruct eqn: tactics).  The match cases that do correspond to a' and
b' will then be easy to prove from those equalities.  The others will
require some way to show their results are not (x',y',z'), hence a
contradiciton - which means some decidable equality on that triple.

On Mon, 6 Jul 2020 18:19:46 +0200
Fritjof <fritjof AT uni-bremen.de> wrote:

> Hi,
> 
> I have the following theorem:
> fun1 a = a' /\ fun2 b = b' <-> fun (x,y,z) = (x',y',z').
> 
> fun1 and fun2 are called inside the function fun:
> fun(x,y,z)
>  match fun1 a with
>    | a' => match fun2 b with 
>            | b' => (x',y',z') (* these values are calculated somehow
> *) | bb' => 
>    | aa' => ...
>  end 
> 
> 
> I can show the following: fun1 a = a' /\ fun2 b = b' -> fun (x,y,z) =
> (x',y',z').  (the first part)
> 
> But not the second one: fun (x,y,z) = (x',y',z') -> fun1 a = a' /\
> fun2 b = b'. I didn't find a way to feed the left side of the
> implication into the hypothesis: fun (x,y,z) = (x',y',z').
> 
> Does someone has a hint for me how to solve this? 
> 
> Best regards,
> --f.