I'm new to Coq and am working on some exercises with predicate logic. In one of the exercises, a transitivity hypothesis is defined as follows:
Hypothesis Transitive : forall x, forall y, forall z, R x y /\ R y z -> R x z.
I have derived the following:
R : D -> D -> Prop
a, b, c : D
Hab : R a b
Hbc : R b c
My goal is to derive Hac : R a c
as a hypothesis using Transitive. Seeing as I am new to Coq, I just tried some things I had seen before such as destruct (Transitive a b c).
but this would result in the error Not an inductive product
. So I figured I was supposed to provide Hab and Hbc
as well and tried destruct (Transitive a b c Hab Hbc).
which results in the following error: The term "Hab" has type "R a b" while it is expected to have type "R a b /\ R b c".
. Okay, so I need to derive something of the type R a b /\ R b c
first:
assert (R a b /\ R b c).
split.
exact Hab.
exact Hbc.
This indeed gives me an hypothesis H0 : R a b /\ R b c
of the correct type. When filling this in, destruct (Transitive a b c H0).
provides me with the error Not an inductive product.
again. I have searched for quite a bit but haven't been able to find any decent explanation of this error.
What exactly does this error tell me? Why did the other error tell me that something of type R a b /\ R b c
was required, but evaluation fails when this type is provided, again giving me this cryptic error about an inductive product? I'm looking for a bare bones Coq explanation and maybe solution, so no external packages. Note that I'm not looking to use or alter the target of the proof at all.