The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear Francisco,

Your lemma is a particular instance of the following

Lemma Acc_clos_refl_trans (A : Set) (R : A -> A -> Prop) s t :
  clos_refl_trans _ R s t -> Acc _ R s -> Acc _ R t.
Proof.
  induction 1 as [ s t H | | ]; auto.
  intros H1; revert H1 t H.
  induction 1 as [ s Hs IHs ]; intros t Hst.
  constructor; apply IHs; auto.
Qed.

Lemma test : forall m n, Acc nat gt (m + n) -> Acc nat gt m.
Proof.
  intros ? ?; apply Acc_clos_refl_trans.
  destruct n.
  rewrite <- plus_n_O; constructor 2.
  constructor 1; omega.
Qed.

Otherwise, I suggest you prove that the much stronger result
that Acc nat gt n holds for any n ...

Lemma Acc_any_rec : forall n m, n >= m -> Acc _ gt m.
Proof.
  induction n ...
Qed.

Theorem gt_wf : forall n, Acc _ gt n.
Proof.
  intros; apply Acc_any_rec with (1 := le_refl _).
Qed.

And after that, your test lemma become a no-brainer.

Good luck,

Dominique

On 07/19/2016 01:19 AM, Francisco Ferreira wrote:
> Hello everybody,
> I defined the following data type
> Inductive Acc (A : Set) (R : A -> A -> Prop) (t : A): Prop :=
> inj : (forall t': A, R t t' -> Acc A R t') -> Acc A R t.
> and I am trying to prove a lemma by induction on it. For example, it has
> the following shape.
> Lemma test: forall m n, Acc nat gt (m + n) -> Acc nat gt m.
> Trying to do induction on (Acc nat gt (m + n)) leads us to an hypothesis
> H0 : forall t' : nat, t > t' -> Acc nat gt m
> where t has no relation with m and n.
> Trying to use the remember tactics
> intros.
> remember (m + n) as t.
> induction H.
> leads us to an induction hypothesis
> H0 : forall t' : nat, t > t' -> t' = m + n -> Acc nat gt m
> but the clause t' = m + n is unsatisfiable for any t' < t.
> How I can use induction on Acc in such a way that the induction
> hypothesis preserves the information and is still usable?
> Thanks,
> Francisco
>