From fe82f3a470c6d30f10d1e7dbc535a263a55ebc13 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 22 Aug 2016 09:16:46 +0200
Subject: [PATCH] Simplify proof of fixpoint_unique.
---
algebra/cofe.v | 8 +++-----
1 file changed, 3 insertions(+), 5 deletions(-)
diff --git a/algebra/cofe.v b/algebra/cofe.v
index d2f120f50..da126ca99 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -198,11 +198,9 @@ Section fixpoint.
Lemma fixpoint_unique (x : A) : x ≡ f x → x ≡ fixpoint f.
Proof.
- rewrite !equiv_dist=> Hx n.
- rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //=.
- induction n as [|n IH]; simpl in *.
- - rewrite Hx; eauto using contractive_0.
- - rewrite Hx. apply (contractive_S _), IH.
+ rewrite !equiv_dist=> Hx n. induction n as [|n IH]; simpl in *.
+ - rewrite Hx fixpoint_unfold; eauto using contractive_0.
+ - rewrite Hx fixpoint_unfold. apply (contractive_S _), IH.
Qed.
Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
--
GitLab