From 98e6192842f7c8f855bbbffeaca5b3d68a2fd854 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Sep 2014 16:37:30 +0200
Subject: [PATCH] Strengthen induction lemma for reflexive transitive closure.

---
 theories/ars.v | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/theories/ars.v b/theories/ars.v
index 5b15d13f..5baeb3f7 100644
--- a/theories/ars.v
+++ b/theories/ars.v
@@ -61,19 +61,22 @@ Section rtc.
 
   Lemma rtc_inv x z : rtc R x z → x = z ∨ ∃ y, R x y ∧ rtc R y z.
   Proof. inversion_clear 1; eauto. Qed.
-
-  Lemma rtc_ind_r (P : A → A → Prop)
-    (Prefl : ∀ x, P x x)
-    (Pstep : ∀ x y z, rtc R x y → R y z → P x y → P x z) :
+  Lemma rtc_ind_r_weak (P : A → A → Prop)
+    (Prefl : ∀ x, P x x) (Pstep : ∀ x y z, rtc R x y → R y z → P x y → P x z) :
     ∀ x z, rtc R x z → P x z.
   Proof.
     cut (∀ y z, rtc R y z → ∀ x, rtc R x y → P x y → P x z).
     { eauto using rtc_refl. }
     induction 1; eauto using rtc_r.
   Qed.
-
+  Lemma rtc_ind_r (P : A → Prop) (x : A)
+    (Prefl : P x) (Pstep : ∀ y z, rtc R x y → R y z → P y → P z) :
+    ∀ z, rtc R x z → P z.
+  Proof.
+    intros z p. revert x z p Prefl Pstep. refine (rtc_ind_r_weak _ _ _); eauto.
+  Qed.
   Lemma rtc_inv_r x z : rtc R x z → x = z ∨ ∃ y, rtc R x y ∧ R y z.
-  Proof. revert x z. apply rtc_ind_r; eauto. Qed.
+  Proof. revert z. apply rtc_ind_r; eauto. Qed.
 
   Lemma nsteps_once x y : R x y → nsteps R 1 x y.
   Proof. eauto with ars. Qed.
-- 
GitLab