Commit 04b92602 authored by Johannes Kloos's avatar Johannes Kloos
Browse files

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.
parent 8389dcbf
......@@ -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)).
unfold Fix.
destruct (wfR x); cbn.
apply HF; intros.
apply Fix_F_proper; auto.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment