From 1f6c3bcfc4bc78226a690b571f64b9e38aab1472 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 19:43:58 -0400 Subject: [PATCH 1/9] fix defeq abuse --- Mathlib/Control/Functor.lean | 8 + Mathlib/Data/PFunctor/Univariate/Basic.lean | 98 +++++++----- Mathlib/Data/PFunctor/Univariate/M.lean | 110 ++++++------- Mathlib/Data/QPF/Univariate/Basic.lean | 168 ++++++++------------ 4 files changed, 177 insertions(+), 207 deletions(-) diff --git a/Mathlib/Control/Functor.lean b/Mathlib/Control/Functor.lean index 59d944a66186ec..53d67f44c18784 100644 --- a/Mathlib/Control/Functor.lean +++ b/Mathlib/Control/Functor.lean @@ -143,6 +143,14 @@ def Comp.mk {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : F def Comp.run {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : Comp F G α) : F (G α) := x +@[simp] +theorem Comp.run_MK {F : Type u → Type w} {G : Type v → Type u} {α : Type v} + (x : F (G α)) : (mk x).run = x := rfl + +@[simp] +theorem Comp.mk_run {F : Type u → Type w} {G : Type v → Type u} {α : Type v} + (x : Comp F G α) : mk (x.run) = x := rfl + namespace Comp variable {F : Type u → Type w} {G : Type v → Type u} diff --git a/Mathlib/Data/PFunctor/Univariate/Basic.lean b/Mathlib/Data/PFunctor/Univariate/Basic.lean index 49ff69976cc078..d99a4dabdc4542 100644 --- a/Mathlib/Data/PFunctor/Univariate/Basic.lean +++ b/Mathlib/Data/PFunctor/Univariate/Basic.lean @@ -43,16 +43,41 @@ instance : Inhabited PFunctor := variable (P : PFunctor.{uA, uB}) {α : Type v₁} {β : Type v₂} {γ : Type v₃} /-- Applying `P` to an object of `Type` -/ -@[coe] +@[coe, implicit_reducible] def Obj (α : Type v) : Type (max v uA uB) := Σ x : P.A, P.B x → α instance : CoeFun PFunctor.{uA, uB} (fun _ => Type v → Type (max v uA uB)) where coe := Obj +section Obj + +variable {P} + +@[implicit_reducible, match_pattern] +def Obj.mk (a : P.A) (f : P.B a → α) : P α := ⟨a, f⟩ + +@[implicit_reducible, elab_as_elim, induction_eliminator, cases_eliminator, match_pattern] +def Obj.rec {motive : P α → Sort*} (mk : ∀ a f, motive (.mk a f)) : ∀ t, motive t := + fun t => mk t.1 t.2 + +@[simp] +theorem Obj.rec_mk {motive : P α → Sort*} + {mk : ∀ a b, motive (.mk a b)} (a : P.A) (b : P.B a → α) : + Obj.rec mk (.mk a b) = mk a b := rfl + +@[implicit_reducible] def Obj.fst (x : P α) : P.A := x.1 +@[implicit_reducible] def Obj.snd (x : P α) : P.B x.fst → α := x.2 + +@[simp] theorem Obj.fst_mk (a : P.A) (f : P.B a → α) : Obj.fst (.mk a f) = a := rfl +@[simp] theorem Obj.snd_mk (a : P.A) (f : P.B a → α) : Obj.snd (.mk a f) = f := rfl + +@[simp] theorem Obj.eta (x : P α) : .mk x.fst x.snd = x := rfl + +end Obj + /-- Applying `P` to a morphism of `Type` -/ -def map (f : α → β) : P α → P β := - fun ⟨a, g⟩ => ⟨a, f ∘ g⟩ +def map (f : α → β) : P α → P β := fun x => .mk x.fst (f ∘ x.snd) instance Obj.inhabited [Inhabited P.A] [Inhabited α] : Inhabited (P α) := ⟨⟨default, default⟩⟩ @@ -66,15 +91,15 @@ theorem map_eq_map {α β : Type v} (f : α → β) (x : P α) : f <$> x = P.map @[simp] protected theorem map_eq (f : α → β) (a : P.A) (g : P.B a → α) : - P.map f ⟨a, g⟩ = ⟨a, f ∘ g⟩ := + P.map f (.mk a g) = .mk a (f ∘ g) := rfl @[simp] -protected theorem id_map : ∀ x : P α, P.map id x = x := fun ⟨_, _⟩ => rfl +protected theorem id_map (x : P α) : P.map id x = x := rfl @[simp] -protected theorem map_map (f : α → β) (g : β → γ) : - ∀ x : P α, P.map g (P.map f x) = P.map (g ∘ f) x := fun ⟨_, _⟩ => rfl +protected theorem map_map (f : α → β) (g : β → γ) (x : P α) : + P.map g (P.map f x) = P.map (g ∘ f) x := rfl instance : LawfulFunctor (Obj.{v} P) where map_const := rfl @@ -147,19 +172,21 @@ Composition of polynomial functors. namespace PFunctor /-- Composition for polynomial functors -/ +@[implicit_reducible] def comp (P₂ : PFunctor.{uA₂, uB₂}) (P₁ : PFunctor.{uA₁, uB₁}) : - PFunctor.{max uA₁ uA₂ uB₂, max uB₁ uB₂} := - ⟨Σ a₂ : P₂.1, P₂.2 a₂ → P₁.1, fun a₂a₁ => Σ u : P₂.2 a₂a₁.1, P₁.2 (a₂a₁.2 u)⟩ + PFunctor.{max uA₁ uA₂ uB₂, max uB₁ uB₂} where + A := Σ a₂ : P₂.A, P₂.B a₂ → P₁.A + B a₂a₁ := Σ u : P₂.B a₂a₁.1, P₁.B (a₂a₁.2 u) /-- Constructor for composition -/ def comp.mk (P₂ : PFunctor.{uA₂, uB₂}) (P₁ : PFunctor.{uA₁, uB₁}) {α : Type v} (x : P₂ (P₁ α)) : comp P₂ P₁ α := - ⟨⟨x.1, Sigma.fst ∘ x.2⟩, fun a₂a₁ => (x.2 a₂a₁.1).2 a₂a₁.2⟩ + .mk ⟨x.fst, Obj.fst ∘ x.snd⟩ fun a₂a₁ => (x.snd a₂a₁.1).snd a₂a₁.2 /-- Destructor for composition -/ def comp.get (P₂ : PFunctor.{uA₂, uB₂}) (P₁ : PFunctor.{uA₁, uB₁}) {α : Type v} (x : comp P₂ P₁ α) : P₂ (P₁ α) := - ⟨x.1.1, fun a₂ => ⟨x.1.2 a₂, fun a₁ => x.2 ⟨a₂, a₁⟩⟩⟩ + .mk x.fst.1 fun a₂ => .mk (x.fst.2 a₂) fun a₁ => x.snd ⟨a₂, a₁⟩ end PFunctor @@ -172,53 +199,36 @@ variable {P : PFunctor.{uA, uB}} open Functor -set_option backward.isDefEq.respectTransparency false in theorem liftp_iff {α : Type u} (p : α → Prop) (x : P α) : - Liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ i, p (f i) := by + Liftp p x ↔ ∃ a f, x = .mk a f ∧ ∀ i, p (f i) := by constructor - · rintro ⟨y, hy⟩ - rcases h : y with ⟨a, f⟩ - refine ⟨a, fun i => (f i).val, ?_, fun i => (f i).property⟩ - rw [← hy, h, map_eq_map, PFunctor.map_eq] - congr - rintro ⟨a, f, xeq, pf⟩ - use ⟨a, fun i => ⟨f i, pf i⟩⟩ - rw [xeq]; rfl - -set_option backward.isDefEq.respectTransparency false in + · rintro ⟨y, rfl⟩ + cases y with | mk a f + refine ⟨a, fun i => (f i).val, rfl, fun i => (f i).property⟩ + · rintro ⟨a, f, rfl, pf⟩ + exact ⟨.mk a fun i => ⟨f i, pf i⟩, rfl⟩ + theorem liftp_iff' {α : Type u} (p : α → Prop) (a : P.A) (f : P.B a → α) : - @Liftp.{u} P.Obj _ α p ⟨a, f⟩ ↔ ∀ i, p (f i) := by + Liftp p (.mk a f : P α) ↔ ∀ i, p (f i) := by simp only [liftp_iff]; constructor <;> intro h · rcases h with ⟨a', f', heq, h'⟩ cases heq assumption - repeat' first | constructor | assumption + · repeat' first | constructor | assumption theorem liftr_iff {α : Type u} (r : α → α → Prop) (x y : P α) : - Liftr r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ i, r (f₀ i) (f₁ i) := by - constructor - · rintro ⟨u, xeq, yeq⟩ - rcases h : u with ⟨a, f⟩ - use a, fun i => (f i).val.fst, fun i => (f i).val.snd - constructor - · rw [← xeq, h] - rfl - constructor - · rw [← yeq, h] - rfl - intro i - exact (f i).property - rintro ⟨a, f₀, f₁, xeq, yeq, h⟩ - use ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩ + Liftr r x y ↔ ∃ a f₀ f₁, x = .mk a f₀ ∧ y = .mk a f₁ ∧ ∀ i, r (f₀ i) (f₁ i) := by constructor - · rw [xeq] - rfl - rw [yeq]; rfl + · rintro ⟨u, rfl, rfl⟩ + cases u with | mk a f + exact ⟨a, fun i => (f i).1.1, fun i => (f i).1.2, rfl, rfl, fun i => (f i).2⟩ + · rintro ⟨a, f₀, f₁, rfl, rfl, h⟩ + exact ⟨.mk a fun i => ⟨(f₀ i, f₁ i), h i⟩, rfl, rfl⟩ open Set theorem supp_eq {α : Type u} (a : P.A) (f : P.B a → α) : - @supp.{u} P.Obj _ α (⟨a, f⟩ : P α) = f '' univ := by + supp (.mk a f : P α) = f '' univ := by ext x; simp only [supp, image_univ, mem_range, mem_ofPred_eq] constructor <;> intro h · apply @h fun x => ∃ y : P.B a, f y = x diff --git a/Mathlib/Data/PFunctor/Univariate/M.lean b/Mathlib/Data/PFunctor/Univariate/M.lean index 8b561a6ff6cefc..bb377a4a21b52c 100644 --- a/Mathlib/Data/PFunctor/Univariate/M.lean +++ b/Mathlib/Data/PFunctor/Univariate/M.lean @@ -213,22 +213,21 @@ theorem truncate_approx (x : M F) (n : ℕ) : truncate (x.approx <| n + 1) = x.a truncate_eq_of_agree _ _ (x.consistent _) /-- unfold an M-type -/ -def dest : M F → F (M F) - | x => ⟨head x, fun i => children x i⟩ +def dest : M F → F (M F) := fun x => .mk (head x) fun i => children x i namespace Approx /-- generates the approximations needed for `M.mk` -/ protected def sMk (x : F (M F)) : ∀ n, CofixA F n | 0 => CofixA.continue - | succ n => CofixA.intro x.1 fun i => (x.2 i).approx n + | succ n => CofixA.intro x.fst fun i => (x.snd i).approx n protected theorem P_mk (x : F (M F)) : AllAgree (Approx.sMk x) | 0 => by constructor | succ n => by constructor - introv - apply (x.2 i).consistent + intro i + apply (x.snd i).consistent end Approx @@ -242,37 +241,28 @@ are the same up to depth `n` -/ inductive Agree' : ℕ → M F → M F → Prop | trivial (x y : M F) : Agree' 0 x y | step {n : ℕ} {a} (x y : F.B a → M F) {x' y'} : - x' = M.mk ⟨a, x⟩ → y' = M.mk ⟨a, y⟩ → (∀ i, Agree' n (x i) (y i)) → Agree' (succ n) x' y' + x' = M.mk (.mk a x) → y' = M.mk (.mk a y) → + (∀ i, Agree' n (x i) (y i)) → Agree' (succ n) x' y' @[simp] theorem dest_mk (x : F (M F)) : dest (M.mk x) = x := rfl -set_option backward.isDefEq.respectTransparency false in @[simp] theorem mk_dest (x : M F) : M.mk (dest x) = x := by apply ext' intro n dsimp only [M.mk] - induction n with - | zero => apply @Subsingleton.elim _ CofixA.instSubsingleton - | succ n => ?_ - dsimp only [Approx.sMk, dest, head] - rcases h : x.approx (succ n) with - | ⟨hd, ch⟩ - have h' : hd = head' (x.approx 1) := by - rw [← head_succ' n, h, head'] - apply x.consistent - revert ch - rw [h'] - intro ch h - congr - ext a - dsimp only [children] - generalize hh : cast _ a = a'' - rw [cast_eq_iff_heq] at hh - revert a'' - rw [h] - intro _ hh - cases hh + induction n with | zero => apply @Subsingleton.elim _ CofixA.instSubsingleton | succ n ih + unfold Approx.sMk dest head + dsimp only [Obj.fst_mk, Obj.snd_mk] + cases h : x.approx (n + 1) with | intro hd ch + obtain rfl : hd = head' (x.approx 1) := by + rw [← head_succ' n 0 x.approx x.consistent, h] + rfl + refine congrArg (CofixA.intro (head' (x.approx 1))) (funext fun a => ?_) + unfold children + dsimp only + rw! [h] rfl theorem mk_inj {x y : F (M F)} (h : M.mk x = M.mk y) : x = y := by rw [← dest_mk x, h, dest_mk] @@ -290,11 +280,11 @@ protected def casesOn {r : M F → Sort w} (x : M F) (f : ∀ x : F (M F), r (M. /-- destructor for M-types, similar to `casesOn` but also gives access directly to the root and subtrees on an M-type -/ -protected def casesOn' {r : M F → Sort w} (x : M F) (f : ∀ a f, r (M.mk ⟨a, f⟩)) : r x := - M.casesOn x (fun ⟨a, g⟩ => f a g) +protected def casesOn' {r : M F → Sort w} (x : M F) (f : ∀ a f, r (M.mk (.mk a f))) : r x := + M.casesOn x (fun x => f x.fst x.snd) theorem approx_mk (a : F.A) (f : F.B a → M F) (i : ℕ) : - (M.mk ⟨a, f⟩).approx (succ i) = CofixA.intro a fun j => (f j).approx i := + (M.mk (.mk a f)).approx (succ i) = CofixA.intro a fun j => (f j).approx i := rfl @[simp] @@ -344,26 +334,25 @@ theorem casesOn_mk {r : M F → Sort*} (x : F (M F)) (f : ∀ x : F (M F), r (M. @[simp] theorem casesOn_mk' {r : M F → Sort*} {a} (x : F.B a → M F) - (f : ∀ (a) (f : F.B a → M F), r (M.mk ⟨a, f⟩)) : - PFunctor.M.casesOn' (M.mk ⟨a, x⟩) f = f a x := - @cases_mk F r ⟨a, x⟩ (fun ⟨a, g⟩ => f a g) + (f : ∀ (a) (f : F.B a → M F), r (M.mk (.mk a f))) : + PFunctor.M.casesOn' (M.mk (.mk a x)) f = f a x := rfl /-- `IsPath p x` tells us if `p` is a valid path through `x` -/ inductive IsPath : Path F → M F → Prop | nil (x : M F) : IsPath [] x | cons (xs : Path F) {a} (x : M F) (f : F.B a → M F) (i : F.B a) : - x = M.mk ⟨a, f⟩ → IsPath xs (f i) → IsPath (⟨a, i⟩ :: xs) x + x = M.mk (.mk a f) → IsPath xs (f i) → IsPath (⟨a, i⟩ :: xs) x theorem isPath_cons {xs : Path F} {a a'} {f : F.B a → M F} {i : F.B a'} : - IsPath (⟨a', i⟩ :: xs) (M.mk ⟨a, f⟩) → a = a' := by - generalize h : M.mk ⟨a, f⟩ = x + IsPath (⟨a', i⟩ :: xs) (M.mk (.mk a f)) → a = a' := by + generalize h : M.mk (.mk a f) = x rintro (_ | ⟨_, _, _, _, rfl, _⟩) cases mk_inj h rfl theorem isPath_cons' {xs : Path F} {a} {f : F.B a → M F} {i : F.B a} : - IsPath (⟨a, i⟩ :: xs) (M.mk ⟨a, f⟩) → IsPath xs (f i) := by - generalize h : M.mk ⟨a, f⟩ = x + IsPath (⟨a, i⟩ :: xs) (M.mk (.mk a f)) → IsPath xs (f i) := by + generalize h : M.mk (.mk a f) = x rintro (_ | ⟨_, _, _, _, rfl, hp⟩) cases mk_inj h exact hp @@ -407,15 +396,14 @@ theorem iselect_eq_default [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) (x · simp [*] @[simp] -theorem head_mk (x : F (M F)) : head (M.mk x) = x.1 := +theorem head_mk (x : F (M F)) : head (M.mk x) = x.fst := Eq.symm <| calc x.1 = (dest (M.mk x)).1 := by rw [dest_mk] _ = head (M.mk x) := rfl -set_option backward.isDefEq.respectTransparency false in -theorem children_mk {a} (x : F.B a → M F) (i : F.B (head (M.mk ⟨a, x⟩))) : - children (M.mk ⟨a, x⟩) i = x (cast (by rw [head_mk]) i) := by apply ext'; intro n; rfl +theorem children_mk {a} (x : F.B a → M F) (i : F.B (head (M.mk (.mk a x)))) : + children (M.mk (.mk a x)) i = x (cast (by simp) i) := by apply ext'; intro n; rfl @[simp] theorem ichildren_mk [DecidableEq F.A] [Inhabited (M F)] (x : F (M F)) (i : F.Idx) : @@ -425,16 +413,17 @@ theorem ichildren_mk [DecidableEq F.A] [Inhabited (M F)] (x : F (M F)) (i : F.Id @[simp] theorem isubtree_cons [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) {a} (f : F.B a → M F) - {i : F.B a} : isubtree (⟨_, i⟩ :: ps) (M.mk ⟨a, f⟩) = isubtree ps (f i) := by + {i : F.B a} : isubtree (⟨_, i⟩ :: ps) (M.mk (.mk a f)) = isubtree ps (f i) := by simp only [isubtree, dite_eq_left, isubtree, M.casesOn_mk']; rfl @[simp] theorem iselect_nil [DecidableEq F.A] [Inhabited (M F)] {a} (f : F.B a → M F) : - iselect nil (M.mk ⟨a, f⟩) = a := rfl + iselect nil (M.mk (.mk a f)) = a := rfl @[simp] theorem iselect_cons [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) {a} (f : F.B a → M F) {i} : - iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect ps (f i) := by simp only [iselect, isubtree_cons] + iselect (⟨a, i⟩ :: ps) (M.mk (.mk a f)) = iselect ps (f i) := by + simp only [iselect, isubtree_cons] theorem corec_def {X} (f : X → F X) (x₀ : X) : M.corec f x₀ = M.mk (F.map (M.corec f) (f x₀)) := by dsimp only [M.corec, M.mk] @@ -508,9 +497,9 @@ local infixl:50 " ~ " => R infinite tree-like structures -/ structure IsBisimulation : Prop where /-- The head of the trees are equal -/ - head : ∀ {a a'} {f f'}, M.mk ⟨a, f⟩ ~ M.mk ⟨a', f'⟩ → a = a' + head : ∀ {a a'} {f f'}, M.mk (.mk a f) ~ M.mk (.mk a' f') → a = a' /-- The tails are equal -/ - tail : ∀ {a} {f f' : F.B a → M F}, M.mk ⟨a, f⟩ ~ M.mk ⟨a, f'⟩ → ∀ i : F.B a, f i ~ f' i + tail : ∀ {a} {f f' : F.B a → M F}, M.mk (.mk a f) ~ M.mk (.mk a f') → ∀ i : F.B a, f i ~ f' i set_option backward.isDefEq.respectTransparency false in theorem nth_of_bisim [Inhabited (M F)] [DecidableEq F.A] @@ -519,8 +508,8 @@ theorem nth_of_bisim [Inhabited (M F)] [DecidableEq F.A] IsPath ps s₁ ∨ IsPath ps s₂ → iselect ps s₁ = iselect ps s₂ ∧ ∃ (a : _) (f f' : F.B a → M F), - isubtree ps s₁ = M.mk ⟨a, f⟩ ∧ - isubtree ps s₂ = M.mk ⟨a, f'⟩ ∧ ∀ i : F.B a, f i ~ f' i := by + isubtree ps s₁ = M.mk (.mk a f) ∧ + isubtree ps s₂ = M.mk (.mk a f') ∧ ∀ i : F.B a, f i ~ f' i := by intro h₀ hh induction s₁ using PFunctor.M.casesOn' with | _ a f induction s₂ using PFunctor.M.casesOn' with | _ a' f' @@ -570,15 +559,16 @@ theorem dest_corec (g : α → P α) (x : α) : M.dest (M.corec g x) = P.map (M. set_option backward.isDefEq.respectTransparency false in theorem bisim (R : M P → M P → Prop) - (h : ∀ x y, R x y → ∃ a f f', M.dest x = ⟨a, f⟩ ∧ M.dest y = ⟨a, f'⟩ ∧ ∀ i, R (f i) (f' i)) : + (h : ∀ x y, R x y → ∃ a f f', + M.dest x = (.mk a f) ∧ M.dest y = (.mk a f') ∧ ∀ i, R (f i) (f' i)) : ∀ x y, R x y → x = y := by introv h' have := Inhabited.mk x.head apply eq_of_bisim R _ _ _ h'; clear h' x y constructor <;> introv ih <;> rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩ <;> clear h - · replace h₀ := congr_arg Sigma.fst h₀ - replace h₁ := congr_arg Sigma.fst h₁ - simp only [dest_mk] at h₀ h₁ + · replace h₀ := congr_arg Obj.fst h₀ + replace h₁ := congr_arg Obj.fst h₁ + simp only [dest_mk, Obj.fst_mk] at h₀ h₁ rw [h₀, h₁] · simp only [dest_mk] at h₀ h₁ cases h₀ @@ -587,8 +577,8 @@ theorem bisim (R : M P → M P → Prop) theorem bisim' {α : Type*} (Q : α → Prop) (u v : α → M P) (h : ∀ x, Q x → ∃ a f f', - M.dest (u x) = ⟨a, f⟩ - ∧ M.dest (v x) = ⟨a, f'⟩ + M.dest (u x) = (.mk a f) + ∧ M.dest (v x) = (.mk a f') ∧ ∀ i, ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x') : ∀ x, Q x → u x = v x := fun x Qx => let R := fun w z : M P => ∃ x', Q x' ∧ w = u x' ∧ z = v x' @@ -600,7 +590,8 @@ theorem bisim' {α : Type*} (Q : α → Prop) (u v : α → M P) -- for the record, show M_bisim follows from _bisim' theorem bisim_equiv (R : M P → M P → Prop) - (h : ∀ x y, R x y → ∃ a f f', M.dest x = ⟨a, f⟩ ∧ M.dest y = ⟨a, f'⟩ ∧ ∀ i, R (f i) (f' i)) : + (h : ∀ x y, R x y → ∃ a f f', + M.dest x = (.mk a f) ∧ M.dest y = (.mk a f') ∧ ∀ i, R (f i) (f' i)) : ∀ x y, R x y → x = y := fun x y Rxy => let Q : M P × M P → Prop := fun p => R p.fst p.snd bisim' Q Prod.fst Prod.snd @@ -615,9 +606,10 @@ theorem corec_unique (g : α → P α) (f : α → M P) (hyp : ∀ x, M.dest (f apply bisim' (fun _ => True) _ _ _ _ trivial clear x intro x _ - rcases gxeq : g x with ⟨a, f'⟩ - have h₀ : M.dest (f x) = ⟨a, f ∘ f'⟩ := by rw [hyp, gxeq, PFunctor.map_eq] - have h₁ : M.dest (M.corec g x) = ⟨a, M.corec g ∘ f'⟩ := by rw [dest_corec, gxeq, PFunctor.map_eq] + cases gxeq : g x with | mk a f' + have h₀ : M.dest (f x) = .mk a (f ∘ f') := by rw [hyp, gxeq, PFunctor.map_eq] + have h₁ : M.dest (M.corec g x) = .mk a (M.corec g ∘ f') := by + rw [dest_corec, gxeq, PFunctor.map_eq] refine ⟨_, _, _, h₀, h₁, ?_⟩ intro i exact ⟨f' i, trivial, rfl, rfl⟩ diff --git a/Mathlib/Data/QPF/Univariate/Basic.lean b/Mathlib/Data/QPF/Univariate/Basic.lean index f5dfdfdb724c04..ab032dd73e2753 100644 --- a/Mathlib/Data/QPF/Univariate/Basic.lean +++ b/Mathlib/Data/QPF/Univariate/Basic.lean @@ -96,60 +96,47 @@ section open Functor -set_option backward.isDefEq.respectTransparency false in theorem liftp_iff {α : Type u} (p : α → Prop) (x : F α) : - Liftp p x ↔ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ i, p (f i) := by + Liftp p x ↔ ∃ a f, x = abs (.mk a f) ∧ ∀ i, p (f i) := by constructor · rintro ⟨y, hy⟩ - rcases h : repr y with ⟨a, f⟩ - use a, fun i => (f i).val - constructor - · rw [← hy, ← abs_repr y, h, ← abs_map] - rfl - intro i - apply (f i).property - rintro ⟨a, f, h₀, h₁⟩ - use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩ - rw [← abs_map, h₀]; rfl + cases h : repr y with | mk a f + refine ⟨a, fun i => (f i).val, ?_, fun i => (f i).property⟩ + rw [← hy, ← abs_repr y, h, ← abs_map] + rfl + · rintro ⟨a, f, h₀, h₁⟩ + refine ⟨abs (.mk a fun i => ⟨f i, h₁ i⟩), ?_⟩ + rw [← abs_map, h₀] + rfl +-- TODO: fix defeq abuse with `Sigma.snd` set_option backward.isDefEq.respectTransparency false in theorem liftp_iff' {α : Type u} (p : α → Prop) (x : F α) : Liftp p x ↔ ∃ u : q.P α, abs u = x ∧ ∀ i, p (u.snd i) := by + rw [liftp_iff] constructor - · rintro ⟨y, hy⟩ - rcases h : repr y with ⟨a, f⟩ - use ⟨a, fun i => (f i).val⟩ - dsimp - constructor - · rw [← hy, ← abs_repr y, h, ← abs_map] - rfl - intro i - apply (f i).property - rintro ⟨⟨a, f⟩, h₀, h₁⟩; dsimp at * - use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩ - rw [← abs_map, ← h₀]; rfl + · intro ⟨a, f, hx, hf⟩ + exact ⟨.mk a f, hx.symm, hf⟩ + · intro ⟨u, hx, hf⟩ + cases u with | mk a f + exact ⟨a, f, hx.symm, hf⟩ -set_option backward.isDefEq.respectTransparency false in theorem liftr_iff {α : Type u} (r : α → α → Prop) (x y : F α) : - Liftr r x y ↔ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ i, r (f₀ i) (f₁ i) := by + Liftr r x y ↔ ∃ a f₀ f₁, x = abs (.mk a f₀) ∧ y = abs (.mk a f₁) ∧ ∀ i, r (f₀ i) (f₁ i) := by constructor - · rintro ⟨u, xeq, yeq⟩ - rcases h : repr u with ⟨a, f⟩ - use a, fun i => (f i).val.fst, fun i => (f i).val.snd - constructor - · rw [← xeq, ← abs_repr u, h, ← abs_map] + · rintro ⟨u, rfl, rfl⟩ + cases h : repr u with | mk a f + refine ⟨a, fun i => (f i).1.1, fun i => (f i).1.2, ?_, ?_, fun i => (f i).2⟩ + · rw [← abs_repr u, h, ← abs_map] rfl - constructor - · rw [← yeq, ← abs_repr u, h, ← abs_map] + · rw [← abs_repr u, h, ← abs_map] + rfl + · rintro ⟨a, f₀, f₁, rfl, rfl, h⟩ + refine ⟨abs (.mk a fun i => ⟨(f₀ i, f₁ i), h i⟩), ?_, ?_⟩ + · rw [← abs_map] + rfl + · rw [← abs_map] rfl - intro i - exact (f i).property - rintro ⟨a, f₀, f₁, xeq, yeq, h⟩ - use abs ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩ - constructor - · rw [xeq, ← abs_map] - rfl - rw [yeq, ← abs_map]; rfl end @@ -168,17 +155,16 @@ theorem recF_eq {α : Type _} (g : F α → α) (x : q.P.W) : rfl theorem recF_eq' {α : Type _} (g : F α → α) (a : q.P.A) (f : q.P.B a → q.P.W) : - recF g ⟨a, f⟩ = g (abs (q.P.map (recF g) ⟨a, f⟩)) := + recF g ⟨a, f⟩ = g (abs (q.P.map (recF g) (.mk a f))) := rfl /-- two trees are equivalent if their F-abstractions are -/ inductive Wequiv : q.P.W → q.P.W → Prop | ind (a : q.P.A) (f f' : q.P.B a → q.P.W) : (∀ x, Wequiv (f x) (f' x)) → Wequiv ⟨a, f⟩ ⟨a, f'⟩ | abs (a : q.P.A) (f : q.P.B a → q.P.W) (a' : q.P.A) (f' : q.P.B a' → q.P.W) : - abs ⟨a, f⟩ = abs ⟨a', f'⟩ → Wequiv ⟨a, f⟩ ⟨a', f'⟩ + abs (.mk a f) = abs (.mk a' f') → Wequiv ⟨a, f⟩ ⟨a', f'⟩ | trans (u v w : q.P.W) : Wequiv u v → Wequiv v w → Wequiv u w -set_option backward.isDefEq.respectTransparency false in /-- `recF` is insensitive to the representation -/ theorem recF_eq_of_Wequiv {α : Type u} (u : F α → α) (x y : q.P.W) : Wequiv x y → recF u x = recF u y := by @@ -211,9 +197,9 @@ def Wrepr : q.P.W → q.P.W := theorem Wrepr_equiv (x : q.P.W) : Wequiv (Wrepr x) x := by induction x with | _ a f ih - apply Wequiv.trans (v := PFunctor.W.mk (q.P.map Wrepr ⟨a, f⟩)) + apply Wequiv.trans (v := PFunctor.W.mk (q.P.map Wrepr (.mk a f))) · apply Wequiv.abs' - have : Wrepr ⟨a, f⟩ = PFunctor.W.mk (repr (abs (q.P.map Wrepr ⟨a, f⟩))) := rfl + have : Wrepr ⟨a, f⟩ = PFunctor.W.mk (repr (abs (q.P.map Wrepr (.mk a f)))) := rfl rw [this, PFunctor.W.dest_mk, abs_repr] rfl apply Wequiv.ind; exact ih @@ -259,14 +245,14 @@ theorem Fix.rec_eq {α : Type _} (g : F α → α) (x : F (Fix F)) : lhs rw [Fix.rec, Fix.mk] dsimp - rcases h : repr x with ⟨a, f⟩ + cases h : repr x with | mk a f rw [PFunctor.map_eq, recF_eq, ← PFunctor.map_eq, PFunctor.W.dest_mk, PFunctor.map_map, abs_map, ← h, abs_repr, this] set_option backward.isDefEq.respectTransparency false in theorem Fix.ind_aux (a : q.P.A) (f : q.P.B a → q.P.W) : - Fix.mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦⟨a, f⟩⟧ := by - have : Fix.mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr ⟨a, f⟩⟧ := by + Fix.mk (abs (.mk a fun x => ⟦f x⟧)) = ⟦⟨a, f⟩⟧ := by + have : Fix.mk (abs (.mk a fun x => ⟦f x⟧)) = ⟦Wrepr ⟨a, f⟩⟧ := by apply Quot.sound; apply Wequiv.abs' rw [PFunctor.W.dest_mk, abs_map, abs_repr, ← abs_map, PFunctor.map_eq] simp only [Wrepr, recF_eq, PFunctor.W.dest_mk, abs_repr, Function.comp] @@ -442,7 +428,7 @@ theorem Cofix.bisim (r : Cofix F → Cofix F → Prop) apply h' theorem Cofix.bisim' {α : Type*} (Q : α → Prop) (u v : α → Cofix F) - (h : ∀ x, Q x → ∃ a f f', Cofix.dest (u x) = abs ⟨a, f⟩ ∧ Cofix.dest (v x) = abs ⟨a, f'⟩ ∧ + (h : ∀ x, Q x → ∃ a f f', Cofix.dest (u x) = abs ⟨a, f⟩ ∧ Cofix.dest (v x) = abs (.mk a f') ∧ ∀ i, ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x') : ∀ x, Q x → u x = v x := fun x Qx => let R := fun w z : Cofix F => ∃ x', Q x' ∧ w = u x' ∧ z = v x' @@ -463,49 +449,20 @@ namespace QPF variable {F₂ : Type u → Type u} [q₂ : QPF F₂] variable {F₁ : Type u → Type u} [q₁ : QPF F₁] -set_option backward.isDefEq.respectTransparency false in /-- composition of qpfs gives another qpf -/ @[instance_reducible] def comp : QPF (Functor.Comp F₂ F₁) where P := PFunctor.comp q₂.P q₁.P - abs {α} := by - dsimp [Functor.Comp] - intro p - exact abs ⟨p.1.1, fun x => abs ⟨p.1.2 x, fun y => p.2 ⟨x, y⟩⟩⟩ - repr {α} := by - dsimp [Functor.Comp] - intro y - refine ⟨⟨(repr y).1, fun u => (repr ((repr y).2 u)).1⟩, ?_⟩ - dsimp [PFunctor.comp] - intro x - exact (repr ((repr y).2 x.1)).snd x.2 - abs_repr {α} := by - dsimp [Functor.Comp] - intro x - conv => - rhs - rw [← abs_repr x] - obtain ⟨a, f⟩ := repr x - dsimp - congr with x - rcases h' : repr (f x) with ⟨b, g⟩ - dsimp; rw [← h', abs_repr] + abs {α} p := .mk <| abs (.mk p.fst.1 fun x => abs (.mk (p.fst.2 x) fun y => p.snd ⟨x, y⟩)) + repr {α} y := + .mk (.mk (repr y.run).fst fun u => (repr ((repr y.run).snd u)).fst) + fun x => (repr ((repr y.run).snd x.1)).snd x.2 + abs_repr := by simp [abs_repr] abs_map {α β} f := by - dsimp +unfoldPartialApp [Functor.Comp, PFunctor.comp] intro p - obtain ⟨a, g⟩ := p; dsimp - obtain ⟨b, h⟩ := a; dsimp - symm - trans - · symm - apply abs_map - congr - rw [PFunctor.map_eq] - dsimp [Function.comp_def] - congr - ext x - rw [← abs_map] - rfl + cases p with | mk a g + cases a with | mk b h + simp [functor_norm, ← abs_map, Function.comp_def] end QPF @@ -548,7 +505,7 @@ open Functor (Liftp Liftr supp) open Set theorem mem_supp {α : Type u} (x : F α) (u : α) : - u ∈ supp x ↔ ∀ a f, abs ⟨a, f⟩ = x → u ∈ f '' univ := by + u ∈ supp x ↔ ∀ a f, abs (.mk a f) = x → u ∈ f '' univ := by rw [supp]; dsimp; constructor · intro h a f haf have : Liftp (fun u => u ∈ f '' univ) x := by @@ -561,13 +518,13 @@ theorem mem_supp {α : Type u} (x : F α) (u : α) : rw [← hi]; apply h' theorem supp_eq {α : Type u} (x : F α) : - supp x = { u | ∀ a f, abs ⟨a, f⟩ = x → u ∈ f '' univ } := by + supp x = { u | ∀ a f, abs (.mk a f) = x → u ∈ f '' univ } := by ext apply mem_supp theorem has_good_supp_iff {α : Type u} (x : F α) : (∀ p, Liftp p x ↔ ∀ u ∈ supp x, p u) ↔ - ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ a' f', abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ := by + ∃ a f, abs (.mk a f) = x ∧ ∀ a' f', abs (.mk a' f') = x → f '' univ ⊆ f' '' univ := by constructor · intro h have : Liftp (· ∈ supp x) x := by rw [h]; intro u; exact id @@ -594,7 +551,7 @@ theorem has_good_supp_iff {α : Type u} (x : F α) : representing a single value all have the same range. -/ def IsUniform : Prop := ∀ ⦃α : Type u⦄ (a a' : q.P.A) (f : q.P.B a → α) (f' : q.P.B a' → α), - abs ⟨a, f⟩ = abs ⟨a', f'⟩ → f '' univ = f' '' univ + abs (.mk a f) = abs (.mk a' f') → f '' univ = f' '' univ /-- does `abs` preserve `Liftp`? -/ def LiftpPreservation : Prop := @@ -605,7 +562,7 @@ def SuppPreservation : Prop := ∀ ⦃α⦄ (x : q.P α), supp (abs x) = supp x theorem supp_eq_of_isUniform (h : q.IsUniform) {α : Type u} (a : q.P.A) (f : q.P.B a → α) : - supp (abs ⟨a, f⟩) = f '' univ := by + supp (abs (.mk a f)) = f '' univ := by ext u; rw [mem_supp]; constructor · intro h' apply h' _ _ rfl @@ -615,41 +572,44 @@ theorem supp_eq_of_isUniform (h : q.IsUniform) {α : Type u} (a : q.P.A) (f : q. theorem liftp_iff_of_isUniform (h : q.IsUniform) {α : Type u} (x : F α) (p : α → Prop) : Liftp p x ↔ ∀ u ∈ supp x, p u := by rw [liftp_iff, ← abs_repr x] - obtain ⟨a, f⟩ := repr x; constructor + cases repr x with | mk a f + constructor · rintro ⟨a', f', abseq, hf⟩ u rw [supp_eq_of_isUniform h, h _ _ _ _ abseq] rintro ⟨i, _, hi⟩ rw [← hi] apply hf - intro h' - refine ⟨a, f, rfl, fun i => h' _ ?_⟩ - rw [supp_eq_of_isUniform h] - exact ⟨i, mem_univ i, rfl⟩ + · intro h' + refine ⟨a, f, rfl, fun i => h' _ ?_⟩ + rw [supp_eq_of_isUniform h] + exact ⟨i, mem_univ i, rfl⟩ -set_option backward.isDefEq.respectTransparency false in theorem supp_map (h : q.IsUniform) {α β : Type u} (g : α → β) (x : F α) : supp (g <$> x) = g '' supp x := by - rw [← abs_repr x]; obtain ⟨a, f⟩ := repr x; rw [← abs_map, PFunctor.map_eq] + rw [← abs_repr x] + cases repr x with | mk a f + rw [← abs_map, PFunctor.map_eq] rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, image_comp] -set_option backward.isDefEq.respectTransparency false in theorem suppPreservation_iff_uniform : q.SuppPreservation ↔ q.IsUniform := by constructor · intro h α a a' f f' h' rw [← PFunctor.supp_eq, ← PFunctor.supp_eq, ← h, h', h] - · rintro h α ⟨a, f⟩ + · intro h α x + cases x with | mk a f rwa [supp_eq_of_isUniform, PFunctor.supp_eq] -set_option backward.isDefEq.respectTransparency false in theorem suppPreservation_iff_liftpPreservation : q.SuppPreservation ↔ q.LiftpPreservation := by constructor <;> intro h - · rintro α p ⟨a, f⟩ + · intro α p x + cases x with | mk a f have h' := h rw [suppPreservation_iff_uniform] at h' dsimp only [SuppPreservation, supp] at h rw [liftp_iff_of_isUniform h', supp_eq_of_isUniform h', PFunctor.liftp_iff'] simp - · rintro α ⟨a, f⟩ + · intro α x + cases x with | mk a f simp only [LiftpPreservation] at h simp only [supp, h] From 4a1f936d72ecd09c8737c6fabfe05f1432f42d3b Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 19:58:34 -0400 Subject: [PATCH 2/9] fix uppercase --- Mathlib/Control/Functor.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Control/Functor.lean b/Mathlib/Control/Functor.lean index 53d67f44c18784..74c57d89e7c41a 100644 --- a/Mathlib/Control/Functor.lean +++ b/Mathlib/Control/Functor.lean @@ -144,7 +144,7 @@ def Comp.run {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : x @[simp] -theorem Comp.run_MK {F : Type u → Type w} {G : Type v → Type u} {α : Type v} +theorem Comp.run_mk {F : Type u → Type w} {G : Type v → Type u} {α : Type v} (x : F (G α)) : (mk x).run = x := rfl @[simp] From 383a4b948a197b43bca26663dcbfbaaafe90ffec Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 21:00:54 -0400 Subject: [PATCH 3/9] add docstrings --- Mathlib/Data/PFunctor/Univariate/Basic.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Data/PFunctor/Univariate/Basic.lean b/Mathlib/Data/PFunctor/Univariate/Basic.lean index d99a4dabdc4542..ef99e15eb07181 100644 --- a/Mathlib/Data/PFunctor/Univariate/Basic.lean +++ b/Mathlib/Data/PFunctor/Univariate/Basic.lean @@ -54,9 +54,15 @@ section Obj variable {P} +/-- Make an element of `P α` from a "shape" `a : P.A` and a family of elements `f : P.B a → α`. + +Important: You should use `PFunctor.Obj.mk` instead of the anonymous constructor `⟨_, _⟩` to avoid abuse +of the definitional equality between `P.Obj α` and `Σ x : P.A, P.B x → α`. -/ @[implicit_reducible, match_pattern] def Obj.mk (a : P.A) (f : P.B a → α) : P α := ⟨a, f⟩ +/-- To prove a theorem about `t : P.Obj α` it suffices to +prove it for `P.Obj.mk a f` for all possible values of `a` and `f`. -/ @[implicit_reducible, elab_as_elim, induction_eliminator, cases_eliminator, match_pattern] def Obj.rec {motive : P α → Sort*} (mk : ∀ a f, motive (.mk a f)) : ∀ t, motive t := fun t => mk t.1 t.2 From 16db7295cb379b63e4b066422c45c95075ca13c3 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 21:04:25 -0400 Subject: [PATCH 4/9] add more docstrings --- Mathlib/Data/PFunctor/Univariate/Basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Data/PFunctor/Univariate/Basic.lean b/Mathlib/Data/PFunctor/Univariate/Basic.lean index ef99e15eb07181..b5a71dafb8bb66 100644 --- a/Mathlib/Data/PFunctor/Univariate/Basic.lean +++ b/Mathlib/Data/PFunctor/Univariate/Basic.lean @@ -72,7 +72,10 @@ theorem Obj.rec_mk {motive : P α → Sort*} {mk : ∀ a b, motive (.mk a b)} (a : P.A) (b : P.B a → α) : Obj.rec mk (.mk a b) = mk a b := rfl +/-- Extract the "shape" of a `x : P α` as `x.fst : P.A`. -/ @[implicit_reducible] def Obj.fst (x : P α) : P.A := x.1 +/-- Extract the underlying value of type `α` associated to an object `x : P α` +at an index `i : P.B x.fst`. -/ @[implicit_reducible] def Obj.snd (x : P α) : P.B x.fst → α := x.2 @[simp] theorem Obj.fst_mk (a : P.A) (f : P.B a → α) : Obj.fst (.mk a f) = a := rfl From 986380d615839b232af5140eb4539e6fef71aa72 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 21:06:17 -0400 Subject: [PATCH 5/9] not a match pattern lol --- Mathlib/Data/PFunctor/Univariate/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/PFunctor/Univariate/Basic.lean b/Mathlib/Data/PFunctor/Univariate/Basic.lean index b5a71dafb8bb66..b657b52cd78775 100644 --- a/Mathlib/Data/PFunctor/Univariate/Basic.lean +++ b/Mathlib/Data/PFunctor/Univariate/Basic.lean @@ -63,7 +63,7 @@ def Obj.mk (a : P.A) (f : P.B a → α) : P α := ⟨a, f⟩ /-- To prove a theorem about `t : P.Obj α` it suffices to prove it for `P.Obj.mk a f` for all possible values of `a` and `f`. -/ -@[implicit_reducible, elab_as_elim, induction_eliminator, cases_eliminator, match_pattern] +@[implicit_reducible, elab_as_elim, induction_eliminator, cases_eliminator] def Obj.rec {motive : P α → Sort*} (mk : ∀ a f, motive (.mk a f)) : ∀ t, motive t := fun t => mk t.1 t.2 From 8adf5dc1785bf041e655bc42682f2b7d9b1242a5 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 21:06:41 -0400 Subject: [PATCH 6/9] docstring hide coercion --- Mathlib/Data/PFunctor/Univariate/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/PFunctor/Univariate/Basic.lean b/Mathlib/Data/PFunctor/Univariate/Basic.lean index b657b52cd78775..8ee446f2575810 100644 --- a/Mathlib/Data/PFunctor/Univariate/Basic.lean +++ b/Mathlib/Data/PFunctor/Univariate/Basic.lean @@ -57,7 +57,7 @@ variable {P} /-- Make an element of `P α` from a "shape" `a : P.A` and a family of elements `f : P.B a → α`. Important: You should use `PFunctor.Obj.mk` instead of the anonymous constructor `⟨_, _⟩` to avoid abuse -of the definitional equality between `P.Obj α` and `Σ x : P.A, P.B x → α`. -/ +of the definitional equality between `P α` and `Σ x : P.A, P.B x → α`. -/ @[implicit_reducible, match_pattern] def Obj.mk (a : P.A) (f : P.B a → α) : P α := ⟨a, f⟩ From 8601a1b4bbed83b07c54cce2d0bdbfbc9e58e918 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 21:07:01 -0400 Subject: [PATCH 7/9] docstring hide coercion again --- Mathlib/Data/PFunctor/Univariate/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/PFunctor/Univariate/Basic.lean b/Mathlib/Data/PFunctor/Univariate/Basic.lean index 8ee446f2575810..66e1ace00308db 100644 --- a/Mathlib/Data/PFunctor/Univariate/Basic.lean +++ b/Mathlib/Data/PFunctor/Univariate/Basic.lean @@ -61,7 +61,7 @@ of the definitional equality between `P α` and `Σ x : P.A, P.B x → α`. -/ @[implicit_reducible, match_pattern] def Obj.mk (a : P.A) (f : P.B a → α) : P α := ⟨a, f⟩ -/-- To prove a theorem about `t : P.Obj α` it suffices to +/-- To prove a theorem about `t : P α` it suffices to prove it for `P.Obj.mk a f` for all possible values of `a` and `f`. -/ @[implicit_reducible, elab_as_elim, induction_eliminator, cases_eliminator] def Obj.rec {motive : P α → Sort*} (mk : ∀ a f, motive (.mk a f)) : ∀ t, motive t := From d8bee3699b7d0cca3b7158d27ffdec2b0128bba4 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 21:14:13 -0400 Subject: [PATCH 8/9] long line --- Mathlib/Data/PFunctor/Univariate/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/PFunctor/Univariate/Basic.lean b/Mathlib/Data/PFunctor/Univariate/Basic.lean index 66e1ace00308db..dbf6d1fb6d0b5d 100644 --- a/Mathlib/Data/PFunctor/Univariate/Basic.lean +++ b/Mathlib/Data/PFunctor/Univariate/Basic.lean @@ -56,8 +56,8 @@ variable {P} /-- Make an element of `P α` from a "shape" `a : P.A` and a family of elements `f : P.B a → α`. -Important: You should use `PFunctor.Obj.mk` instead of the anonymous constructor `⟨_, _⟩` to avoid abuse -of the definitional equality between `P α` and `Σ x : P.A, P.B x → α`. -/ +Important: You should use `PFunctor.Obj.mk` instead of the anonymous constructor `⟨_, _⟩` +to avoid abuse of the definitional equality between `P α` and `Σ x : P.A, P.B x → α`. -/ @[implicit_reducible, match_pattern] def Obj.mk (a : P.A) (f : P.B a → α) : P α := ⟨a, f⟩ From 5c64610700491ad639f9f84515cb19e6b5ec98eb Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Mon, 24 Aug 2026 08:33:26 -0400 Subject: [PATCH 9/9] `Sigma.snd` is fine now --- Mathlib/Data/QPF/Univariate/Basic.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Data/QPF/Univariate/Basic.lean b/Mathlib/Data/QPF/Univariate/Basic.lean index ab032dd73e2753..d214502c17c99d 100644 --- a/Mathlib/Data/QPF/Univariate/Basic.lean +++ b/Mathlib/Data/QPF/Univariate/Basic.lean @@ -109,8 +109,6 @@ theorem liftp_iff {α : Type u} (p : α → Prop) (x : F α) : rw [← abs_map, h₀] rfl --- TODO: fix defeq abuse with `Sigma.snd` -set_option backward.isDefEq.respectTransparency false in theorem liftp_iff' {α : Type u} (p : α → Prop) (x : F α) : Liftp p x ↔ ∃ u : q.P α, abs u = x ∧ ∀ i, p (u.snd i) := by rw [liftp_iff]