The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,
you need to be more precise, see below:

Le lun. 6 juil. 2020 à 18:20, Fritjof <fritjof AT uni-bremen.de> a écrit :
>
> Hi,
>
> I have the following theorem:
> fun1 a = a' /\ fun2 b = b' <-> fun (x,y,z) = (x',y',z').

What does "I have" mean? You have it proved? Or You want to prove it?

> 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

this is not a valid coq definition. Do you mean this?

Definition 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.

1) Note that "fun" is a reserved keyword so this is probably not
accepted by coq.
2) I don't see why the "<-" of your theorem is true. It amounts to
proving that fun is injective probably. So again: is the theorem
proved or are you trying to prove it. In the latter case for what
reason would it be true from right to left?

>
> 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').

I think you are trying to prove something either false or quite non trivial.

Best

P
> Does someone has a hint for me how to solve this?
>
> Best regards,
> --f.