The Coq mailing list

[Qinshi Wang <qinshiw AT cs.princeton.edu>]

Dear Fritjof,

It seems what you are trying to prove is not provable. Given (fun (x, y, z) = (x', y', z')), it is still possible that (x', y', z') comes from other branches, e.g. aa' or bb'. You must show these branches are not possible to give (x', y', z').

Best,

Qinshi

On Tue, Jul 7, 2020 at 12:19 AM 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.