From a8f80fb37e92ac3755c8f478f322ab964f605053 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 11 Sep 2025 20:06:17 +0100 Subject: [PATCH] chore: add comments to `Sequences.lean` --- .../Sequences.lean | 150 ++++++++++++++---- 1 file changed, 117 insertions(+), 33 deletions(-) diff --git a/LeroyCompilerVerificationCourse/Sequences.lean b/LeroyCompilerVerificationCourse/Sequences.lean index ad428ac..678f489 100644 --- a/LeroyCompilerVerificationCourse/Sequences.lean +++ b/LeroyCompilerVerificationCourse/Sequences.lean @@ -4,31 +4,11 @@ Released under LGPL 2.1 license as described in the file LICENSE.md. Authors: Wojciech Różowski -/ -def infseq {α} (R : α → α → Prop) : α → Prop := - λ x : α => ∃ y, R x y ∧ infseq R y - coinductive_fixpoint - --- Application of the rewrite rule -def infseq_fixpoint {α} (R : α → α → Prop) (x : α) : - infseq R x = ∃ y, R x y ∧ infseq R y := by - rw [infseq] - --- The associated coinduction principle -theorem infseq_coinduction_principle {α} (h : α → Prop) (R : α → α → Prop) - (prem : ∀ (x : α), h x → ∃ y, R x y ∧ h y) : ∀ x, h x → infseq R x := by - apply infseq.coinduct - grind +/- + Finite sequences of transitions -/-- -info: infseq.coinduct.{u_1} {α : Sort u_1} (R : α → α → Prop) (pred : α → Prop) - (hyp : ∀ (x : α), pred x → ∃ y, R x y ∧ pred y) (x✝ : α) : pred x✝ → infseq R x✝ + Zero, one or several transitions: reflexive, transitive closure of `R`. -/ -#guard_msgs in #check infseq.coinduct - --- Simple proof by coinduction -theorem cycle_infseq {R : α → α → Prop} (x : α) : R x x → infseq R x := - infseq.coinduct R (λ m => R m m) (by grind) _ - @[grind] inductive star (R : α → α → Prop) : α → α → Prop where | star_refl : ∀ x : α, star R x x | star_step : ∀ {x y z}, R x y → star R y z → star R x z @@ -42,6 +22,9 @@ attribute [grind =>] star.star_step @[grind] theorem star_trans {α} (R : α → α → Prop) (a b : α) (sab : star R a b) : ∀ c : α, star R b c → star R a c := by induction sab with grind +/- + One or several transitions: transitive closure of `R`. +-/ @[grind cases] inductive plus (R : α → α → Prop) : α → α → Prop where | plus_left : ∀ {a b c}, R a b → star R b c → plus R a c @@ -78,14 +61,95 @@ theorem star_plus_trans : -- grind_pattern star_plus_trans => star R a b, plus R b c + theorem plus_right : star R a b -> R b c -> plus R a c := by grind +/- + No transitions from a state. +-/ +@[grind] def irred (R : α → α → Prop) (a : α) : Prop := ∀ b, ¬(R a b) + +/- + Infinite sequences of transitions + + It is easy to characterize the fact that all transition sequences starting + from a state `a` are infinite: it suffices to say that any finite sequence + starting from `a` can always be extended by one more transition. +-/ def all_seq_inf (R : α → α → Prop) (x : α) : Prop := ∀ y : α, star R x y → ∃ z, R y z +/- + However, this is not the notion we are trying to characterize: that, starting + from `x`, there exists one infinite sequence of transitions + `x` --> `x₁` --> `x₂` --> ... -> `xₙ` -> .... + + Indeed, consider `R : Nat → Nat → Prop` such that `R 0 0` and `R 0 1`. + `all_seq_inf 0` does not hold, because a sequence `0` -->* `1` cannot be extended. + Yet, `R` admits an infinite sequence, namely `0` --> `0` --> ... + + Another attempt would be to represent the sequence of states + `x` --> `x₁` --> `x₂` --> ... -> `xₙ` -> ... explicitly, as a function + `f : Nat → α` such that `f i` is the `i`-th state `xᵢ` of the sequence. +-/ def infseq_with_function (R : α → α → Prop) (a: α) : Prop := ∃ f : Nat → α, f 0 = a ∧ ∀ i, R (f i) (f (1 + i)) +/- + This is a correct characterization of the existence of an infinite sequence + of reductions. However, it is very inconvenient to work with this definition. + To obtain a practical definition of infinite sequences, we use the following + coinductive definition of the predicate `infseq R`. + + An inductive predicate is the least fixpoint: the smallest predicate that satisfies its constructors; a coinductive predicate is a greatest fixpoint: the largest predicate that satisfies its defining equation. + + The `infseq` predicate above must be defined coinductively. Indeed, if we define it inductively, the predicate would be empty (always false), since there are no base cases! +-/ +def infseq {α} (R : α → α → Prop) : α → Prop := + λ x : α => ∃ y, R x y ∧ infseq R y + coinductive_fixpoint + +-- Application of the rewrite rule +def infseq_fixpoint {α} (R : α → α → Prop) (x : α) : + infseq R x = ∃ y, R x y ∧ infseq R y := by + rw [infseq] + +/- +Consider a set `h` of states `α`, that is, a predicate `h : α → Prop. + +Assume that for every `x` in `h`, we can make one `R` transition to a `y` +that is still in `h`. Then, starting from `x` in `h`, we can transition to +some `x₁` in `h`, then to some `x₂` still in `h`, then... It is clear +that we are just building an infinite sequence of transitions starting from +`x`. Therefore `infseq R x` should hold. +-/ +theorem infseq_coinduction_principle {α} (h : α → Prop) (R : α → α → Prop) + (prem : ∀ (x : α), h x → ∃ y, R x y ∧ h y) : ∀ x, h x → infseq R x := by + apply infseq.coinduct + grind + +/- + Lean provides support for constructing proofs by coinduction. + For example, we can prove the following: +-/ + +theorem cycle_infseq {R : α → α → Prop} (x : α) : R x x → infseq R x := + infseq.coinduct R (λ m => R m m) (by grind) _ + +/- + An even more useful variant of this coinduction principle considers a + set `X` where for every `a` in `X`, we can make one *or several* transitions + to reach a `b` in `X`. +-/ +theorem infseq_coinduction_principle_2 + (X : α → Prop) (h₁ : ∀ (a : α), X a → ∃ b, plus R a b ∧ X b) (a : α) (rel : X a) : infseq R a := by + apply infseq.coinduct _ (fun a => ∃ b, star R a b ∧ X b) <;> grind + +/- + Here is an example of use of `infseq_coinduction_principle`: + if all finite transition sequences starting at `x` can be extended, + `infseq R x` holds. +-/ def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x → infseq R x := by apply infseq.coinduct intro x H @@ -99,10 +163,10 @@ def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x → apply H grind -theorem infseq_coinduction_principle_2 - (X : α → Prop) (h₁ : ∀ (a : α), X a → ∃ b, plus R a b ∧ X b) (a : α) (rel : X a) : infseq R a := by - apply infseq.coinduct _ (fun a => ∃ b, star R a b ∧ X b) <;> grind - +/- + Likewise, the function-based characterization `infseq_with_function` + implies `infseq`. +-/ theorem infseq_from_function : ∀ a, infseq_with_function R a → infseq R a := by apply infseq.coinduct intro x hyp @@ -112,29 +176,49 @@ theorem infseq_from_function : ∀ a, infseq_with_function R a → infseq R a := unfold infseq_with_function refine ⟨fun n => f (n + 1), by grind⟩ -@[grind] def irred (R : α → α → Prop) (a : α) : Prop := ∀ b, ¬(R a b) +section -theorem star_star_inv (R_functional : ∀ a b c, R a b -> R a c -> b = c) (sab : star R a b) : +/- + A transition relation is functional if every state can transition to at most + one other state. +-/ +variable {R : α → α → Prop} (R_functional : ∀ a b c, R a b -> R a c -> b = c) + +include R_functional + +/- + Uniqueness of finite transition sequences. +-/ +theorem star_star_inv (sab : star R a b) : ∀ c, star R a c → star R b c ∨ star R c b := by induction sab with grind -theorem finseq_unique (R_functional : ∀ a b c, R a b -> R a c -> b = c) : +theorem finseq_unique : ∀ a b b', star R a b → irred R b → star R a b' → irred R b' → b = b' := by intro a b b' sab ib sab' ib' apply Or.elim (star_star_inv R_functional sab b' sab') <;> grind -@[grind] theorem infseq_star_inv (R_functional : ∀ a b c, R a b -> R a c -> b = c) : ∀ a b, star R a b → infseq R a → infseq R b := by +/- + A state cannot both diverge and terminate on an irreducible state. +-/ +@[grind] theorem infseq_star_inv : ∀ a b, star R a b → infseq R a → infseq R b := by intro a b sab ia induction sab with grind [infseq] -theorem infseq_finseq_excl (R_functional : ∀ a b c, R a b -> R a c -> b = c): ∀ a b, star R a b → irred R b → infseq R a → False := by +theorem infseq_finseq_excl : ∀ a b, star R a b → irred R b → infseq R a → False := by intro a b sab irb ia have h : infseq R b := by grind grind [infseq] -theorem infseq_all_seq_inf (R_functional : ∀ a b c, R a b -> R a c -> b = c): ∀ a, infseq R a → all_seq_inf R a := by +/- + If there exists an infinite sequence of transitions from `a`, + all sequences of transitions arising from `a` are infinite. +-/ +theorem infseq_all_seq_inf : ∀ a, infseq R a → all_seq_inf R a := by intro a ia unfold all_seq_inf intro b sab have h : infseq R b := by grind grind [infseq] + +end