From d9c89c8fa8955d40fa0732467a4488b7dccb5a38 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Mon, 8 Aug 2016 14:50:23 +0200 Subject: [PATCH] Better fix to avoid relying on the order in which simplify_eq works. --- algebra/cofe_solver.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v index 9c5c79f6..20a9ff0f 100644 --- a/algebra/cofe_solver.v +++ b/algebra/cofe_solver.v @@ -106,17 +106,17 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed. Lemma coerce_f {k j} (H : S k = S j) (x : A k) : coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x). Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed. -Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) : +Lemma gg_gg {k i i1 i2 j} : ∀ (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k), gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)). Proof. - assert (i = i2 + i1) by lia; move:H1=>H1; simplify_eq/=. revert j x H1. + intros ? -> x. assert (i = i2 + i1) as -> by lia. revert j x H1. induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=; [by rewrite coerce_id|by rewrite g_coerce IH]. Qed. -Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) : +Lemma ff_ff {k i i1 i2 j} : ∀ (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k), coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)). Proof. - assert (i = i1 + i2) by lia; move:H1=>H1; simplify_eq/=. + intros ? <- x. assert (i = i1 + i2) as -> by lia. induction i1 as [|i1 IH]; simplify_eq/=; [by rewrite coerce_id|by rewrite coerce_f IH]. Qed. -- GitLab