From 082aed88f3a0cb01ead3aa1776bd35f6d0f72a5f Mon Sep 17 00:00:00 2001 From: Xingyu Xie Date: Fri, 24 Jul 2026 14:28:29 +0200 Subject: [PATCH] Core: new lemmas: comp_idfunL, comp_idfunR (registered as simplify hints) Left/right identity of function composition. Both are definitional (closed by conversion); their main value is the simplify-hint registration, which lets /= collapse identity compositions that arise when massaging dmap/expectation goals (e.g. E d idfun). Co-Authored-By: Claude Fable 5 --- theories/core/Core.ec | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/theories/core/Core.ec b/theories/core/Core.ec index 21e3cf54d..44f36ffbd 100644 --- a/theories/core/Core.ec +++ b/theories/core/Core.ec @@ -150,6 +150,14 @@ proof. by move=> fK gK x y; rewrite -{1}[y]gK; apply (can_eq f g). qed. lemma inj_idfun: injective (idfun<:'a>). proof. by []. qed. +lemma comp_idfunL ['a 'b] (f : 'a -> 'b) : idfun \o f = f. +proof. by []. qed. + +lemma comp_idfunR ['a 'b] (f : 'a -> 'b) : f \o idfun = f. +proof. by []. qed. + +hint simplify comp_idfunL, comp_idfunR. + lemma inj_can_sym (f:'a -> 'b) f': cancel f f' => injective f' => cancel f' f. proof. by move=> fK injf' x; apply injf'; rewrite fK. qed.