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