max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: rename keywords for (co)inductive predicates and the names of the associated (co)induction principles

Browse source
This commit is contained in:
Wojciech Rozowski 2025-06-23 17:41:22 +02:00 • committed by Joachim Breitner
parent b4b68415e0
commit 22cd34c341
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
View file

@ -131,7 +131,7 @@ theorem IterM.step_filterM {f : β → n (ULift Bool)}
intro step
match step with
| .yield it' out h =>
simp only [PostconditionT.lift,
simp only [PostconditionT.lift,
PostconditionT.operation_map, Functor.map_map, PlausibleIterStep.skip,
PlausibleIterStep.yield, bind_map_left]
apply bind_congr
@ -156,7 +156,7 @@ theorem IterM.step_mapM {γ : Type w} {f : β → n γ}
match step with
| .yield it' out h =>
simp only [bind_pure_comp]
simp only [PostconditionT.lift, Functor.map,
simp only [PostconditionT.lift, Functor.map,
]
simp only [PostconditionT.operation_map, Functor.map_map, PlausibleIterStep.skip,
PlausibleIterStep.yield, bind_map_left, bind_pure_comp]
@ -483,7 +483,7 @@ theorem IterM.Equiv.filterMapWithPostcondition {α₁ α₂ β γ : Type w}
(h : IterM.Equiv ita itb) :
IterM.Equiv (ita.filterMapWithPostcondition f) (itb.filterMapWithPostcondition f) := by
rw [IterM.Equiv]
refine BundledIterM.Equiv.fixpoint_induct n γ ?R ?implies (.ofIterM _) (.ofIterM _) ?hR
refine BundledIterM.Equiv.coinduct n γ ?R ?implies (.ofIterM _) (.ofIterM _) ?hR
case R =>
intro ita' itb'
exact ∃ (ita : IterM (α := α₁) m β) (itb : IterM (α := α₂) m β),

6
src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean
View file

@ -83,7 +83,7 @@ def BundledIterM.Equiv (m : Type w → Type w') (β : Type w) [Monad m] [LawfulM
(ita itb : BundledIterM m β) : Prop :=
(BundledIterM.step ita).map (IterStep.mapIterator (Quot.mk (BundledIterM.Equiv m β))) =
(BundledIterM.step itb).map (IterStep.mapIterator (Quot.mk (BundledIterM.Equiv m β)))
greatest_fixpoint monotonicity by
coinductive_fixpoint monotonicity by
intro R S hRS ita itb h
simp only [BundledIterM.step] at ⊢ h
simp only [quotMk_eq_quotOfQuot_comp hRS, IterStep.mapIterator_comp, HetT.comp_map, h]
@ -130,7 +130,7 @@ protected theorem BundledIterM.Equiv.exact {m : Type w → Type w'} {β : Type w
[LawfulMonad m] (ita itb : BundledIterM m β) :
Quot.mk (BundledIterM.Equiv m β) ita =
Quot.mk (BundledIterM.Equiv m β) itb → BundledIterM.Equiv m β ita itb := by
refine BundledIterM.Equiv.fixpoint_induct m β
refine BundledIterM.Equiv.coinduct m β
(fun ita' itb' => Quot.mk _ ita' = Quot.mk _ itb') ?_ ita itb
intro ita' itb' h
replace h := congrArg (BundledIterM.stepOnQuotient) h
@ -240,7 +240,7 @@ theorem IterM.Equiv.of_morphism {α₁ α₂} {m : Type w → Type w'} [Monad m]
(f : IterM (α := α₁) m β → IterM (α := α₂) m β)
(h : ∀ it, IterM.stepAsHetT (f it) = IterStep.mapIterator f <$> IterM.stepAsHetT it) :
IterM.Equiv ita (f ita) := by
refine BundledIterM.Equiv.fixpoint_induct m β ?R ?implies (.ofIterM ita) (.ofIterM (f ita)) ?hf
refine BundledIterM.Equiv.coinduct m β ?R ?implies (.ofIterM ita) (.ofIterM (f ita)) ?hf
case R =>
intro ita itb
exact ∃ it, ita = .ofIterM it ∧ itb = .ofIterM (f it)