1
$\begingroup$

I'm working through the "Properties of Relations" chapter of Software Foundations, but have got stuck on one of the exercises, lt_trans'':

Theorem lt_trans'' :
  transitive lt.
Proof.
  unfold lt. unfold transitive.
  intros n m o Hnm Hmo.
  induction o as [| o'].
  (* FILL IN HERE *) Admitted.

The base case for the induction is straightforward, but I'm stumped as to how to progress on the successor case. Proof state is:

  n, m, o' : nat
  Hnm : S n <= m
  Hmo : S m <= S o'
  IHo' : S m <= o' -> S n <= o'
  ============================
  S n <= S o'

To apply the induction hypothesis, I need S m <= o', but I only know that S m <= S o', and so it feels there is no way to make progress. Hoping someone can point me in the right direction as to how to solve this exercise.

$\endgroup$
1
$\begingroup$

Not all relations are transitive, so you're going to need to use the definition of lt and le, or some lemma that you've already proved about them.

Intuitively speaking, there are two cases: either $m = o'$ or $m \lt o'$. In the first case, Hnm says that $S(n) \le o'$, from which the conclusion is one application of le_S away. In the second case, you can apply IHo'.

This form of reasoning assumes some very well-known facts about arithmetic. (It's usually hard to formally prove something if you don't already have some intuition about the topic.) But you haven't proved them yet, so you can't directly use them. Instead, you have to make these cases appear via the construction of the data or the proof. It's very common to reason about the structure of a proof hypothesis: such-and-such hypothesis is of this form, and therefore it can only have been constructed in a certain way.

An important tactic for reasoning about the structure of a hypotheses in a non-recursive way is inversion. Roughly speaking, inversion does case analysis on a hypothesis and works out how these cases can be possible, unlike destruct which does case analysis but loses information on how the hypothesis could be possible. We want to reason about how $m \le o'$ can be possible, and there's a hypothesis that's very cloes to this: Hmo. So apply the tactic inversion Hmo.

I'll let you work out the details of the proof. If you don't care about the details, Coq will fill them in for you, but as a learning exercise you should complete these auto steps by hand.

Theorem lt_trans'' :
  forall n m o, n < m -> m < o -> n < o.
Proof.
  unfold lt.
  intros n m o Hnm Hmo.
  induction o; inversion Hmo; subst; auto.
Qed.
| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thanks, was able to fill in the details based on the above 👍 $\endgroup$ – Matt R Jun 14 at 17:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.