CODEWITHSUNDEEP
logiccoq
larsr
larsr

Reputation: 5811

Proof about less than

I'm trying to prove some theorems about less_than in Coq. I'm using this inductive definition:

Inductive less_than : nat->nat->Prop :=
   | lt1 : forall a, less_than O (S a)
   | lt2 : forall a b, less_than a b -> less_than a (S b)
   | lt3 : forall a b, less_than a b -> less_than (S a) (S b).

and I always end up needing to show the inverse of lt3,

Lemma inv_lt3, forall a b, less_than (S a) (S b) -> less_than a b.
Proof.
   ???

I'm stuck, and would be very grateful if someone have some hints on how to proceed.

(Is there something wrong with my inductive definition of less_than?)

Thanks!

Upvotes: 1

Views: 120

Answers (1)

Ptival
Ptival

Reputation: 9437

First thing, your definition of less_than is a bit unfortunate in the sense that the second constructor is redundant. You should consider switching to the simpler:

Inductive less_than : nat -> nat -> Prop :=
| ltO : forall a, less_than O (S a)
| ltS : forall a b, less_than a b -> less_than (S a) (S b)
.

The inversion would then match coq's inversion, making your proof trivial:

Lemma inv_ltS: forall a b, less_than (S a) (S b) -> less_than a b.
Proof. now inversion 1. Qed.

The second clause was redundant because, for every pair (a, b) st. you want a proof of less_than a b, you can always apply lt3 a times and then apply lt1. Your lt2 is in fact a consequence of the two other constructors:

Ltac inv H := inversion H; subst; clear H; try tauto.

(* there is probably an easier way to do that? *)
Lemma lt2 : forall a b, less_than a b -> less_than a (S b).
Proof.
  intros a b. revert a. induction b; intros.
  inv H.
  inv H.
  apply ltO.
  apply ltS. now apply IHb.
Qed.

Now if you really wish to keep your particular definition, here is how you could have attempted the proof:

Lemma inv_lt: forall a b, less_than (S a) (S b) -> less_than a b.
Proof.
  induction b; intros.
  inv H. inv H2.
  inv H. apply lt2. now apply IHb.
Qed.

Upvotes: 5

Related Questions