From d19ceda8d503ef10d543260f255d59b8b0ab8779 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Thu, 17 Nov 2016 00:24:21 +0100
Subject: [PATCH] Prove that Fix_F is proper.
---
theories/relations.v | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/theories/relations.v b/theories/relations.v
index c7e4b1a..cb8ceee 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -221,3 +221,13 @@ nor by conversion tests in the kernel), but in some cases we do need it for
computation (that is, we cannot make it opaque). We use the [Strategy]
command to make its expanding behavior less eager. *)
Strategy 100 [wf_guard].
+
+Lemma Fix_F_proper `{R : relation A}
+ (B : A → Type)
+ (E : ∀ x, relation (B x)) {E_Equivalence : ∀ x, Equivalence (E x)}
+ (F : ∀ x, (∀ y, R y x → B y) → B x)
+ (HF : ∀ (x : A) (f g : ∀ y, R y x → B y),
+ (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
+ (x : A) (acc1 acc2 : Acc R x) :
+ E _ (Fix_F B F acc1) (Fix_F B F acc2).
+Proof. revert x acc1 acc2. fix 2. intros x [acc1] [acc2]; simpl; auto. Qed.
--
GitLab