From a8a6f71abbec7728bf29de3b23e225051f787fdd Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Mon, 19 May 2025 12:27:46 +0100
Subject: [PATCH] fix: add monotonicity lemmas for universal quantifiers
 (#8403)

This PR adds missing monotonicity lemmas for universal quantifiers, that
are used in defining (co)inductive predicates.
---
 src/Init/Internal/Order/Basic.lean         | 12 ++++++++++++
 tests/lean/run/coinductive_predicates.lean | 20 ++++++++++++++++++++
 2 files changed, 32 insertions(+)

diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean
index bb6409c400..f1f92c27f2 100644
--- a/src/Init/Internal/Order/Basic.lean
+++ b/src/Init/Internal/Order/Basic.lean
@@ -877,6 +877,12 @@ instance ImplicationOrder.instCompleteLattice : CompleteLattice ImplicationOrder
     @monotone _ _ _ ImplicationOrder.instOrder (fun x => (Exists (f x))) :=
   fun x y hxy ⟨w, hw⟩ => ⟨w, monotone_apply w f h x y hxy hw⟩
 
+@[partial_fixpoint_monotone] theorem implication_order_monotone_forall
+    {α} [PartialOrder α] {β} (f : α → β → ImplicationOrder)
+    (h : monotone f) :
+    @monotone _ _ _ ImplicationOrder.instOrder (fun x => ∀ y, f x y) :=
+  fun x y hxy h₂ y₁ => monotone_apply y₁ f h x y hxy (h₂ y₁)
+
 @[partial_fixpoint_monotone] theorem implication_order_monotone_and
     {α} [PartialOrder α] (f₁ : α → ImplicationOrder) (f₂ : α → ImplicationOrder)
     (h₁ : @monotone _ _ _ ImplicationOrder.instOrder f₁)
@@ -931,6 +937,12 @@ def ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplica
     @monotone _ _ _ ReverseImplicationOrder.instOrder (fun x => Exists (f x)) :=
   fun x y hxy ⟨w, hw⟩ => ⟨w, monotone_apply w f h x y hxy hw⟩
 
+@[partial_fixpoint_monotone] theorem coind_monotone_forall
+    {α} [PartialOrder α] {β} (f : α → β → ReverseImplicationOrder)
+    (h : monotone f) :
+    @monotone _ _ _ ReverseImplicationOrder.instOrder (fun x => ∀ y, f x y) :=
+  fun x y hxy h₂ y₁ => monotone_apply y₁ f h x y hxy (h₂ y₁)
+
 @[partial_fixpoint_monotone] theorem coind_monotone_and
     {α} [PartialOrder α] (f₁ : α → Prop) (f₂ : α → Prop)
     (h₁ : @monotone _ _ _ ReverseImplicationOrder.instOrder f₁)
diff --git a/tests/lean/run/coinductive_predicates.lean b/tests/lean/run/coinductive_predicates.lean
index b23d04d837..b7be0fa565 100644
--- a/tests/lean/run/coinductive_predicates.lean
+++ b/tests/lean/run/coinductive_predicates.lean
@@ -156,3 +156,23 @@ theorem infseq_coinduction_principle_2:
         exact rel2
         apply Exists.intro mid
         exact ⟨ s, h₆ ⟩
+
+-- Automata theory example that involves forall quantifier
+def DFA (Q : Type) (A : Type) : Type := Q → (Bool × (A → Q))
+
+def language_equivalent (automaton : DFA Q A) (q₁ q₂ : Q)  : Prop :=
+  let ⟨o₁, t₁⟩ := automaton q₁
+  let ⟨o₂, t₂⟩ := automaton q₂
+  o₁ = o₂ ∧ (∀ a : A, language_equivalent automaton (t₁ a) (t₂ a))
+greatest_fixpoint
+
+/--
+info: language_equivalent.fixpoint_induct {Q A : Type} (automaton : DFA Q A) (x : Q → Q → Prop)
+  (y :
+    ∀ (x_1 x_2 : Q),
+      x x_1 x_2 →
+        (automaton x_1).fst = (automaton x_2).fst ∧ ∀ (a : A), x ((automaton x_1).snd a) ((automaton x_2).snd a))
+  (x✝ x✝¹ : Q) : x x✝ x✝¹ → language_equivalent automaton x✝ x✝¹
+-/
+#guard_msgs in
+#check language_equivalent.fixpoint_induct