From fc2e3b003a30ab1ecd851fb2ba6b8dcc6e656278 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 13 Oct 2022 06:00:59 +0000 Subject: [PATCH] refactor(algebra/free_monoid): add `to_list`/`of_list` (#16926) * add `free_monoid.to_list` and `free_monoid.of_list`; * update API to explicitly use these functions; * fix `control.fold`. --- src/algebra/free_monoid/basic.lean | 128 ++++++++++++++++++++++------- src/control/fold.lean | 114 +++++++++++-------------- 2 files changed, 146 insertions(+), 96 deletions(-) diff --git a/src/algebra/free_monoid/basic.lean b/src/algebra/free_monoid/basic.lean index 53c3e796994ca..fe39381ef6667 100644 --- a/src/algebra/free_monoid/basic.lean +++ b/src/algebra/free_monoid/basic.lean @@ -25,47 +25,106 @@ def free_monoid (α) := list α namespace free_monoid +/-- The identity equivalence between `free_monoid α` and `list α`. -/ +@[to_additive "The identity equivalence between `free_add_monoid α` and `list α`."] +def to_list : free_monoid α ≃ list α := equiv.refl _ + +/-- The identity equivalence between `list α` and `free_monoid α`. -/ +@[to_additive "The identity equivalence between `list α` and `free_add_monoid α`."] +def of_list : list α ≃ free_monoid α := equiv.refl _ + +@[simp, to_additive] lemma to_list_symm : (@to_list α).symm = of_list := rfl +@[simp, to_additive] lemma of_list_symm : (@of_list α).symm = to_list := rfl +@[simp, to_additive] lemma to_list_of_list (l : list α) : to_list (of_list l) = l := rfl +@[simp, to_additive] lemma of_list_to_list (xs : free_monoid α) : of_list (to_list xs) = xs := rfl +@[simp, to_additive] lemma to_list_comp_of_list : @to_list α ∘ of_list = id := rfl +@[simp, to_additive] lemma of_list_comp_to_list : @of_list α ∘ to_list = id := rfl + @[to_additive] -instance : monoid (free_monoid α) := -{ one := [], - mul := λ x y, (x ++ y : list α), - mul_one := by intros; apply list.append_nil, - one_mul := by intros; refl, - mul_assoc := by intros; apply list.append_assoc } +instance : cancel_monoid (free_monoid α) := +{ one := of_list [], + mul := λ x y, of_list (x.to_list ++ y.to_list), + mul_one := list.append_nil, + one_mul := list.nil_append, + mul_assoc := list.append_assoc, + mul_left_cancel := λ _ _ _, list.append_left_cancel, + mul_right_cancel := λ _ _ _, list.append_right_cancel } @[to_additive] instance : inhabited (free_monoid α) := ⟨1⟩ -@[to_additive] -lemma one_def : (1 : free_monoid α) = [] := rfl +@[simp, to_additive] lemma to_list_one : (1 : free_monoid α).to_list = [] := rfl +@[simp, to_additive] lemma of_list_nil : of_list ([] : list α) = 1 := rfl -@[to_additive] -lemma mul_def (xs ys : list α) : (xs * ys : free_monoid α) = (xs ++ ys : list α) := +@[simp, to_additive] +lemma to_list_mul (xs ys : free_monoid α) : (xs * ys).to_list = xs.to_list ++ ys.to_list := rfl + +@[simp, to_additive] +lemma of_list_append (xs ys : list α) : + of_list (xs ++ ys) = of_list xs * of_list ys := rfl -@[to_additive] -lemma prod_eq_join (xs : list (free_monoid α)) : xs.prod = xs.join := -by induction xs; simp [*, mul_def, list.join, one_def] +@[simp, to_additive] +lemma to_list_prod (xs : list (free_monoid α)) : to_list xs.prod = (xs.map to_list).join := +by induction xs; simp [*, list.join] + +@[simp, to_additive] +lemma of_list_join (xs : list (list α)) : of_list xs.join = (xs.map of_list).prod := +to_list.injective $ by simp /-- Embeds an element of `α` into `free_monoid α` as a singleton list. -/ @[to_additive "Embeds an element of `α` into `free_add_monoid α` as a singleton list." ] -def of (x : α) : free_monoid α := [x] +def of (x : α) : free_monoid α := of_list [x] -@[to_additive] -lemma of_def (x : α) : of x = [x] := rfl +@[simp, to_additive] lemma to_list_of (x : α) : to_list (of x) = [x] := rfl +@[to_additive] lemma of_list_singleton (x : α) : of_list [x] = of x := rfl -@[to_additive] -lemma of_injective : function.injective (@of α) := -λ a b, list.head_eq_of_cons_eq +@[simp, to_additive] lemma of_list_cons (x : α) (xs : list α) : + of_list (x :: xs) = of x * of_list xs := +rfl + +@[to_additive] lemma to_list_of_mul (x : α) (xs : free_monoid α) : + to_list (of x * xs) = x :: xs.to_list := +rfl -@[to_additive] lemma of_mul_eq_cons (x : α) (l : free_monoid α) : of x * l = x :: l := rfl +@[to_additive] lemma of_injective : function.injective (@of α) := list.singleton_injective -/-- Recursor for `free_monoid` using `1` and `of x * xs` instead of `[]` and `x :: xs`. -/ +/-- Recursor for `free_monoid` using `1` and `free_monoid.of x * xs` instead of `[]` and +`x :: xs`. -/ @[elab_as_eliminator, to_additive - "Recursor for `free_add_monoid` using `0` and `of x + xs` instead of `[]` and `x :: xs`."] + "Recursor for `free_add_monoid` using `0` and `free_add_monoid.of x + xs` instead of `[]` and + `x :: xs`."] def rec_on {C : free_monoid α → Sort*} (xs : free_monoid α) (h0 : C 1) (ih : Π x xs, C xs → C (of x * xs)) : C xs := list.rec_on xs h0 ih +@[simp, to_additive] lemma rec_on_one {C : free_monoid α → Sort*} (h0 : C 1) + (ih : Π x xs, C xs → C (of x * xs)) : + @rec_on α C 1 h0 ih = h0 := +rfl + +@[simp, to_additive] lemma rec_on_of_mul {C : free_monoid α → Sort*} (x : α) (xs : free_monoid α) + (h0 : C 1) (ih : Π x xs, C xs → C (of x * xs)) : + @rec_on α C (of x * xs) h0 ih = ih x xs (rec_on xs h0 ih) := +rfl + +/-- A version of `list.cases_on` for `free_monoid` using `1` and `free_monoid.of x * xs` instead of +`[]` and `x :: xs`. -/ +@[elab_as_eliminator, to_additive + "A version of `list.cases_on` for `free_add_monoid` using `0` and `free_add_monoid.of x + xs` + instead of `[]` and `x :: xs`."] +def cases_on {C : free_monoid α → Sort*} (xs : free_monoid α) (h0 : C 1) + (ih : Π x xs, C (of x * xs)) : C xs := list.cases_on xs h0 ih + +@[simp, to_additive] lemma cases_on_one {C : free_monoid α → Sort*} (h0 : C 1) + (ih : Π x xs, C (of x * xs)) : + @cases_on α C 1 h0 ih = h0 := +rfl + +@[simp, to_additive] lemma cases_on_of_mul {C : free_monoid α → Sort*} (x : α) (xs : free_monoid α) + (h0 : C 1) (ih : Π x xs, C (of x * xs)) : + @cases_on α C (of x * xs) h0 ih = ih x xs := +rfl + @[ext, to_additive] lemma hom_eq ⦃f g : free_monoid α →* M⦄ (h : ∀ x, f (of x) = g (of x)) : f = g := @@ -76,8 +135,8 @@ monoid_hom.ext $ λ l, rec_on l (f.map_one.trans g.map_one.symm) $ @[to_additive "Equivalence between maps `α → A` and additive monoid homomorphisms `free_add_monoid α →+ A`."] def lift : (α → M) ≃ (free_monoid α →* M) := -{ to_fun := λ f, ⟨λ l, (l.map f).prod, rfl, - λ l₁ l₂, by simp only [mul_def, list.map_append, list.prod_append]⟩, +{ to_fun := λ f, ⟨λ l, (l.to_list.map f).prod, rfl, + λ l₁ l₂, by simp only [to_list_mul, list.map_append, list.prod_append]⟩, inv_fun := λ f x, f (of x), left_inv := λ f, funext $ λ x, one_mul (f x), right_inv := λ f, hom_eq $ λ x, one_mul (f (of x)) } @@ -86,10 +145,9 @@ def lift : (α → M) ≃ (free_monoid α →* M) := lemma lift_symm_apply (f : free_monoid α →* M) : lift.symm f = f ∘ of := rfl @[to_additive] -lemma lift_apply (f : α → M) (l : free_monoid α) : lift f l = (l.map f).prod := rfl +lemma lift_apply (f : α → M) (l : free_monoid α) : lift f l = (l.to_list.map f).prod := rfl -@[to_additive] -lemma lift_comp_of (f : α → M) : (lift f) ∘ of = f := lift.symm_apply_apply f +@[to_additive] lemma lift_comp_of (f : α → M) : lift f ∘ of = f := lift.symm_apply_apply f @[simp, to_additive] lemma lift_eval_of (f : α → M) (x : α) : lift f (of x) = f x := @@ -110,10 +168,14 @@ monoid_hom.ext_iff.1 (comp_lift g f) x /-- Define a multiplicative action of `free_monoid α` on `β`. -/ @[to_additive "Define an additive action of `free_add_monoid α` on `β`."] def mk_mul_action (f : α → β → β) : mul_action (free_monoid α) β := -{ smul := λ l b, list.foldr f b l, +{ smul := λ l b, l.to_list.foldr f b, one_smul := λ x, rfl, mul_smul := λ xs ys b, list.foldr_append _ _ _ _ } +@[to_additive] lemma smul_def (f : α → β → β) (l : free_monoid α) (b : β) : + (by haveI := mk_mul_action f; exact l • b = l.to_list.foldr f b) := +rfl + @[simp, to_additive] lemma of_smul (f : α → β → β) (x : α) (y : β) : (by haveI := mk_mul_action f; exact of x • y) = f x y := rfl @@ -123,12 +185,20 @@ each `of x` to `of (f x)`. -/ @[to_additive "The unique additive monoid homomorphism `free_add_monoid α →+ free_add_monoid β` that sends each `of x` to `of (f x)`."] def map (f : α → β) : free_monoid α →* free_monoid β := -{ to_fun := list.map f, +{ to_fun := λ l, of_list $ l.to_list.map f, map_one' := rfl, map_mul' := λ l₁ l₂, list.map_append _ _ _ } @[simp, to_additive] lemma map_of (f : α → β) (x : α) : map f (of x) = of (f x) := rfl +@[to_additive] lemma to_list_map (f : α → β) (xs : free_monoid α) : + (map f xs).to_list = xs.to_list.map f := +rfl + +@[to_additive] lemma of_list_map (f : α → β) (xs : list α) : + of_list (xs.map f) = map f (of_list xs) := +rfl + @[to_additive] lemma lift_of_comp_eq_map (f : α → β) : lift (λ x, of (f x)) = map f := diff --git a/src/control/fold.lean b/src/control/fold.lean index 2944d754f29cf..f00281fcffdeb 100644 --- a/src/control/fold.lean +++ b/src/control/fold.lean @@ -104,24 +104,18 @@ how the monoid of endofunctions define `foldl`. def foldl.mk (f : α → α) : foldl α := op f def foldl.get (x : foldl α) : α → α := unop x @[simps] def foldl.of_free_monoid (f : β → α → β) : free_monoid α →* monoid.foldl β := -{ to_fun := λ xs, op $ flip (list.foldl f) xs, +{ to_fun := λ xs, op $ flip (list.foldl f) xs.to_list, map_one' := rfl, - map_mul' := by intros; simp only [free_monoid.mul_def, flip, unop_op, + map_mul' := by intros; simp only [free_monoid.to_list_mul, flip, unop_op, list.foldl_append, op_inj]; refl } @[reducible] def foldr (α : Type u) : Type u := End α def foldr.mk (f : α → α) : foldr α := f def foldr.get (x : foldr α) : α → α := x @[simps] def foldr.of_free_monoid (f : α → β → β) : free_monoid α →* monoid.foldr β := -{ to_fun := λ xs, flip (list.foldr f) xs, +{ to_fun := λ xs, flip (list.foldr f) xs.to_list, map_one' := rfl, - map_mul' := - begin - intros, - simp only [free_monoid.mul_def, list.foldr_append, flip], - refl - end } - + map_mul' := λ xs ys, funext $ λ z, list.foldr_append _ _ _ _ } @[reducible] def mfoldl (m : Type u → Type u) [monad m] (α : Type u) : Type u := mul_opposite $ End $ Kleisli.mk m α @@ -129,7 +123,7 @@ def mfoldl.mk (f : α → m α) : mfoldl m α := op f def mfoldl.get (x : mfoldl m α) : α → m α := unop x @[simps] def mfoldl.of_free_monoid [is_lawful_monad m] (f : β → α → m β) : free_monoid α →* monoid.mfoldl m β := -{ to_fun := λ xs, op $ flip (list.mfoldl f) xs, +{ to_fun := λ xs, op $ flip (list.mfoldl f) xs.to_list, map_one' := rfl, map_mul' := by intros; apply unop_injective; ext; apply list.mfoldl_append } @@ -139,7 +133,7 @@ def mfoldr.mk (f : α → m α) : mfoldr m α := f def mfoldr.get (x : mfoldr m α) : α → m α := x @[simps] def mfoldr.of_free_monoid [is_lawful_monad m] (f : α → β → m β) : free_monoid α →* monoid.mfoldr m β := -{ to_fun := λ xs, flip (list.mfoldr f) xs, +{ to_fun := λ xs, flip (list.mfoldr f) xs.to_list, map_one' := rfl, map_mul' := by intros; ext; apply list.mfoldr_append } @@ -204,27 +198,18 @@ def map_fold [monoid α] [monoid β] (f : α →* β) : preserves_seq' := by { intros, simp only [f.map_mul, (<*>)], }, preserves_pure' := by { intros, simp only [f.map_one, pure] } } -def free.mk : α → free_monoid α := list.ret - -def free.map (f : α → β) : free_monoid α →* free_monoid β := -{ to_fun := list.map f, - map_mul' := λ x y, - by simp only [free_monoid.mul_def, list.map_append, free_add_monoid.add_def], - map_one' := by simp only [free_monoid.one_def, list.map, free_add_monoid.zero_def] } - lemma free.map_eq_map (f : α → β) (xs : list α) : - f <$> xs = free.map f xs := rfl + f <$> xs = (free_monoid.map f (free_monoid.of_list xs)).to_list := rfl lemma foldl.unop_of_free_monoid (f : β → α → β) (xs : free_monoid α) (a : β) : - unop (foldl.of_free_monoid f xs) a = list.foldl f a xs := rfl + unop (foldl.of_free_monoid f xs) a = list.foldl f a xs.to_list := rfl variables (m : Type u → Type u) [monad m] [is_lawful_monad m] variables {t : Type u → Type u} [traversable t] [is_lawful_traversable t] open is_lawful_traversable -lemma fold_map_hom - [monoid α] [monoid β] (f : α →* β) +lemma fold_map_hom [monoid α] [monoid β] (f : α →* β) (g : γ → α) (x : t γ) : f (fold_map g x) = fold_map (f ∘ g) x := calc f (fold_map g x) @@ -236,19 +221,9 @@ calc f (fold_map g x) lemma fold_map_hom_free [monoid β] (f : free_monoid α →* β) (x : t α) : - f (fold_map free.mk x) = fold_map (f ∘ free.mk) x := + f (fold_map free_monoid.of x) = fold_map (f ∘ free_monoid.of) x := fold_map_hom f _ x -variable {m} - -lemma fold_mfoldl_cons (f : α → β → m α) (x : β) (y : α) : - list.mfoldl f y (free.mk x) = f y x := -by simp only [free.mk, list.ret, list.mfoldl, bind_pure] - -lemma fold_mfoldr_cons (f : β → α → m α) (x : β) (y : α) : - list.mfoldr f y (free.mk x) = f x y := -by simp only [free.mk, list.ret, list.mfoldr, pure_bind] - end applicative_transformation section equalities @@ -257,37 +232,38 @@ variables {α β γ : Type u} variables {t : Type u → Type u} [traversable t] [is_lawful_traversable t] @[simp] -lemma foldl.of_free_monoid_comp_free_mk (f : α → β → α) : - foldl.of_free_monoid f ∘ free.mk = foldl.mk ∘ flip f := rfl +lemma foldl.of_free_monoid_comp_of (f : α → β → α) : + foldl.of_free_monoid f ∘ free_monoid.of = foldl.mk ∘ flip f := rfl @[simp] -lemma foldr.of_free_monoid_comp_free_mk (f : β → α → α) : - foldr.of_free_monoid f ∘ free.mk = foldr.mk ∘ f := rfl +lemma foldr.of_free_monoid_comp_of (f : β → α → α) : + foldr.of_free_monoid f ∘ free_monoid.of = foldr.mk ∘ f := rfl @[simp] -lemma mfoldl.of_free_monoid_comp_free_mk {m} [monad m] [is_lawful_monad m] (f : α → β → m α) : - mfoldl.of_free_monoid f ∘ free.mk = mfoldl.mk ∘ flip f := -by ext; simp [(∘), mfoldl.of_free_monoid, mfoldl.mk, flip, fold_mfoldl_cons]; refl +lemma mfoldl.of_free_monoid_comp_of {m} [monad m] [is_lawful_monad m] (f : α → β → m α) : + mfoldl.of_free_monoid f ∘ free_monoid.of = mfoldl.mk ∘ flip f := +by { ext1 x, simp [(∘), mfoldl.of_free_monoid, mfoldl.mk, flip], refl } @[simp] -lemma mfoldr.of_free_monoid_comp_free_mk {m} [monad m] [is_lawful_monad m] (f : β → α → m α) : - mfoldr.of_free_monoid f ∘ free.mk = mfoldr.mk ∘ f := -by { ext, simp [(∘), mfoldr.of_free_monoid, mfoldr.mk, flip, fold_mfoldr_cons] } +lemma mfoldr.of_free_monoid_comp_of {m} [monad m] [is_lawful_monad m] (f : β → α → m α) : + mfoldr.of_free_monoid f ∘ free_monoid.of = mfoldr.mk ∘ f := +by { ext, simp [(∘), mfoldr.of_free_monoid, mfoldr.mk, flip] } lemma to_list_spec (xs : t α) : - to_list xs = (fold_map free.mk xs : free_monoid _) := + to_list xs = free_monoid.to_list (fold_map free_monoid.of xs) := eq.symm $ -calc fold_map free.mk xs - = (fold_map free.mk xs).reverse.reverse : by simp only [list.reverse_reverse] -... = (list.foldr cons [] (fold_map free.mk xs).reverse).reverse +calc free_monoid.to_list (fold_map free_monoid.of xs) + = free_monoid.to_list (fold_map free_monoid.of xs).reverse.reverse + : by simp only [list.reverse_reverse] +... = free_monoid.to_list (list.foldr cons [] (fold_map free_monoid.of xs).reverse).reverse : by simp only [list.foldr_eta] -... = (unop (foldl.of_free_monoid (flip cons) (fold_map free.mk xs)) []).reverse - : by simp [flip,list.foldr_reverse,foldl.of_free_monoid, unop_op] +... = (unop (foldl.of_free_monoid (flip cons) (fold_map free_monoid.of xs)) []).reverse + : by simp [flip, list.foldr_reverse, foldl.of_free_monoid, unop_op] ... = to_list xs : begin rw fold_map_hom_free (foldl.of_free_monoid (flip $ @cons α)), - simp only [to_list, foldl, list.reverse_inj, foldl.get, - foldl.of_free_monoid_comp_free_mk], - all_goals { apply_instance } + { simp only [to_list, foldl, list.reverse_inj, foldl.get, + foldl.of_free_monoid_comp_of] }, + { apply_instance } end lemma fold_map_map [monoid γ] (f : α → β) (g : β → γ) (xs : t α) : @@ -297,23 +273,27 @@ by simp only [fold_map,traverse_map] lemma foldl_to_list (f : α → β → α) (xs : t β) (x : α) : foldl f x xs = list.foldl f x (to_list xs) := begin - rw ← foldl.unop_of_free_monoid, + rw [← free_monoid.to_list_of_list (to_list xs), ← foldl.unop_of_free_monoid], simp only [foldl, to_list_spec, fold_map_hom_free, - foldl.of_free_monoid_comp_free_mk, foldl.get] + foldl.of_free_monoid_comp_of, foldl.get, free_monoid.of_list_to_list] end lemma foldr_to_list (f : α → β → β) (xs : t α) (x : β) : foldr f x xs = list.foldr f x (to_list xs) := begin - change _ = foldr.of_free_monoid _ _ _, - simp only [foldr, to_list_spec, fold_map_hom_free, - foldr.of_free_monoid_comp_free_mk, foldr.get] + change _ = foldr.of_free_monoid _ (free_monoid.of_list $ to_list xs) _, + rw [to_list_spec, foldr, foldr.get, free_monoid.of_list_to_list, fold_map_hom_free, + foldr.of_free_monoid_comp_of] end +/- + +-/ + lemma to_list_map (f : α → β) (xs : t α) : - to_list (f <$> xs) = f <$> to_list xs := by -{ simp only [to_list_spec,free.map_eq_map,fold_map_hom (free.map f), fold_map_map]; - refl } + to_list (f <$> xs) = f <$> to_list xs := +by simp only [to_list_spec, free.map_eq_map, fold_map_hom, fold_map_map, + free_monoid.of_list_to_list, free_monoid.map_of, (∘)] @[simp] theorem foldl_map (g : β → γ) (f : α → γ → α) (a : α) (l : t β) : foldl f a (g <$> l) = foldl (λ x y, f x (g y)) a l := @@ -328,7 +308,7 @@ begin simp only [to_list_spec, fold_map, traverse], induction xs, case list.nil { refl }, - case list.cons : _ _ ih { unfold list.traverse list.ret, rw ih, refl } + case list.cons : _ _ ih { conv_rhs { rw [← ih] }, refl } end theorem length_to_list {xs : t α} : length xs = list.length (to_list xs) := @@ -353,17 +333,17 @@ variables {m : Type u → Type u} [monad m] [is_lawful_monad m] lemma mfoldl_to_list {f : α → β → m α} {x : α} {xs : t β} : mfoldl f x xs = list.mfoldl f x (to_list xs) := -calc mfoldl f x xs = unop (mfoldl.of_free_monoid f (to_list xs)) x : +calc mfoldl f x xs = unop (mfoldl.of_free_monoid f (free_monoid.of_list $ to_list xs)) x : by simp only [mfoldl, to_list_spec, fold_map_hom_free (mfoldl.of_free_monoid f), - mfoldl.of_free_monoid_comp_free_mk, mfoldl.get] + mfoldl.of_free_monoid_comp_of, mfoldl.get, free_monoid.of_list_to_list] ... = list.mfoldl f x (to_list xs) : by simp [mfoldl.of_free_monoid, unop_op, flip] lemma mfoldr_to_list (f : α → β → m β) (x : β) (xs : t α) : mfoldr f x xs = list.mfoldr f x (to_list xs) := begin - change _ = mfoldr.of_free_monoid f (to_list xs) x, + change _ = mfoldr.of_free_monoid f (free_monoid.of_list $ to_list xs) x, simp only [mfoldr, to_list_spec, fold_map_hom_free (mfoldr.of_free_monoid f), - mfoldr.of_free_monoid_comp_free_mk, mfoldr.get] + mfoldr.of_free_monoid_comp_of, mfoldr.get, free_monoid.of_list_to_list] end @[simp] theorem mfoldl_map (g : β → γ) (f : α → γ → m α) (a : α) (l : t β) :