From 04b92602fbe8d31daffc0d9dd512feabae4f4c1c Mon Sep 17 00:00:00 2001 From: Johannes Kloos Date: Tue, 31 Oct 2017 11:36:52 +0100 Subject: [PATCH] Unfolding lemma for Fix in setoids. This generalizes Fix_unfold to a setoid setting. In particular, we can use this to unfold multi-argument fixpoints without requiring functional extensionality. --- theories/relations.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/theories/relations.v b/theories/relations.v index a17f51c..a1e59d2 100644 --- a/theories/relations.v +++ b/theories/relations.v @@ -235,3 +235,16 @@ Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x) (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. + +Lemma Fix_unfold_rel `{R: relation A} (wfR: wf R) (B: A → Type) (E: ∀ x, relation (B 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): + E _ (Fix wfR B F x) (F x (λ y _, Fix wfR B F y)). +Proof. + unfold Fix. + destruct (wfR x); cbn. + apply HF; intros. + apply Fix_F_proper; auto. +Qed. -- GitLab