Destructing transitivity hypothesis on simple predicate logic

Question

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.

Answer 1

You seem to misunderstand what destruct is for. destruct takes a term whose product is an inductive type, and performs case analysis. For example, if you have the hypothesis H : A /\ B, destruct H as [HA HB]. gives you two hypotheses HA : A and HB : B. If you have H : A \/ B, destruct H as [HA | HB] (note the pipe, to separate the cases) splits the proof into two subproofs, one where you have HA : A and one where you have HB : B.

If you have already understood the basics of the underlying theory behind Coq, destruct just corresponds to pattern matching in Gallina.

In this case, Transitive a b c H0 has type R x z. Since R x z is a Prop that you have no further knowledge on, there is no meaningful case analysis that you can do on it. But that's not a problem since destruct is not the tool you're looking for in the first place. In general, if you want to add a new hypothesis after having proved it, you should use assert like so:

Hypothesis (D : Type) (R : D -> D -> Prop) (a b c : D) (Hab : R a b) (Hbc : R b c).
Hypothesis Transitive : forall x y z, R x y /\ R y z -> R x z.
Goal 1+1=2. (* dummy goal for demonstration purposes *)
  assert (Hac : R a c). {
    apply Transitive with (y := b). split; [exact Hab | exact Hbc].
  }
  (* Continue your proof with the new hypothesis Hac *)

Or you could write the proof term yourself (this works in simple cases like this):

Hypothesis (D : Type) (R : D -> D -> Prop) (a b c : D) (Hab : R a b) (Hbc : R b c).
Hypothesis Transitive : forall x y z, R x y /\ R y z -> R x z.
Goal 1+1=2. (* dummy goal for demonstration purposes *)
  assert (Hac := Transitive a b c (conj Hab Hbc)).
  (* Continue your proof with the new hypothesis Hac *)

Answer 2

It is normal since the conclusion of Transitive is R x z, using destruct fails. So maybe what you really want to do is

assert (R a c).
apply (Transitive a b c).