The Coq mailing list

[Francisco Ferreira <fco AT 42nd.ca>]

Thank you for your answers! They really helped.

On Tue, Jul 19, 2016 at 5:49 AM, Dominique Larchey-Wendling
<dominique.larchey-wendling AT loria.fr>
 wrote:
> 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
>>
>