diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index 8e23455a4d..4c58ba04e3 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -254,6 +254,7 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as : | [], b, _ => pure b | a::as', b, h => do have : a ∈ as := by + clear f have ⟨bs, h⟩ := h subst h exact mem_append_right _ (Mem.head ..) diff --git a/src/Init/Internal/Order.lean b/src/Init/Internal/Order.lean index e5389b4516..49eac64248 100644 --- a/src/Init/Internal/Order.lean +++ b/src/Init/Internal/Order.lean @@ -5,4 +5,5 @@ Authors: Joachim Breitner -/ prelude import Init.Internal.Order.Basic +import Init.Internal.Order.Lemmas import Init.Internal.Order.Tactic diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean index e94bc3fecc..cfc7121e58 100644 --- a/src/Init/Internal/Order/Basic.lean +++ b/src/Init/Internal/Order/Basic.lean @@ -104,7 +104,7 @@ variable {α : Sort u} [PartialOrder α] variable {β : Sort v} [PartialOrder β] /-- -A function is monotone if if it maps related elements to releated elements. +A function is monotone if it maps related elements to releated elements. This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise. -/ @@ -401,6 +401,7 @@ theorem monotone_letFun (hmono : ∀ y, monotone (fun x => k x y)) : monotone fun (x : α) => letFun v (k x) := hmono v +@[partial_fixpoint_monotone] theorem monotone_ite {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] (c : Prop) [Decidable c] @@ -411,6 +412,7 @@ theorem monotone_ite · apply hmono₁ · apply hmono₂ +@[partial_fixpoint_monotone] theorem monotone_dite {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] (c : Prop) [Decidable c] @@ -440,38 +442,41 @@ instance [PartialOrder α] [PartialOrder β] : PartialOrder (α ×' β) where dsimp at * rw [rel_antisymm ha.1 hb.1, rel_antisymm ha.2 hb.2] -theorem monotone_pprod [PartialOrder α] [PartialOrder β] [PartialOrder γ] +@[partial_fixpoint_monotone] +theorem PProd.monotone_mk [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : γ → α} {g : γ → β} (hf : monotone f) (hg : monotone g) : monotone (fun x => PProd.mk (f x) (g x)) := fun _ _ h12 => ⟨hf _ _ h12, hg _ _ h12⟩ -theorem monotone_pprod_fst [PartialOrder α] [PartialOrder β] [PartialOrder γ] +@[partial_fixpoint_monotone] +theorem PProd.monotone_fst [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : γ → α ×' β} (hf : monotone f) : monotone (fun x => (f x).1) := fun _ _ h12 => (hf _ _ h12).1 -theorem monotone_pprod_snd [PartialOrder α] [PartialOrder β] [PartialOrder γ] +@[partial_fixpoint_monotone] +theorem PProd.monotone_snd [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : γ → α ×' β} (hf : monotone f) : monotone (fun x => (f x).2) := fun _ _ h12 => (hf _ _ h12).2 -def chain_pprod_fst [CCPO α] [CCPO β] (c : α ×' β → Prop) : α → Prop := fun a => ∃ b, c ⟨a, b⟩ -def chain_pprod_snd [CCPO α] [CCPO β] (c : α ×' β → Prop) : β → Prop := fun b => ∃ a, c ⟨a, b⟩ +def PProd.chain.fst [CCPO α] [CCPO β] (c : α ×' β → Prop) : α → Prop := fun a => ∃ b, c ⟨a, b⟩ +def PProd.chain.snd [CCPO α] [CCPO β] (c : α ×' β → Prop) : β → Prop := fun b => ∃ a, c ⟨a, b⟩ -theorem chain.pprod_fst [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) : - chain (chain_pprod_fst c) := by +theorem PProd.chain.chain_fst [CCPO α] [CCPO β] {c : α ×' β → Prop} (hchain : chain c) : + chain (chain.fst c) := by intro a₁ a₂ ⟨b₁, h₁⟩ ⟨b₂, h₂⟩ cases hchain ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h₁ h₂ case inl h => left; exact h.1 case inr h => right; exact h.1 -theorem chain.pprod_snd [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) : - chain (chain_pprod_snd c) := by +theorem PProd.chain.chain_snd [CCPO α] [CCPO β] {c : α ×' β → Prop} (hchain : chain c) : + chain (chain.snd c) := by intro b₁ b₂ ⟨a₁, h₁⟩ ⟨a₂, h₂⟩ cases hchain ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h₁ h₂ case inl h => left; exact h.2 case inr h => right; exact h.2 -instance [CCPO α] [CCPO β] : CCPO (α ×' β) where - csup c := ⟨CCPO.csup (chain_pprod_fst c), CCPO.csup (chain_pprod_snd c)⟩ +instance instCCPOPProd [CCPO α] [CCPO β] : CCPO (α ×' β) where + csup c := ⟨CCPO.csup (PProd.chain.fst c), CCPO.csup (PProd.chain.snd c)⟩ csup_spec := by intro ⟨a, b⟩ c hchain dsimp @@ -480,32 +485,32 @@ instance [CCPO α] [CCPO β] : CCPO (α ×' β) where intro ⟨h₁, h₂⟩ ⟨a', b'⟩ cab constructor <;> dsimp at * · apply rel_trans ?_ h₁ - apply le_csup hchain.pprod_fst + apply le_csup (PProd.chain.chain_fst hchain) exact ⟨b', cab⟩ · apply rel_trans ?_ h₂ - apply le_csup hchain.pprod_snd + apply le_csup (PProd.chain.chain_snd hchain) exact ⟨a', cab⟩ next => intro h constructor <;> dsimp - · apply csup_le hchain.pprod_fst + · apply csup_le (PProd.chain.chain_fst hchain) intro a' ⟨b', hcab⟩ apply (h _ hcab).1 - · apply csup_le hchain.pprod_snd + · apply csup_le (PProd.chain.chain_snd hchain) intro b' ⟨a', hcab⟩ apply (h _ hcab).2 theorem admissible_pprod_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : α → Prop) (hadm : admissible P) : admissible (fun (x : α ×' β) => P x.1) := by intro c hchain h - apply hadm _ hchain.pprod_fst + apply hadm _ (PProd.chain.chain_fst hchain) intro x ⟨y, hxy⟩ apply h ⟨x,y⟩ hxy theorem admissible_pprod_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : β → Prop) (hadm : admissible P) : admissible (fun (x : α ×' β) => P x.2) := by intro c hchain h - apply hadm _ hchain.pprod_snd + apply hadm _ (PProd.chain.chain_snd hchain) intro y ⟨x, hxy⟩ apply h ⟨x,y⟩ hxy @@ -609,6 +614,7 @@ class MonoBind (m : Type u → Type v) [Bind m] [∀ α, PartialOrder (m α)] wh bind_mono_left {a₁ a₂ : m α} {f : α → m b} (h : a₁ ⊑ a₂) : a₁ >>= f ⊑ a₂ >>= f bind_mono_right {a : m α} {f₁ f₂ : α → m b} (h : ∀ x, f₁ x ⊑ f₂ x) : a >>= f₁ ⊑ a >>= f₂ +@[partial_fixpoint_monotone] theorem monotone_bind (m : Type u → Type v) [Bind m] [∀ α, PartialOrder (m α)] [MonoBind m] {α β : Type u} @@ -634,7 +640,7 @@ noncomputable instance : MonoBind Option where · exact FlatOrder.rel.refl · exact h _ -theorem admissible_eq_some (P : Prop) (y : α) : +theorem Option.admissible_eq_some (P : Prop) (y : α) : admissible (fun (x : Option α) => x = some y → P) := by apply admissible_flatOrder; simp @@ -677,7 +683,7 @@ theorem find_spec : ∀ n m, find P n = some m → n ≤ m ∧ P m := by refine fix_induct (motive := fun (f : Nat → Option Nat) => ∀ n m, f n = some m → n ≤ m ∧ P m) _ ?hadm ?hstep case hadm => -- apply admissible_pi_apply does not work well, hard to infer everything - exact admissible_pi_apply _ (fun n => admissible_pi _ (fun m => admissible_eq_some _ m)) + exact admissible_pi_apply _ (fun n => admissible_pi _ (fun m => Option.admissible_eq_some _ m)) case hstep => intro f ih n m heq simp only [findF] at heq diff --git a/src/Init/Internal/Order/Lemmas.lean b/src/Init/Internal/Order/Lemmas.lean new file mode 100644 index 0000000000..7b56aedf69 --- /dev/null +++ b/src/Init/Internal/Order/Lemmas.lean @@ -0,0 +1,685 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ + +prelude + +import Init.Data.List.Control +import Init.Data.Array.Basic +import Init.Internal.Order.Basic + +/-! + +This file contains monotonicity lemmas for higher-order monadic operations (e.g. `mapM`) in the +standard library. This allows recursive definitions using `partial_fixpoint` to use nested +recursion. + +Ideally, every higher-order monadic funciton in the standard library has a lemma here. At the time +of writing, this file covers functions from + +* Init/Data/Option/Basic.lean +* Init/Data/List/Control.lean +* Init/Data/Array/Basic.lean + +in the order of their apperance there. No automation to check the exhaustiveness exists yet. + +The lemma statements are written manually, but follow a predictable scheme, and could be automated. +Likewise, the proofs are written very naively. Most of them could be handled by a tactic like +`monotonicity` (extended to make use of local hypotheses). +-/ + +namespace Lean.Order + +open Lean.Order + +variable {m : Type u → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] +variable {α β : Type u} +variable {γ : Type w} [PartialOrder γ] + +@[partial_fixpoint_monotone] +theorem Functor.monotone_map [LawfulMonad m] (f : γ → m α) (g : α → β) (hmono : monotone f) : + monotone (fun x => g <$> f x) := by + simp only [← LawfulMonad.bind_pure_comp ] + apply monotone_bind _ _ _ hmono + apply monotone_const + +@[partial_fixpoint_monotone] +theorem Seq.monotone_seq [LawfulMonad m] (f : γ → m α) (g : γ → m (α → β)) + (hmono₁ : monotone g) (hmono₂ : monotone f) : + monotone (fun x => g x <*> f x) := by + simp only [← LawfulMonad.bind_map ] + apply monotone_bind + · assumption + · apply monotone_of_monotone_apply + intro y + apply Functor.monotone_map + assumption + +@[partial_fixpoint_monotone] +theorem SeqLeft.monotone_seqLeft [LawfulMonad m] (f : γ → m α) (g : γ → m β) + (hmono₁ : monotone g) (hmono₂ : monotone f) : + monotone (fun x => g x <* f x) := by + simp only [seqLeft_eq] + apply Seq.monotone_seq + · apply Functor.monotone_map + assumption + · assumption + +@[partial_fixpoint_monotone] +theorem SeqRight.monotone_seqRight [LawfulMonad m] (f : γ → m α) (g : γ → m β) + (hmono₁ : monotone g) (hmono₂ : monotone f) : + monotone (fun x => g x *> f x) := by + simp only [seqRight_eq] + apply Seq.monotone_seq + · apply Functor.monotone_map + assumption + · assumption + +namespace Option + +@[partial_fixpoint_monotone] +theorem monotone_bindM (f : γ → α → m (Option β)) (xs : Option α) (hmono : monotone f) : + monotone (fun x => xs.bindM (f x)) := by + cases xs with + | none => apply monotone_const + | some x => + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_mapM (f : γ → α → m β) (xs : Option α) (hmono : monotone f) : + monotone (fun x => xs.mapM (f x)) := by + cases xs with + | none => apply monotone_const + | some x => + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_elimM (a : γ → m (Option α)) (n : γ → m β) (s : γ → α → m β) + (hmono₁ : monotone a) (hmono₂ : monotone n) (hmono₃ : monotone s) : + monotone (fun x => Option.elimM (a x) (n x) (s x)) := by + apply monotone_bind + · apply hmono₁ + · apply monotone_of_monotone_apply + intro o + cases o + case none => apply hmono₂ + case some y => + dsimp only [Option.elim] + apply monotone_apply + apply hmono₃ + +omit [MonoBind m] in +@[partial_fixpoint_monotone] +theorem monotone_getDM (o : Option α) (y : γ → m α) (hmono : monotone y) : + monotone (fun x => o.getDM (y x)) := by + cases o + · apply hmono + · apply monotone_const + +end Option + + +namespace List + +@[partial_fixpoint_monotone] +theorem monotone_mapM (f : γ → α → m β) (xs : List α) (hmono : monotone f) : + monotone (fun x => xs.mapM (f x)) := by + cases xs with + | nil => apply monotone_const + | cons _ xs => + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + dsimp + generalize [y] = ys + induction xs generalizing ys with + | nil => apply monotone_const + | cons _ _ ih => + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + apply ih + +@[partial_fixpoint_monotone] +theorem monotone_forM (f : γ → α → m PUnit) (xs : List α) (hmono : monotone f) : + monotone (fun x => xs.forM (f x)) := by + induction xs with + | nil => apply monotone_const + | cons _ _ ih => + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + apply ih + +@[partial_fixpoint_monotone] +theorem monotone_filterAuxM + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type} + (f : γ → α → m Bool) (xs acc : List α) (hmono : monotone f) : + monotone (fun x => xs.filterAuxM (f x) acc) := by + induction xs generalizing acc with + | nil => apply monotone_const + | cons _ _ ih => + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + apply ih + +@[partial_fixpoint_monotone] +theorem monotone_filterM + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type} + (f : γ → α → m Bool) (xs : List α) (hmono : monotone f) : + monotone (fun x => xs.filterM (f x)) := by + apply monotone_bind + · exact monotone_filterAuxM f xs [] hmono + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_filterRevM + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type} + (f : γ → α → m Bool) (xs : List α) (hmono : monotone f) : + monotone (fun x => xs.filterRevM (f x)) := by + exact monotone_filterAuxM f xs.reverse [] hmono + +@[partial_fixpoint_monotone] +theorem monotone_foldlM + (f : γ → β → α → m β) (init : β) (xs : List α) (hmono : monotone f) : + monotone (fun x => xs.foldlM (f x) (init := init)) := by + induction xs generalizing init with + | nil => apply monotone_const + | cons _ _ ih => + apply monotone_bind + · apply monotone_apply + apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + apply ih + +@[partial_fixpoint_monotone] +theorem monotone_foldrM + (f : γ → α → β → m β) (init : β) (xs : List α) (hmono : monotone f) : + monotone (fun x => xs.foldrM (f x) (init := init)) := by + apply monotone_foldlM + apply monotone_of_monotone_apply + intro s + apply monotone_of_monotone_apply + intro a + apply monotone_apply (a := s) + apply monotone_apply (a := a) + apply hmono + +@[partial_fixpoint_monotone] +theorem monotone_anyM + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type} + (f : γ → α → m Bool) (xs : List α) (hmono : monotone f) : + monotone (fun x => xs.anyM (f x)) := by + induction xs with + | nil => apply monotone_const + | cons _ _ ih => + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + cases y + · apply ih + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_allM + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type} + (f : γ → α → m Bool) (xs : List α) (hmono : monotone f) : + monotone (fun x => xs.allM (f x)) := by + induction xs with + | nil => apply monotone_const + | cons _ _ ih => + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + cases y + · apply monotone_const + · apply ih + +@[partial_fixpoint_monotone] +theorem monotone_findM? + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type} + (f : γ → α → m Bool) (xs : List α) (hmono : monotone f) : + monotone (fun x => xs.findM? (f x)) := by + induction xs with + | nil => apply monotone_const + | cons _ _ ih => + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + cases y + · apply ih + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_findSomeM? + (f : γ → α → m (Option β)) (xs : List α) (hmono : monotone f) : + monotone (fun x => xs.findSomeM? (f x)) := by + induction xs with + | nil => apply monotone_const + | cons _ _ ih => + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + cases y + · apply ih + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_forIn'_loop {α : Type uu} + (as : List α) (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (as' : List α) (b : β) + (p : Exists (fun bs => bs ++ as' = as)) (hmono : monotone f) : + monotone (fun x => List.forIn'.loop as (f x) as' b p) := by + induction as' generalizing b with + | nil => apply monotone_const + | cons a as' ih => + apply monotone_bind + · apply monotone_apply + apply monotone_apply + apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + cases y with + | done => apply monotone_const + | yield => apply ih + +@[partial_fixpoint_monotone] +theorem monotone_forIn' {α : Type uu} + (as : List α) (init : β) (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (hmono : monotone f) : + monotone (fun x => forIn' as init (f x)) := by + apply monotone_forIn'_loop + apply hmono + +@[partial_fixpoint_monotone] +theorem monotone_forIn {α : Type uu} + (as : List α) (init : β) (f : γ → (a : α) → β → m (ForInStep β)) (hmono : monotone f) : + monotone (fun x => forIn as init (f x)) := by + apply monotone_forIn' as init _ + apply monotone_of_monotone_apply + intro y + apply monotone_of_monotone_apply + intro p + apply monotone_apply (a := y) + apply hmono + +end List + +namespace Array + +@[partial_fixpoint_monotone] +theorem monotone_modifyM (a : Array α) (i : Nat) (f : γ → α → m α) (hmono : monotone f) : + monotone (fun x => a.modifyM i (f x)) := by + unfold Array.modifyM + split + · apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_const + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_forIn'_loop {α : Type uu} + (as : Array α) (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (i : Nat) (h : i ≤ as.size) + (b : β) (hmono : monotone f) : + monotone (fun x => Array.forIn'.loop as (f x) i h b) := by + induction i, h, b using Array.forIn'.loop.induct with + | case1 => apply monotone_const + | case2 _ _ _ _ _ _ _ ih => + apply monotone_bind + · apply monotone_apply + apply monotone_apply + apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + cases y with + | done => apply monotone_const + | yield => apply ih + +@[partial_fixpoint_monotone] +theorem monotone_forIn' {α : Type uu} + (as : Array α) (init : β) (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (hmono : monotone f) : + monotone (fun x => forIn' as init (f x)) := by + apply monotone_forIn'_loop + apply hmono + + +@[partial_fixpoint_monotone] +theorem monotone_forIn {α : Type uu} + (as : Array α) (init : β) (f : γ → (a : α) → β → m (ForInStep β)) (hmono : monotone f) : + monotone (fun x => forIn as init (f x)) := by + apply monotone_forIn' as init _ + apply monotone_of_monotone_apply + intro y + apply monotone_of_monotone_apply + intro p + apply monotone_apply (a := y) + apply hmono + +@[partial_fixpoint_monotone] +theorem monotone_foldlM_loop + (f : γ → β → α → m β) (xs : Array α) (stop : Nat) (h : stop ≤ xs.size) (i j : Nat) (b : β) + (hmono : monotone f) : monotone (fun x => Array.foldlM.loop (f x) xs stop h i j b) := by + induction i, j, b using Array.foldlM.loop.induct (h := h) with + | case1 => + simp only [Array.foldlM.loop, ↓reduceDIte, *] + apply monotone_const + | case2 _ _ _ _ _ ih => + unfold Array.foldlM.loop + simp only [↓reduceDIte, *] + apply monotone_bind + · apply monotone_apply + apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + apply ih + | case3 => + simp only [Array.foldlM.loop, ↓reduceDIte, *] + apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_foldlM + (f : γ → β → α → m β) (init : β) (xs : Array α) (start stop : Nat) (hmono : monotone f) : + monotone (fun x => xs.foldlM (f x) init start stop) := by + unfold Array.foldlM + split <;> apply monotone_foldlM_loop (hmono := hmono) + +@[partial_fixpoint_monotone] +theorem monotone_foldrM_fold + (f : γ → α → β → m β) (xs : Array α) (stop i : Nat) (h : i ≤ xs.size) (b : β) + (hmono : monotone f) : monotone (fun x => Array.foldrM.fold (f x) xs stop i h b) := by + induction i, h, b using Array.foldrM.fold.induct (stop := stop) with + | case1 => + unfold Array.foldrM.fold + simp only [↓reduceIte, *] + apply monotone_const + | case2 => + unfold Array.foldrM.fold + simp only [↓reduceIte, *] + apply monotone_const + | case3 _ _ _ _ _ _ ih => + unfold Array.foldrM.fold + simp only [reduceCtorEq, ↓reduceIte, *] + apply monotone_bind + · apply monotone_apply + apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + apply ih + +@[partial_fixpoint_monotone] +theorem monotone_foldrM + (f : γ → α → β → m β) (init : β) (xs : Array α) (start stop : Nat) (hmono : monotone f) : + monotone (fun x => xs.foldrM (f x) init start stop) := by + unfold Array.foldrM + split + · split + · apply monotone_foldrM_fold (hmono := hmono) + · apply monotone_const + · split + · apply monotone_foldrM_fold (hmono := hmono) + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_mapM (xs : Array α) (f : γ → α → m β) (hmono : monotone f) : + monotone (fun x => xs.mapM (f x)) := by + suffices ∀ i r, monotone (fun x => Array.mapM.map (f x) xs i r) by apply this + intros i r + induction i, r using Array.mapM.map.induct xs + case case1 ih => + unfold Array.mapM.map + simp only [↓reduceDIte, *] + apply monotone_bind + · apply monotone_apply + apply hmono + · intro y + apply monotone_of_monotone_apply + apply ih + case case2 => + unfold Array.mapM.map + simp only [↓reduceDIte, *] + apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_mapFinIdxM (xs : Array α) (f : γ → (i : Nat) → α → i < xs.size → m β) + (hmono : monotone f) : monotone (fun x => xs.mapFinIdxM (f x)) := by + suffices ∀ i j (h : i + j = xs.size) r, monotone (fun x => Array.mapFinIdxM.map xs (f x) i j h r) by apply this + intros i j h r + induction i, j, h, r using Array.mapFinIdxM.map.induct xs + case case1 => + apply monotone_const + case case2 ih => + apply monotone_bind + · dsimp + apply monotone_apply + apply monotone_apply + apply monotone_apply + apply hmono + · intro y + apply monotone_of_monotone_apply + apply ih + +@[partial_fixpoint_monotone] +theorem monotone_findSomeM? + (f : γ → α → m (Option β)) (xs : Array α) (hmono : monotone f) : + monotone (fun x => xs.findSomeM? (f x)) := by + unfold Array.findSomeM? + apply monotone_bind + · apply monotone_forIn + apply monotone_of_monotone_apply + intro y + apply monotone_of_monotone_apply + intro r + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_const + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_findM? + {m : Type → Type} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type} + (f : γ → α → m Bool) (xs : Array α) (hmono : monotone f) : + monotone (fun x => xs.findM? (f x)) := by + unfold Array.findM? + apply monotone_bind + · apply monotone_forIn + apply monotone_of_monotone_apply + intro y + apply monotone_of_monotone_apply + intro r + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_const + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_findIdxM? + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type u} + (f : γ → α → m Bool) (xs : Array α) (hmono : monotone f) : + monotone (fun x => xs.findIdxM? (f x)) := by + unfold Array.findIdxM? + apply monotone_bind + · apply monotone_forIn + apply monotone_of_monotone_apply + intro y + apply monotone_of_monotone_apply + intro r + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_const + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_anyM_loop + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type u} + (f : γ → α → m Bool) (xs : Array α) (stop : Nat) (h : stop ≤ xs.size) (j : Nat) + (hmono : monotone f) : monotone (fun x => Array.anyM.loop (f x) xs stop h j) := by + induction j using Array.anyM.loop.induct (h := h) with + | case2 => + unfold Array.anyM.loop + simp only [↓reduceDIte, *] + apply monotone_const + | case1 _ _ _ ih => + unfold Array.anyM.loop + simp only [↓reduceDIte, *] + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + split + · apply monotone_const + · apply ih + +@[partial_fixpoint_monotone] +theorem monotone_anyM + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type u} + (f : γ → α → m Bool) (xs : Array α) (start stop : Nat) (hmono : monotone f) : + monotone (fun x => xs.anyM (f x) start stop) := by + unfold Array.anyM + split + · apply monotone_anyM_loop + apply hmono + · apply monotone_anyM_loop + apply hmono + +@[partial_fixpoint_monotone] +theorem monotone_allM + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type u} + (f : γ → α → m Bool) (xs : Array α) (start stop : Nat) (hmono : monotone f) : + monotone (fun x => xs.allM (f x) start stop) := by + unfold Array.allM + apply monotone_bind + · apply monotone_anyM + apply monotone_of_monotone_apply + intro y + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_const + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_findSomeRevM? + (f : γ → α → m (Option β)) (xs : Array α) (hmono : monotone f) : + monotone (fun x => xs.findSomeRevM? (f x)) := by + unfold Array.findSomeRevM? + suffices ∀ i (h : i ≤ xs.size), monotone (fun x => Array.findSomeRevM?.find (f x) xs i h) by apply this + intros i h + induction i, h using Array.findSomeRevM?.find.induct with + | case1 => + unfold Array.findSomeRevM?.find + apply monotone_const + | case2 _ _ _ _ ih => + unfold Array.findSomeRevM?.find + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_of_monotone_apply + intro y + cases y with + | none => apply ih + | some y => apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_findRevM? + {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type} + (f : γ → α → m Bool) (xs : Array α) (hmono : monotone f) : + monotone (fun x => xs.findRevM? (f x)) := by + unfold Array.findRevM? + apply monotone_findSomeRevM? + apply monotone_of_monotone_apply + intro y + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_const + +@[partial_fixpoint_monotone] +theorem monotone_array_forM + (f : γ → α → m PUnit) (xs : Array α) (start stop : Nat) (hmono : monotone f) : + monotone (fun x => xs.forM (f x) start stop) := by + unfold Array.forM + apply monotone_foldlM + apply monotone_of_monotone_apply + intro y + apply hmono + +@[partial_fixpoint_monotone] +theorem monotone_array_forRevM + (f : γ → α → m PUnit) (xs : Array α) (start stop : Nat) (hmono : monotone f) : + monotone (fun x => xs.forRevM (f x) start stop) := by + unfold Array.forRevM + apply monotone_foldrM + apply monotone_of_monotone_apply + intro y + apply monotone_of_monotone_apply + intro z + apply monotone_apply + apply hmono + +@[partial_fixpoint_monotone] +theorem monotone_flatMapM + (f : γ → α → m (Array β)) (xs : Array α) (hmono : monotone f) : + monotone (fun x => xs.flatMapM (f x)) := by + unfold Array.flatMapM + apply monotone_foldlM + apply monotone_of_monotone_apply + intro y + apply monotone_of_monotone_apply + intro z + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_const + + +@[partial_fixpoint_monotone] +theorem monotone_array_filterMapM + (f : γ → α → m (Option β)) (xs : Array α) (hmono : monotone f) : + monotone (fun x => xs.filterMapM (f x)) := by + unfold Array.filterMapM + apply monotone_foldlM + apply monotone_of_monotone_apply + intro y + apply monotone_of_monotone_apply + intro z + apply monotone_bind + · apply monotone_apply + apply hmono + · apply monotone_const + +end Array + +end Lean.Order diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 0e4f09bea1..082e834773 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -9,6 +9,7 @@ import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Structural import Lean.Elab.PreDefinition.WF.Main import Lean.Elab.PreDefinition.MkInhabitant +import Lean.Elab.PreDefinition.PartialFixpoint namespace Lean.Elab open Meta @@ -162,7 +163,8 @@ def ensureFunIndReservedNamesAvailable (preDefs : Array PreDefinition) : MetaM U Checks consistency of a clique of TerminationHints: * If not all have a hint, the hints are ignored (log error) -* If one has `structural`, check that all have it, (else throw error) +* None have both `termination_by` and `nontermination` (throw error) +* If one has `structural` or `partialFixpoint`, check that all have it (else throw error) * A `structural` should not have a `decreasing_by` (else log error) -/ @@ -171,21 +173,26 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do let preDefsWithout := preDefs.filter (·.termination.terminationBy?.isNone) let structural := preDefWith.termination.terminationBy? matches some {structural := true, ..} + let partialFixpoint := preDefWith.termination.partialFixpoint?.isSome for preDef in preDefs do if let .some termBy := preDef.termination.terminationBy? then - if !structural && !preDefsWithout.isEmpty then + if let .some partialFixpointStx := preDef.termination.partialFixpoint? then + throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \ + be both terminating and a partial fixpoint" + + if !structural && !partialFixpoint && !preDefsWithout.isEmpty then let m := MessageData.andList (preDefsWithout.toList.map (m!"{·.declName}")) let doOrDoes := if preDefsWithout.size = 1 then "does" else "do" logErrorAt termBy.ref (m!"incomplete set of `termination_by` annotations:\n"++ - m!"This function is mutually with {m}, which {doOrDoes} not have " ++ + m!"This function is mutually recursive with {m}, which {doOrDoes} not have " ++ m!"a `termination_by` clause.\n" ++ m!"The present clause is ignored.") - if structural && ! termBy.structural then + if structural && !termBy.structural then throwErrorAt termBy.ref (m!"Invalid `termination_by`; this function is mutually " ++ m!"recursive with {preDefWith.declName}, which is marked as `termination_by " ++ m!"structural` so this one also needs to be marked `structural`.") - if ! structural && termBy.structural then + if !structural && termBy.structural then throwErrorAt termBy.ref (m!"Invalid `termination_by`; this function is mutually " ++ m!"recursive with {preDefWith.declName}, which is not marked as `structural` " ++ m!"so this one cannot be `structural` either.") @@ -194,6 +201,23 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do logErrorAt decr.ref (m!"Invalid `decreasing_by`; this function is marked as " ++ m!"structurally recursive, so no explicit termination proof is needed.") + if partialFixpoint && preDef.termination.partialFixpoint?.isNone then + throwErrorAt preDef.ref (m!"Invalid `termination_by`; this function is mutually " ++ + m!"recursive with {preDefWith.declName}, which is marked as " ++ + m!"`nontermination_partialFixpointursive` so this one also needs to be marked " ++ + m!"`nontermination_partialFixpointursive`.") + + if preDef.termination.partialFixpoint?.isSome then + if let .some decr := preDef.termination.decreasingBy? then + logErrorAt decr.ref (m!"Invalid `decreasing_by`; this function is marked as " ++ + m!"nonterminating, so no explicit termination proof is needed.") + + if !partialFixpoint then + if let some stx := preDef.termination.partialFixpoint? then + throwErrorAt stx.ref (m!"Invalid `termination_by`; this function is mutually " ++ + m!"recursive with {preDefWith.declName}, which is not also marked as " ++ + m!"`nontermination_partialFixpointursive`, so this one cannot be either.") + /-- Elaborates the `TerminationHint` in the clique to `TerminationArguments` -/ @@ -208,6 +232,10 @@ def shouldUseStructural (preDefs : Array PreDefinition) : Bool := preDefs.any fun preDef => preDef.termination.terminationBy? matches some {structural := true, ..} +def shouldUsepartialFixpoint (preDefs : Array PreDefinition) : Bool := + preDefs.any fun preDef => + preDef.termination.partialFixpoint?.isSome + def shouldUseWF (preDefs : Array PreDefinition) : Bool := preDefs.any fun preDef => preDef.termination.terminationBy? matches some {structural := false, ..} || @@ -254,6 +282,8 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC let termArg?s ← elabTerminationByHints preDefs if shouldUseStructural preDefs then structuralRecursion preDefs termArg?s + else if shouldUsepartialFixpoint preDefs then + partialFixpoint preDefs else if shouldUseWF preDefs then wfRecursion preDefs termArg?s else diff --git a/src/Lean/Elab/PreDefinition/Mutual.lean b/src/Lean/Elab/PreDefinition/Mutual.lean new file mode 100644 index 0000000000..8b1f33c699 --- /dev/null +++ b/src/Lean/Elab/PreDefinition/Mutual.lean @@ -0,0 +1,92 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Joachim Breitner +-/ +prelude +import Lean.Elab.PreDefinition.Basic + +/-! +This module contains code common to mutual-via-fixedpoint constructions, i.e. +well-founded recursion and partial fixed-points, but independent of the details of the mutual packing. +-/ + +namespace Lean.Elab.Mutual +open Meta + +partial def withCommonTelescope (preDefs : Array PreDefinition) (k : Array Expr → Array Expr → MetaM α) : MetaM α := + go #[] (preDefs.map (·.value)) +where + go (fvars : Array Expr) (vals : Array Expr) : MetaM α := do + if !(vals.all fun val => val.isLambda) then + k fvars vals + else if !(← vals.allM fun val => isDefEq val.bindingDomain! vals[0]!.bindingDomain!) then + k fvars vals + else + withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x => + go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x) + +def getFixedPrefix (preDefs : Array PreDefinition) : MetaM Nat := + withCommonTelescope preDefs fun xs vals => do + let resultRef ← IO.mkRef xs.size + for val in vals do + if (← resultRef.get) == 0 then return 0 + forEachExpr' val fun e => do + if preDefs.any fun preDef => e.isAppOf preDef.declName then + let args := e.getAppArgs + resultRef.modify (min args.size ·) + for arg in args, x in xs do + if !(← withoutProofIrrelevance <| withReducible <| isDefEq arg x) then + -- We continue searching if e's arguments are not a prefix of `xs` + return true + return false + else + return true + resultRef.get + +def addPreDefsFromUnary (preDefs : Array PreDefinition) (preDefsNonrec : Array PreDefinition) + (unaryPreDefNonRec : PreDefinition) : TermElabM Unit := do + /- + We must remove `implemented_by` attributes from the auxiliary application because + this attribute is only relevant for code that is compiled. Moreover, the `[implemented_by ]` + attribute would check whether the `unaryPreDef` type matches with ``'s type, and produce + and error. See issue #2899 + -/ + let preDefNonRec := unaryPreDefNonRec.filterAttrs fun attr => attr.name != `implemented_by + let declNames := preDefs.toList.map (·.declName) + + -- Do not complain if the user sets @[semireducible], which usually is a noop, + -- we recognize that below and then do not set @[irreducible] + withOptions (allowUnsafeReducibility.set · true) do + if unaryPreDefNonRec.declName = preDefs[0]!.declName then + addNonRec preDefNonRec (applyAttrAfterCompilation := false) + else + withEnableInfoTree false do + addNonRec preDefNonRec (applyAttrAfterCompilation := false) + preDefsNonrec.forM (addNonRec · (applyAttrAfterCompilation := false) (all := declNames)) + +/-- +Cleans the right-hand-sides of the predefinitions, to prepare for inclusion in the EqnInfos: + * Remove RecAppSyntax markers + * Abstracts nested proofs (and for that, add the `_unsafe_rec` definitions) +-/ +def cleanPreDefs (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) := do + addAndCompilePartialRec preDefs + let preDefs ← preDefs.mapM (eraseRecAppSyntax ·) + let preDefs ← preDefs.mapM (abstractNestedProofs ·) + return preDefs + +/-- +Assign final attributes to the definitions. Assumes the EqnInfos to be already present. +-/ +def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do + for preDef in preDefs do + markAsRecursive preDef.declName + generateEagerEqns preDef.declName + applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation + -- Unless the user asks for something else, mark the definition as irreducible + unless preDef.modifiers.attrs.any fun a => + a.name = `reducible || a.name = `semireducible do + setIrreducibleAttribute preDef.declName + +end Lean.Elab.Mutual diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint.lean new file mode 100644 index 0000000000..8d8a3e7358 --- /dev/null +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ +prelude +import Lean.Elab.PreDefinition.PartialFixpoint.Eqns +import Lean.Elab.PreDefinition.PartialFixpoint.Main +import Lean.Elab.PreDefinition.PartialFixpoint.Induction diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean new file mode 100644 index 0000000000..32b0790b6a --- /dev/null +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean @@ -0,0 +1,117 @@ +/- +Copyright (c) 2022 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Lean.Elab.Tactic.Conv +import Lean.Meta.Tactic.Rewrite +import Lean.Meta.Tactic.Split +import Lean.Elab.PreDefinition.Basic +import Lean.Elab.PreDefinition.Eqns +import Lean.Meta.ArgsPacker.Basic +import Init.Data.Array.Basic +import Init.Internal.Order.Basic + +namespace Lean.Elab.PartialFixpoint +open Meta +open Eqns + +structure EqnInfo extends EqnInfoCore where + declNames : Array Name + declNameNonRec : Name + fixedPrefixSize : Nat + deriving Inhabited + +private def deltaLHSUntilFix (declName declNameNonRec : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do + let target ← mvarId.getType' + let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected" + let lhs' ← deltaExpand lhs fun n => n == declName || n == declNameNonRec + mvarId.replaceTargetDefEq (← mkEq lhs' rhs) + +partial def rwFixUnder (lhs : Expr) : MetaM Expr := do + if lhs.isAppOfArity ``Order.fix 4 then + return mkAppN (mkConst ``Order.fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs + else if lhs.isApp then + let h ← rwFixUnder lhs.appFn! + mkAppM ``congrFun #[h, lhs.appArg!] + else if lhs.isProj then + let f := mkLambda `p .default (← inferType lhs.projExpr!) (lhs.updateProj! (.bvar 0)) + let h ← rwFixUnder lhs.projExpr! + mkAppM ``congrArg #[f, h] + else + throwError "rwFixUnder: unexpected expression {lhs}" + +private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do + let mut mvarId := mvarId + let target ← mvarId.getType' + let some (_, lhs, rhs) := target.eq? | unreachable! + let h ← rwFixUnder lhs + let some (_, _, lhsNew) := (← inferType h).eq? | unreachable! + let targetNew ← mkEq lhsNew rhs + let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew + mvarId.assign (← mkEqTrans h mvarNew) + return mvarNew.mvarId! + +private partial def mkProof (declName : Name) (declNameNonRec : Name) (type : Expr) : MetaM Expr := do + trace[Elab.definition.partialFixpoint] "proving: {type}" + withNewMCtxDepth do + let main ← mkFreshExprSyntheticOpaqueMVar type + let (_, mvarId) ← main.mvarId!.intros + let mvarId ← deltaLHSUntilFix declName declNameNonRec mvarId + let mvarId ← rwFixEq mvarId + if ← withAtLeastTransparency .all (tryURefl mvarId) then + instantiateMVars main + else + throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}" + +def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) := + withOptions (tactic.hygienic.set · false) do + let baseName := declName + let eqnTypes ← withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do + let us := info.levelParams.map mkLevelParam + let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body + let goal ← mkFreshExprSyntheticOpaqueMVar target + withReducible do + mkEqnTypes info.declNames goal.mvarId! + let mut thmNames := #[] + for h : i in [: eqnTypes.size] do + let type := eqnTypes[i] + trace[Elab.definition.partialFixpoint] "{eqnTypes[i]}" + let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1) + thmNames := thmNames.push name + let value ← mkProof declName info.declNameNonRec type + let (type, value) ← removeUnusedEqnHypotheses type value + addDecl <| Declaration.thmDecl { + name, type, value + levelParams := info.levelParams + } + return thmNames + +builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension + +def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : MetaM Unit := do + preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName + unless preDefs.all fun p => p.kind.isTheorem do + unless (← preDefs.allM fun p => isProp p.type) do + let declNames := preDefs.map (·.declName) + modifyEnv fun env => + preDefs.foldl (init := env) fun env preDef => + eqnInfoExt.insert env preDef.declName { preDef with + declNames, declNameNonRec, fixedPrefixSize } + +def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do + if let some info := eqnInfoExt.find? (← getEnv) declName then + mkEqns declName info + else + return none + +def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do + let env ← getEnv + Eqns.getUnfoldFor? declName fun _ => eqnInfoExt.find? env declName |>.map (·.toEqnInfoCore) + +builtin_initialize + registerGetEqnsFn getEqnsFor? + registerGetUnfoldEqnFn getUnfoldFor? + +end Lean.Elab.PartialFixpoint diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean new file mode 100644 index 0000000000..a4cd82a705 --- /dev/null +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean @@ -0,0 +1,292 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ + +prelude +import Lean.Meta.Basic +import Lean.Meta.Match.MatcherApp.Transform +import Lean.Meta.Check +import Lean.Meta.Tactic.Subst +import Lean.Meta.Injective -- for elimOptParam +import Lean.Meta.ArgsPacker +import Lean.Meta.PProdN +import Lean.Meta.Tactic.Apply +import Lean.Elab.PreDefinition.PartialFixpoint.Eqns +import Lean.Elab.Command +import Lean.Meta.Tactic.ElimInfo + +namespace Lean.Elab.PartialFixpoint + +open Lean Elab Meta + +open Lean.Order + +def mkAdmAnd (α instα adm₁ adm₂ : Expr) : MetaM Expr := + mkAppOptM ``admissible_and #[α, instα, none, none, adm₁, adm₂] + +partial def mkAdmProj (packedInst : Expr) (i : Nat) (e : Expr) : MetaM Expr := do + if let some inst ← whnfUntil packedInst ``instCCPOPProd then + let_expr instCCPOPProd α β instα instβ := inst | throwError "mkAdmProj: unexpected instance {inst}" + if i == 0 then + mkAppOptM ``admissible_pprod_fst #[α, β, instα, instβ, none, e] + else + let e ← mkAdmProj instβ (i - 1) e + mkAppOptM ``admissible_pprod_snd #[α, β, instα, instβ, none, e] + else + assert! i == 0 + return e + +def CCPOProdProjs (n : Nat) (inst : Expr) : Array Expr := Id.run do + let mut insts := #[inst] + while insts.size < n do + let inst := insts.back! + let_expr Lean.Order.instCCPOPProd _ _ inst₁ inst₂ := inst + | panic! s!"isOptionFixpoint: unexpected CCPO instance {inst}" + insts := insts.pop + insts := insts.push inst₁ + insts := insts.push inst₂ + return insts + + +/-- `maskArray mask xs` keeps those `x` where the corresponding entry in `mask` is `true` -/ +-- Worth having in the standard libray? +private def maskArray {α} (mask : Array Bool) (xs : Array α) : Array α := Id.run do + let mut ys := #[] + for b in mask, x in xs do + if b then ys := ys.push x + return ys + +/-- Appends `_1` etc to `base` unless `n == 1` -/ +private def numberNames (n : Nat) (base : String) : Array Name := + .ofFn (n := n) fun ⟨i, _⟩ => + if n == 1 then .mkSimple base else .mkSimple s!"{base}_{i+1}" + +def deriveInduction (name : Name) : MetaM Unit := do + mapError (f := (m!"Cannot derive fixpoint induction principle (please report this issue)\n{indentD ·}")) do + let some eqnInfo := eqnInfoExt.find? (← getEnv) name | + throwError "{name} is not defined by partial_fixpoint" + + let infos ← eqnInfo.declNames.mapM getConstInfoDefn + -- First open up the fixed parameters everywhere + let e' ← lambdaBoundedTelescope infos[0]!.value eqnInfo.fixedPrefixSize fun xs _ => do + -- Now look at the body of an arbitrary of the functions (they are essentially the same + -- up to the final projections) + let body ← instantiateLambda infos[0]!.value xs + + -- The body should now be of the form of the form (fix … ).2.2.1 + -- We strip the projections (if present) + let body' := PProdN.stripProjs body + let some fixApp ← whnfUntil body' ``fix + | throwError "Unexpected function body {body}" + let_expr fix α instCCPOα F hmono := fixApp + | throwError "Unexpected function body {body'}" + + let instCCPOs := CCPOProdProjs infos.size instCCPOα + let types ← infos.mapM (instantiateForall ·.type xs) + let packedType ← PProdN.pack 0 types + let motiveTypes ← types.mapM (mkArrow · (.sort 0)) + let motiveNames := numberNames motiveTypes.size "motive" + withLocalDeclsDND (motiveNames.zip motiveTypes) fun motives => do + let packedMotive ← + withLocalDeclD (← mkFreshUserName `x) packedType fun x => do + mkLambdaFVars #[x] <| ← PProdN.pack 0 <| + motives.mapIdx fun idx motive => + mkApp motive (PProdN.proj motives.size idx packedType x) + + let admTypes ← motives.mapIdxM fun i motive => do + mkAppOptM ``admissible #[types[i]!, instCCPOs[i]!, some motive] + let admNames := numberNames admTypes.size "adm" + withLocalDeclsDND (admNames.zip admTypes) fun adms => do + let adms' ← adms.mapIdxM fun i adm => mkAdmProj instCCPOα i adm + let packedAdm ← PProdN.genMk (mkAdmAnd α instCCPOα) adms' + let hNames := numberNames infos.size "h" + let hTypes_hmask : Array (Expr × Array Bool) ← infos.mapIdxM fun i _info => do + let approxNames := infos.map fun info => + match info.name with + | .str _ n => .mkSimple n + | _ => `f + withLocalDeclsDND (approxNames.zip types) fun approxs => do + let ihTypes := approxs.mapIdx fun j approx => mkApp motives[j]! approx + withLocalDeclsDND (ihTypes.map (⟨`ih, ·⟩)) fun ihs => do + let f ← PProdN.mk 0 approxs + let Ff := F.beta #[f] + let Ffi := PProdN.proj motives.size i packedType Ff + let t := mkApp motives[i]! Ffi + let t ← PProdN.reduceProjs t + let mask := approxs.map fun approx => t.containsFVar approx.fvarId! + let t ← mkForallFVars (maskArray mask approxs ++ maskArray mask ihs) t + pure (t, mask) + let (hTypes, masks) := hTypes_hmask.unzip + withLocalDeclsDND (hNames.zip hTypes) fun hs => do + let packedH ← + withLocalDeclD `approx packedType fun approx => + let packedIHType := packedMotive.beta #[approx] + withLocalDeclD `ih packedIHType fun ih => do + let approxs := PProdN.projs motives.size packedType approx + let ihs := PProdN.projs motives.size packedIHType ih + let e ← PProdN.mk 0 <| hs.mapIdx fun i h => + let mask := masks[i]! + mkAppN h (maskArray mask approxs ++ maskArray mask ihs) + mkLambdaFVars #[approx, ih] e + let e' ← mkAppOptM ``fix_induct #[α, instCCPOα, F, hmono, packedMotive, packedAdm, packedH] + -- Should be the type of e', but with the function definitions folded + let packedConclusion ← PProdN.pack 0 <| ← + motives.mapIdxM fun i motive => do + let f ← mkConstWithLevelParams infos[i]!.name + return mkApp motive (mkAppN f xs) + let e' ← mkExpectedTypeHint e' packedConclusion + let e' ← mkLambdaFVars hs e' + let e' ← mkLambdaFVars adms e' + let e' ← mkLambdaFVars motives e' + let e' ← mkLambdaFVars (binderInfoForMVars := .default) (usedOnly := true) xs e' + let e' ← instantiateMVars e' + trace[Elab.definition.partialFixpoint.induction] "complete body of fixpoint induction principle:{indentExpr e'}" + pure e' + + let eTyp ← inferType e' + let eTyp ← elimOptParam eTyp + -- logInfo m!"eTyp: {eTyp}" + let params := (collectLevelParams {} eTyp).params + -- Prune unused level parameters, preserving the original order + let us := infos[0]!.levelParams.filter (params.contains ·) + + let inductName := name ++ `fixpoint_induct + addDecl <| Declaration.thmDecl + { name := inductName, levelParams := us, type := eTyp, value := e' } + +def isInductName (env : Environment) (name : Name) : Bool := Id.run do + let .str p s := name | return false + match s with + | "fixpoint_induct" => + if let some eqnInfo := eqnInfoExt.find? env p then + return p == eqnInfo.declNames[0]! + return false + | _ => return false + +builtin_initialize + registerReservedNamePredicate isInductName + + registerReservedNameAction fun name => do + if isInductName (← getEnv) name then + let .str p _ := name | return false + MetaM.run' <| deriveInduction p + return true + return false + +/-- +Returns true if `name` defined by `partial_fixpoint`, the first in its mutual group, +and all functions are defined using the `CCPO` instance for `Option`. +-/ +def isOptionFixpoint (env : Environment) (name : Name) : Bool := Option.isSome do + let eqnInfo ← eqnInfoExt.find? env name + guard <| name == eqnInfo.declNames[0]! + let defnInfo ← env.find? eqnInfo.declNameNonRec + assert! defnInfo.hasValue + let mut value := defnInfo.value! + while value.isLambda do value := value.bindingBody! + let_expr Lean.Order.fix _ inst _ _ := value | panic! s!"isOptionFixpoint: unexpected value {value}" + let insts := CCPOProdProjs eqnInfo.declNames.size inst + insts.forM fun inst => do + let mut inst := inst + while inst.isAppOfArity ``instCCPOPi 3 do + guard inst.appArg!.isLambda + inst := inst.appArg!.bindingBody! + guard <| inst.isAppOfArity ``instCCPOOption 1 + +def isPartialCorrectnessName (env : Environment) (name : Name) : Bool := Id.run do + let .str p s := name | return false + unless s == "partial_correctness" do return false + return isOptionFixpoint env p + +/-- +Given `motive : α → β → γ → Prop`, construct a proof of +`admissible (fun f => ∀ x y r, f x y = r → motive x y r)` +-/ +def mkOptionAdm (motive : Expr) : MetaM Expr := do + let type ← inferType motive + forallTelescope type fun ysr _ => do + let P := mkAppN motive ysr + let ys := ysr.pop + let r := ysr.back! + let mut inst ← mkAppM ``Option.admissible_eq_some #[P, r] + inst ← mkLambdaFVars #[r] inst + inst ← mkAppOptM ``admissible_pi #[none, none, none, none, inst] + for y in ys.reverse do + inst ← mkLambdaFVars #[y] inst + inst ← mkAppOptM ``admissible_pi_apply #[none, none, none, none, inst] + pure inst + +def derivePartialCorrectness (name : Name) : MetaM Unit := do + let fixpointInductThm := name ++ `fixpoint_induct + unless (← getEnv).contains fixpointInductThm do + deriveInduction name + + mapError (f := (m!"Cannot derive partial correctness theorem (please report this issue)\n{indentD ·}")) do + let some eqnInfo := eqnInfoExt.find? (← getEnv) name | + throwError "{name} is not defined by partial_fixpoint" + + let infos ← eqnInfo.declNames.mapM getConstInfoDefn + -- First open up the fixed parameters everywhere + let e' ← lambdaBoundedTelescope infos[0]!.value eqnInfo.fixedPrefixSize fun xs _ => do + let types ← infos.mapM (instantiateForall ·.type xs) + + -- for `f : α → β → Option γ`, we expect a `motive : α → β → γ → Prop` + let motiveTypes ← types.mapM fun type => + forallTelescopeReducing type fun ys type => do + let type ← whnf type + let_expr Option γ := type | throwError "Expected `Option`, got:{indentExpr type}" + withLocalDeclD (← mkFreshUserName `r) γ fun r => + mkForallFVars (ys.push r) (.sort 0) + let motiveDecls ← motiveTypes.mapIdxM fun i motiveType => do + let n := if infos.size = 1 then .mkSimple "motive" + else .mkSimple s!"motive_{i+1}" + pure (n, fun _ => pure motiveType) + withLocalDeclsD motiveDecls fun motives => do + -- the motives, as expected by `f.fixpoint_induct`: + -- fun f => ∀ x y r, f x y = some r → motive x y r + let motives' ← motives.mapIdxM fun i motive => do + withLocalDeclD (← mkFreshUserName `f) types[i]! fun f => do + forallTelescope (← inferType motive) fun ysr _ => do + let ys := ysr.pop + let r := ysr.back! + let heq ← mkEq (mkAppN f ys) (← mkAppM ``some #[r]) + let motive' ← mkArrow heq (mkAppN motive ysr) + let motive' ← mkForallFVars ysr motive' + mkLambdaFVars #[f] motive' + + let e' ← mkAppOptM fixpointInductThm <| (xs ++ motives').map some + let adms ← motives.mapM mkOptionAdm + let e' := mkAppN e' adms + let e' ← mkLambdaFVars motives e' + let e' ← mkLambdaFVars (binderInfoForMVars := .default) (usedOnly := true) xs e' + let e' ← instantiateMVars e' + trace[Elab.definition.partialFixpoint.induction] "complete body of partial correctness principle:{indentExpr e'}" + pure e' + + let eTyp ← inferType e' + let eTyp ← elimOptParam eTyp + let eTyp ← Core.betaReduce eTyp + -- logInfo m!"eTyp: {eTyp}" + let params := (collectLevelParams {} eTyp).params + -- Prune unused level parameters, preserving the original order + let us := infos[0]!.levelParams.filter (params.contains ·) + + let inductName := name ++ `partial_correctness + addDecl <| Declaration.thmDecl + { name := inductName, levelParams := us, type := eTyp, value := e' } + +builtin_initialize + registerReservedNamePredicate isPartialCorrectnessName + + registerReservedNameAction fun name => do + let .str p s := name | return false + unless s == "partial_correctness" do return false + unless isOptionFixpoint (← getEnv) p do return false + MetaM.run' <| derivePartialCorrectness p + return false + +end Lean.Elab.PartialFixpoint + +builtin_initialize Lean.registerTraceClass `Elab.definition.partialFixpoint.induction diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean new file mode 100644 index 0000000000..155828f34d --- /dev/null +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean @@ -0,0 +1,188 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ +prelude +import Lean.Elab.PreDefinition.MkInhabitant +import Lean.Elab.PreDefinition.Mutual +import Lean.Elab.PreDefinition.PartialFixpoint.Eqns +import Lean.Elab.Tactic.Monotonicity +import Init.Internal.Order.Basic +import Lean.Meta.PProdN + +namespace Lean.Elab + +open Meta +open Monotonicity + +open Lean.Order + +private def replaceRecApps (recFnNames : Array Name) (fixedPrefixSize : Nat) (f : Expr) (e : Expr) : MetaM Expr := do + let t ← inferType f + return e.replace fun e => + if let some idx := recFnNames.findIdx? (e.isAppOfArity · fixedPrefixSize) then + some <| PProdN.proj recFnNames.size idx t f + else + none + +/-- +For pretty error messages: +Takes `F : (fun f => e)`, where `f` is the packed function, and replaces `f` in `e` with the user-visible +constants, which are added to the environment temporarily. +-/ +private def unReplaceRecApps {α} (preDefs : Array PreDefinition) (fixedArgs : Array Expr) + (F : Expr) (k : Expr → MetaM α) : MetaM α := do + unless F.isLambda do throwError "Expected lambda:{indentExpr F}" + withoutModifyingEnv do + preDefs.forM addAsAxiom + let fns := preDefs.map fun d => + mkAppN (.const d.declName (d.levelParams.map mkLevelParam)) fixedArgs + let packedFn ← PProdN.mk 0 fns + let e ← lambdaBoundedTelescope F 1 fun f e => do + let f := f[0]! + -- Replace f with calls to the constants + let e := e.replace fun e => do if e == f then return packedFn else none + -- And reduce projection redexes + let e ← PProdN.reduceProjs e + pure e + k e + +def mkInstCCPOPProd (inst₁ inst₂ : Expr) : MetaM Expr := do + mkAppOptM ``instCCPOPProd #[none, none, inst₁, inst₂] + +def mkMonoPProd (hmono₁ hmono₂ : Expr) : MetaM Expr := do + -- mkAppM does not support the equivalent of (cfg := { synthAssignedInstances := false}), + -- so this is a bit more pedestrian + let_expr monotone _ inst _ inst₁ _ := (← inferType hmono₁) + | throwError "mkMonoPProd: unexpected type of{indentExpr hmono₁}" + let_expr monotone _ _ _ inst₂ _ := (← inferType hmono₂) + | throwError "mkMonoPProd: unexpected type of{indentExpr hmono₂}" + mkAppOptM ``PProd.monotone_mk #[none, none, none, inst₁, inst₂, inst, none, none, hmono₁, hmono₂] + +def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do + -- We expect all functions in the clique to have `partial_fixpoint` syntax + let hints := preDefs.filterMap (·.termination.partialFixpoint?) + assert! preDefs.size = hints.size + -- For every function of type `∀ x y, r x y`, an CCPO instance + -- ∀ x y, CCPO (r x y), but crucially constructed using `instCCPOPi` + let ccpoInsts ← preDefs.mapIdxM fun i preDef => withRef hints[i]!.ref do + lambdaTelescope preDef.value fun xs _body => do + let type ← instantiateForall preDef.type xs + let inst ← + try + synthInstance (← mkAppM ``CCPO #[type]) + catch _ => + trace[Elab.definition.partialFixpoint] "No CCPO instance found for {preDef.declName}, trying inhabitation" + let msg := m!"failed to compile definition '{preDef.declName}' using `partial_fixpoint`" + let w ← mkInhabitantFor msg #[] preDef.type + let instNonempty ← mkAppM ``Nonempty.intro #[mkAppN w xs] + let classicalWitness ← mkAppOptM ``Classical.ofNonempty #[none, instNonempty] + mkAppOptM ``FlatOrder.instCCPO #[none, classicalWitness] + mkLambdaFVars xs inst + + let fixedPrefixSize ← Mutual.getFixedPrefix preDefs + trace[Elab.definition.partialFixpoint] "fixed prefix size: {fixedPrefixSize}" + + let declNames := preDefs.map (·.declName) + + forallBoundedTelescope preDefs[0]!.type fixedPrefixSize fun fixedArgs _ => do + -- ∀ x y, CCPO (rᵢ x y) + let ccpoInsts := ccpoInsts.map (·.beta fixedArgs) + let types ← preDefs.mapM (instantiateForall ·.type fixedArgs) + + -- (∀ x y, r₁ x y) ×' (∀ x y, r₂ x y) + let packedType ← PProdN.pack 0 types + + -- CCPO (∀ x y, rᵢ x y) + let ccpoInsts' ← ccpoInsts.mapM fun inst => + lambdaTelescope inst fun xs inst => do + let mut inst := inst + for x in xs.reverse do + inst ← mkAppOptM ``instCCPOPi #[(← inferType x), none, (← mkLambdaFVars #[x] inst)] + pure inst + -- CCPO ((∀ x y, r₁ x y) ×' (∀ x y, r₂ x y)) + let packedCCPOInst ← PProdN.genMk mkInstCCPOPProd ccpoInsts' + -- Order ((∀ x y, r₁ x y) ×' (∀ x y, r₂ x y)) + let packedPartialOrderInst ← mkAppOptM ``CCPO.toPartialOrder #[none, packedCCPOInst] + + -- Error reporting hook, presenting monotonicity errors in terms of recursive functions + let failK {α} f (monoThms : Array Name) : MetaM α := do + unReplaceRecApps preDefs fixedArgs f fun t => do + let extraMsg := if monoThms.isEmpty then m!"" else + m!"Tried to apply {.andList (monoThms.toList.map (m!"'{.ofConstName ·}'"))}, but failed.\n\ + Possible cause: A missing `{.ofConstName ``MonoBind}` instance.\n\ + Use `set_option trace.Elab.Tactic.partial_monotonicity true` to debug." + if let some recApp := t.find? hasRecAppSyntax then + let some syn := getRecAppSyntax? recApp | panic! "getRecAppSyntax? failed" + withRef syn <| + throwError "Cannot eliminate recursive call `{syn}` enclosed in{indentExpr t}\n{extraMsg}" + else + throwError "Cannot eliminate recursive call in{indentExpr t}\n{extraMsg}" + + -- Adjust the body of each function to take the other functions as a + -- (packed) parameter + let Fs ← preDefs.mapM fun preDef => do + let body ← instantiateLambda preDef.value fixedArgs + withLocalDeclD (← mkFreshUserName `f) packedType fun f => do + let body' ← withoutModifyingEnv do + -- replaceRecApps needs the constants in the env to typecheck things + preDefs.forM (addAsAxiom ·) + replaceRecApps declNames fixedPrefixSize f body + mkLambdaFVars #[f] body' + + -- Construct and solve monotonicity goals for each function separately + -- This way we preserve the user's parameter names as much as possible + -- and can (later) use the user-specified per-function tactic + let hmonos ← preDefs.mapIdxM fun i preDef => do + let type := types[i]! + let F := Fs[i]! + let inst ← mkAppOptM ``CCPO.toPartialOrder #[type, ccpoInsts'[i]!] + let goal ← mkAppOptM ``monotone #[packedType, packedPartialOrderInst, type, inst, F] + if let some term := hints[i]!.term? then + let hmono ← Term.withSynthesize <| Term.elabTermEnsuringType term goal + let hmono ← instantiateMVars hmono + let mvars ← getMVars hmono + if mvars.isEmpty then + pure hmono + else + discard <| Term.logUnassignedUsingErrorInfos mvars + mkSorry goal (synthetic := true) + else + let hmono ← mkFreshExprSyntheticOpaqueMVar goal + mapError (f := (m!"Could not prove '{preDef.declName}' to be monotone in its recursive calls:{indentD ·}")) do + solveMono failK hmono.mvarId! + trace[Elab.definition.partialFixpoint] "monotonicity proof for {preDef.declName}: {hmono}" + instantiateMVars hmono + let hmono ← PProdN.genMk mkMonoPProd hmonos + + let packedValue ← mkAppOptM ``fix #[packedType, packedCCPOInst, none, hmono] + trace[Elab.definition.partialFixpoint] "packedValue: {packedValue}" + + let declName := + if preDefs.size = 1 then + preDefs[0]!.declName + else + preDefs[0]!.declName ++ `mutual + let packedType' ← mkForallFVars fixedArgs packedType + let packedValue' ← mkLambdaFVars fixedArgs packedValue + let preDefNonRec := { preDefs[0]! with + declName := declName + type := packedType' + value := packedValue'} + let preDefsNonrec ← preDefs.mapIdxM fun fidx preDef => do + let us := preDefNonRec.levelParams.map mkLevelParam + let value := mkConst preDefNonRec.declName us + let value := mkAppN value fixedArgs + let value := PProdN.proj preDefs.size fidx packedType value + let value ← mkLambdaFVars fixedArgs value + pure { preDef with value } + + Mutual.addPreDefsFromUnary preDefs preDefsNonrec preDefNonRec + let preDefs ← Mutual.cleanPreDefs preDefs + PartialFixpoint.registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize + Mutual.addPreDefAttributes preDefs + +end Lean.Elab + +builtin_initialize Lean.registerTraceClass `Elab.definition.partialFixpoint diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index d631e8307e..b82b16f713 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -294,7 +294,7 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp let brecOn := mkAppN brecOn packedFArgs let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.indexOf? fnIdx | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}" - let brecOn ← PProdN.proj size idx brecOn + let brecOn ← PProdN.projM size idx brecOn mkLambdaFVars ys (mkAppN brecOn otherArgs) end Lean.Elab.Structural diff --git a/src/Lean/Elab/PreDefinition/TerminationHint.lean b/src/Lean/Elab/PreDefinition/TerminationHint.lean index 9243c33494..47725cf9a7 100644 --- a/src/Lean/Elab/PreDefinition/TerminationHint.lean +++ b/src/Lean/Elab/PreDefinition/TerminationHint.lean @@ -15,7 +15,7 @@ namespace Lean.Elab /-- A single `termination_by` clause -/ structure TerminationBy where ref : Syntax - structural : Bool + structural : Bool vars : TSyntaxArray [`ident, ``Lean.Parser.Term.hole] body : Term /-- @@ -33,6 +33,12 @@ structure DecreasingBy where tactic : TSyntax ``Lean.Parser.Tactic.tacticSeq deriving Inhabited +/-- A single `partial_fixpoint` clause -/ +structure PartialFixpoint where + ref : Syntax + term? : Option Term + deriving Inhabited + /-- The termination annotations for a single function. For `decreasing_by`, we store the whole `decreasing_by tacticSeq` expression, as this @@ -42,6 +48,7 @@ structure TerminationHints where ref : Syntax terminationBy?? : Option Syntax terminationBy? : Option TerminationBy + partialFixpoint? : Option PartialFixpoint decreasingBy? : Option DecreasingBy /-- Here we record the number of parameters past the `:`. It is set by @@ -55,26 +62,29 @@ structure TerminationHints where extraParams : Nat deriving Inhabited -def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩ +def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, .none, 0⟩ /-- Logs warnings when the `TerminationHints` are unexpectedly present. -/ def TerminationHints.ensureNone (hints : TerminationHints) (reason : String) : CoreM Unit := do - match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with - | .none, .none, .none => pure () - | .none, .none, .some dec_by => + match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy?, hints.partialFixpoint? with + | .none, .none, .none, .none => pure () + | .none, .none, .some dec_by, .none => logWarningAt dec_by.ref m!"unused `decreasing_by`, function is {reason}" - | .some term_by?, .none, .none => + | .some term_by?, .none, .none, .none => logWarningAt term_by? m!"unused `termination_by?`, function is {reason}" - | .none, .some term_by, .none => + | .none, .some term_by, .none, .none => logWarningAt term_by.ref m!"unused `termination_by`, function is {reason}" - | _, _, _ => + | .none, .none, .none, .some partialFixpoint => + logWarningAt partialFixpoint.ref m!"unused `partial_fixpoint`, function is {reason}" + | _, _, _, _=> logWarningAt hints.ref m!"unused termination hints, function is {reason}" /-- True if any form of termination hint is present. -/ def TerminationHints.isNotNone (hints : TerminationHints) : Bool := hints.terminationBy??.isSome || hints.terminationBy?.isSome || - hints.decreasingBy?.isSome + hints.decreasingBy?.isSome || + hints.partialFixpoint?.isSome /-- Remembers `extraParams` for later use. Needs to happen early enough where we still know @@ -117,6 +127,8 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) : | _ => pure none else pure none let terminationBy? : Option TerminationBy ← if let some t := t? then match t with + | `(terminationBy|termination_by partialFixpointursion) => + pure (some {ref := t, structural := false, vars := #[], body := ⟨.missing⟩ : TerminationBy}) | `(terminationBy|termination_by $[structural%$s]? => $_body) => throwErrorAt t "no extra parameters bounds, please omit the `=>`" | `(terminationBy|termination_by $[structural%$s]? $vars* => $body) => @@ -124,12 +136,17 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) : | `(terminationBy|termination_by $[structural%$s]? $body:term) => pure (some {ref := t, structural := s.isSome, vars := #[], body}) | `(terminationBy?|termination_by?) => pure none + | `(partialFixpoint|partial_fixpoint $[monotonicity $_]?) => pure none | _ => throwErrorAt t "unexpected `termination_by` syntax" else pure none + let partialFixpoint? : Option PartialFixpoint ← if let some t := t? then match t with + | `(partialFixpoint|partial_fixpoint $[monotonicity $term?]?) => pure (some {ref := t, term?}) + | _ => pure none + else pure none let decreasingBy? ← d?.mapM fun d => match d with | `(decreasingBy|decreasing_by $tactic) => pure {ref := d, tactic} | _ => throwErrorAt d "unexpected `decreasing_by` syntax" - return { ref := stx, terminationBy??, terminationBy?, decreasingBy?, extraParams := 0 } + return { ref := stx, terminationBy??, terminationBy?, partialFixpoint?, decreasingBy?, extraParams := 0 } | _ => throwErrorAt stx s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}" end Lean.Elab diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 52e6239c32..43c17b93b5 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -10,6 +10,7 @@ import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Eqns import Lean.Meta.ArgsPacker.Basic import Init.Data.Array.Basic +import Init.Internal.Order.Basic namespace Lean.Elab.WF open Meta @@ -20,7 +21,6 @@ structure EqnInfo extends EqnInfoCore where declNameNonRec : Name fixedPrefixSize : Nat argsPacker : ArgsPacker - hasInduct : Bool deriving Inhabited private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do @@ -28,13 +28,23 @@ private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId. let some (_, lhs, _) := target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected" if lhs.isAppOf ``WellFounded.fix then return mvarId + else if lhs.isAppOf ``Order.fix then + return mvarId else deltaLHSUntilFix (← deltaLHS mvarId) private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do let target ← mvarId.getType' let some (_, lhs, rhs) := target.eq? | unreachable! - let h := mkAppN (mkConst ``WellFounded.fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs + let h ← + if lhs.isAppOf ``WellFounded.fix then + pure <| mkAppN (mkConst ``WellFounded.fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs + else if lhs.isAppOf ``Order.fix then + let x := lhs.getAppArgs.back! + let args := lhs.getAppArgs.pop + mkAppM ``congrFun #[mkAppN (mkConst ``Order.fix_eq lhs.getAppFn.constLevels!) args, x] + else + throwTacticEx `rwFixEq mvarId "expected fixed-point application" let some (_, _, lhsNew) := (← inferType h).eq? | unreachable! let targetNew ← mkEq lhsNew rhs let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew @@ -102,7 +112,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) := builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) - (argsPacker : ArgsPacker) (hasInduct : Bool) : MetaM Unit := do + (argsPacker : ArgsPacker) : MetaM Unit := do preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName /- See issue #2327. @@ -115,7 +125,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi modifyEnv fun env => preDefs.foldl (init := env) fun env preDef => eqnInfoExt.insert env preDef.declName { preDef with - declNames, declNameNonRec, fixedPrefixSize, argsPacker, hasInduct } + declNames, declNameNonRec, fixedPrefixSize, argsPacker } def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do if let some info := eqnInfoExt.find? (← getEnv) declName then diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean index c5f04e3c0e..ab5eede9a8 100644 --- a/src/Lean/Elab/PreDefinition/WF/Main.lean +++ b/src/Lean/Elab/PreDefinition/WF/Main.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura prelude import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.TerminationArgument +import Lean.Elab.PreDefinition.Mutual import Lean.Elab.PreDefinition.WF.PackMutual import Lean.Elab.PreDefinition.WF.Preprocess import Lean.Elab.PreDefinition.WF.Rel @@ -18,74 +19,6 @@ namespace Lean.Elab open WF open Meta -private partial def addNonRecPreDefs (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) : TermElabM Unit := do - let us := preDefNonRec.levelParams.map mkLevelParam - let all := preDefs.toList.map (·.declName) - for h : fidx in [:preDefs.size] do - let preDef := preDefs[fidx] - let value ← forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do - let value := mkAppN (mkConst preDefNonRec.declName us) xs - let value ← argsPacker.curryProj value fidx - mkLambdaFVars xs value - trace[Elab.definition.wf] "{preDef.declName} := {value}" - addNonRec { preDef with value } (applyAttrAfterCompilation := false) (all := all) - -partial def withCommonTelescope (preDefs : Array PreDefinition) (k : Array Expr → Array Expr → TermElabM α) : TermElabM α := - go #[] (preDefs.map (·.value)) -where - go (fvars : Array Expr) (vals : Array Expr) : TermElabM α := do - if !(vals.all fun val => val.isLambda) then - k fvars vals - else if !(← vals.allM fun val => isDefEq val.bindingDomain! vals[0]!.bindingDomain!) then - k fvars vals - else - withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x => - go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x) - -def getFixedPrefix (preDefs : Array PreDefinition) : TermElabM Nat := - withCommonTelescope preDefs fun xs vals => do - let resultRef ← IO.mkRef xs.size - for val in vals do - if (← resultRef.get) == 0 then return 0 - forEachExpr' val fun e => do - if preDefs.any fun preDef => e.isAppOf preDef.declName then - let args := e.getAppArgs - resultRef.modify (min args.size ·) - for arg in args, x in xs do - if !(← withoutProofIrrelevance <| withReducible <| isDefEq arg x) then - -- We continue searching if e's arguments are not a prefix of `xs` - return true - return false - else - return true - resultRef.get - -private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize : Nat) : MetaM Bool := do - if preDefs.size == 1 then - lambdaTelescope preDefs[0]!.value fun xs _ => return xs.size == fixedPrefixSize + 1 - else - return false - -/-- -Collect the names of the varying variables (after the fixed prefix); this also determines the -arity for the well-founded translations, and is turned into an `ArgsPacker`. -We use the term to determine the arity, but take the name from the type, for better names in the -``` -fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n -``` -idiom. --/ -def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name) := do - -- We take the arity from the term, but the names from the types - let arity ← lambdaTelescope preDef.value fun xs _ => return xs.size - assert! fixedPrefixSize ≤ arity - if arity = fixedPrefixSize then - throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments" - forallBoundedTelescope preDef.type arity fun xs _ => do - assert! xs.size = arity - let xs : Array Expr := xs[fixedPrefixSize:] - xs.mapM (·.fvarId!.getUserName) - def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do let termArgs? := termArg?s.mapM id -- Either all or none, checked by `elabTerminationByHints` let preDefs ← preDefs.mapM fun preDef => @@ -93,9 +26,12 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do for preDef in preDefs do addAsAxiom preDef - let fixedPrefixSize ← getFixedPrefix preDefs + let fixedPrefixSize ← Mutual.getFixedPrefix preDefs trace[Elab.definition.wf] "fixed prefix: {fixedPrefixSize}" let varNamess ← preDefs.mapM (varyingVarNames fixedPrefixSize ·) + for varNames in varNamess, preDef in preDefs do + if varNames.isEmpty then + throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments" let argsPacker := { varNamess } let preDefsDIte ← preDefs.mapM fun preDef => return { preDef with value := (← iteToDIte preDef.value) } return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsDIte) @@ -118,39 +54,14 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi eraseRecAppSyntaxExpr value /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/ let value ← unfoldDeclsFrom envNew value - let unaryPreDef := { unaryPreDef with value } - /- - We must remove `implemented_by` attributes from the auxiliary application because - this attribute is only relevant for code that is compiled. Moreover, the `[implemented_by ]` - attribute would check whether the `unaryPreDef` type matches with ``'s type, and produce - and error. See issue #2899 - -/ - let unaryPreDef := unaryPreDef.filterAttrs fun attr => attr.name != `implemented_by - return unaryPreDef + return { unaryPreDef with value } + trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}" - let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d - -- Do not complain if the user sets @[semireducible], which usually is a noop, - -- we recognize that below and then do not set @[irreducible] - withOptions (allowUnsafeReducibility.set · true) do - if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then - addNonRec preDefNonRec (applyAttrAfterCompilation := false) - else - withEnableInfoTree false do - addNonRec preDefNonRec (applyAttrAfterCompilation := false) - addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec - -- We create the `_unsafe_rec` before we abstract nested proofs. - -- Reason: the nested proofs may be referring to the _unsafe_rec. - addAndCompilePartialRec preDefs - let preDefs ← preDefs.mapM (abstractNestedProofs ·) - registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker (hasInduct := true) - for preDef in preDefs do - markAsRecursive preDef.declName - generateEagerEqns preDef.declName - applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation - -- Unless the user asks for something else, mark the definition as irreducible - unless preDef.modifiers.attrs.any fun a => - a.name = `reducible || a.name = `semireducible do - setIrreducibleAttribute preDef.declName + let preDefsNonrec ← preDefsFromUnaryNonRec fixedPrefixSize argsPacker preDefs preDefNonRec + Mutual.addPreDefsFromUnary preDefs preDefsNonrec preDefNonRec + let preDefs ← Mutual.cleanPreDefs preDefs + registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker + Mutual.addPreDefAttributes preDefs builtin_initialize registerTraceClass `Elab.definition.wf diff --git a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean index fbe6f442de..acc3daf507 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean +++ b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean @@ -1,11 +1,17 @@ /- Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, Joachim Breitner -/ prelude import Lean.Meta.ArgsPacker import Lean.Elab.PreDefinition.Basic +import Lean.Elab.PreDefinition.WF.Eqns + +/-! +This module contains roughly everything neede to turn mutual n-ary functions into a single unary +function, as used by well-founded recursion. +-/ namespace Lean.Elab.WF open Meta @@ -30,41 +36,49 @@ def withAppN (n : Nat) (e : Expr) (k : Array Expr → MetaM Expr) : MetaM Expr : mkLambdaFVars xs e' /-- -A `post` for `Meta.transform` to replace recursive calls to the original `preDefs` with calls -to the new unary function `newfn`. +Processes the expression and replaces calls to the `preDefs` with calls to `f`. -/ -private partial def post (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Name) - (domain : Expr) (newFn : Name) (e : Expr) : MetaM TransformStep := do - let f := e.getAppFn - if !f.isConst then +def packCalls (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Name) (newF : Expr) + (e : Expr) : MetaM Expr := do + let fType ← inferType newF + unless fType.isForall do + throwError "Not a forall: {newF} : {fType}" + let domain := fType.bindingDomain! + transform e (skipConstInApp := true) (post := fun e => do + let f := e.getAppFn + if !f.isConst then + return TransformStep.done e + if let some fidx := funNames.indexOf? f.constName! then + let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size + let e' ← withAppN arity e fun args => do + let packedArg ← argsPacker.pack domain fidx args[fixedPrefix:] + return mkApp newF packedArg + return TransformStep.done e' return TransformStep.done e - let declName := f.constName! - let us := f.constLevels! - if let some fidx := funNames.indexOf? declName then - let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size - let e' ← withAppN arity e fun args => do - let fixedArgs := args[:fixedPrefix] - let packedArg ← argsPacker.pack domain fidx args[fixedPrefix:] - return mkApp (mkAppN (mkConst newFn us) fixedArgs) packedArg - return TransformStep.done e' - return TransformStep.done e + ) + +def mutualName (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : Name := + if argsPacker.onlyOneUnary then + preDefs[0]!.declName + else + if argsPacker.numFuncs > 1 then + preDefs[0]!.declName ++ `_mutual + else + preDefs[0]!.declName ++ `_unary /-- Creates a single unary function from the given `preDefs`, using the machinery in the `ArgPacker` module. -/ def packMutual (fixedPrefix : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : MetaM PreDefinition := do - let arities := argsPacker.arities - if let #[1] := arities then return preDefs[0]! - let newFn := if argsPacker.numFuncs > 1 then preDefs[0]!.declName ++ `_mutual - else preDefs[0]!.declName ++ `_unary - -- Bring the fixed Prefix into scope + if argsPacker.onlyOneUnary then return preDefs[0]! + let newFn := mutualName argsPacker preDefs + -- Bring the fixed prefix into scope forallBoundedTelescope preDefs[0]!.type (some fixedPrefix) fun ys _ => do let types ← preDefs.mapM (instantiateForall ·.type ys) let vals ← preDefs.mapM (instantiateLambda ·.value ys) let type ← argsPacker.uncurryType types - let packedDomain := type.bindingDomain! -- Temporarily add the unary function as an axiom, so that all expressions -- are still type correct @@ -72,10 +86,44 @@ def packMutual (fixedPrefix : Nat) (argsPacker : ArgsPacker) (preDefs : Array Pr let preDefNew := { preDefs[0]! with declName := newFn, type } addAsAxiom preDefNew + let us := preDefs[0]!.levelParams.map mkLevelParam + let f := mkAppN (mkConst newFn us) ys + let value ← argsPacker.uncurry vals - let value ← transform value (skipConstInApp := true) - (post := post fixedPrefix argsPacker (preDefs.map (·.declName)) packedDomain newFn) + let value ← packCalls fixedPrefix argsPacker (preDefs.map (·.declName)) f value let value ← mkLambdaFVars ys value return { preDefNew with value } +/-- +Collect the names of the varying variables (after the fixed prefix); this also determines the +arity for the well-founded translations, and is turned into an `ArgsPacker`. +We use the term to determine the arity, but take the name from the type, for better names in the +``` +fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n +``` +idiom. +-/ +def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name) := do + -- We take the arity from the term, but the names from the types + let arity ← lambdaTelescope preDef.value fun xs _ => return xs.size + assert! fixedPrefixSize ≤ arity + forallBoundedTelescope preDef.type arity fun xs _ => do + assert! xs.size = arity + let xs : Array Expr := xs[fixedPrefixSize:] + xs.mapM (·.fvarId!.getUserName) + + +def preDefsFromUnaryNonRec (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) + (preDefs : Array PreDefinition) (unaryPreDefNonRec : PreDefinition) : MetaM (Array PreDefinition) := do + withoutModifyingEnv do + let us := unaryPreDefNonRec.levelParams.map mkLevelParam + addAsAxiom unaryPreDefNonRec + preDefs.mapIdxM fun fidx preDef => do + let value ← forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do + let value := mkAppN (mkConst unaryPreDefNonRec.declName us) xs + let value ← argsPacker.curryProj value fidx + mkLambdaFVars xs value + trace[Elab.definition.wf] "{preDef.declName} := {value}" + pure { preDef with value } + end Lean.Elab.WF diff --git a/src/Lean/Elab/Tactic/Monotonicity.lean b/src/Lean/Elab/Tactic/Monotonicity.lean index 50f02f63cb..6ccc0911e4 100644 --- a/src/Lean/Elab/Tactic/Monotonicity.lean +++ b/src/Lean/Elab/Tactic/Monotonicity.lean @@ -21,7 +21,6 @@ partial def headBetaUnderLambda (f : Expr) : Expr := Id.run do f := f.updateLambda! f.bindingInfo! f.bindingDomain! f.bindingBody!.headBeta return f - /-- Environment extensions for monotonicity lemmas -/ builtin_initialize monotoneExt : SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ← @@ -85,7 +84,7 @@ partial def solveMonoCall (α inst_α : Expr) (e : Expr) : MetaM (Option Expr) : let_expr monotone _ _ _ inst _ := hmonoType | throwError "solveMonoCall {e}: unexpected type {hmonoType}" let some inst ← whnfUntil inst ``instPartialOrderPProd | throwError "solveMonoCall {e}: unexpected instance {inst}" let_expr instPartialOrderPProd β γ inst_β inst_γ ← inst | throwError "solveMonoCall {e}: whnfUntil failed?{indentExpr inst}" - let n := if e.projIdx! == 0 then ``monotone_pprod_fst else ``monotone_pprod_snd + let n := if e.projIdx! == 0 then ``PProd.monotone_fst else ``PProd.monotone_snd return ← mkAppOptM n #[β, γ, α, inst_β, inst_γ, inst_α, none, hmono] if e == .bvar 0 then @@ -126,19 +125,25 @@ def solveMonoStep (failK : ∀ {α}, Expr → Array Name → MetaM α := @defaul goal.assign goal' return [goal'.mvarId!] - -- Float letE to the environment + -- Handle let if let .letE n t v b _nonDep := e then if t.hasLooseBVars || v.hasLooseBVars then - failK f #[] - let goal' ← withLetDecl n t v fun x => do - let b' := f.updateLambdaE! f.bindingDomain! (b.instantiate1 x) + -- We cannot float the let to the context, so just zeta-reduce. + let b' := f.updateLambdaE! f.bindingDomain! (b.instantiate1 v) let goal' ← mkFreshExprSyntheticOpaqueMVar (mkApp type.appFn! b') - goal.assign (← mkLetFVars #[x] goal') - pure goal' - return [goal'.mvarId!] + goal.assign goal' + return [goal'.mvarId!] + else + -- No recursive call in t or v, so float out + let goal' ← withLetDecl n t v fun x => do + let b' := f.updateLambdaE! f.bindingDomain! (b.instantiate1 x) + let goal' ← mkFreshExprSyntheticOpaqueMVar (mkApp type.appFn! b') + goal.assign (← mkLetFVars #[x] goal') + pure goal' + return [goal'.mvarId!] -- Float `letFun` to the environment. - -- `applyConst` tends to reduce the redex + -- (cannot use `applyConst`, it tends to reduce the let redex) match_expr e with | letFun γ _ v b => if γ.hasLooseBVars || v.hasLooseBVars then diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean index 4e2e32ab20..d6d84de667 100644 --- a/src/Lean/Meta/ArgsPacker.lean +++ b/src/Lean/Meta/ArgsPacker.lean @@ -56,6 +56,8 @@ Given a telescope of FVars of type `tᵢ`, iterates `PSigma` to produce the type `t₁ ⊗' t₂ …`. -/ def packType (xs : Array Expr) : MetaM Expr := do + if xs.isEmpty then + return mkConst ``Unit let mut d ← inferType xs.back! for x in xs.pop.reverse do d ← mkAppOptM ``PSigma #[some (← inferType x), some (← mkLambdaFVars #[x] d)] @@ -66,7 +68,11 @@ def packType (xs : Array Expr) : MetaM Expr := do Create a unary application by packing the given arguments using `PSigma.mk`. The `type` should be the expected type of the packed argument, as created with `packType`. -/ -partial def pack (type : Expr) (args : Array Expr) : Expr := go 0 type +partial def pack (type : Expr) (args : Array Expr) : Expr := + if args.isEmpty then + mkConst ``Unit.unit + else + go 0 type where go (i : Nat) (type : Expr) : Expr := if h : i < args.size - 1 then @@ -88,6 +94,7 @@ Unpacks a unary packed argument created with `Unary.pack`. Throws an error if the expression is not of that form. -/ def unpack (arity : Nat) (e : Expr) : Option (Array Expr) := do + if arity = 0 then return #[] let mut e := e let mut args := #[] while args.size + 1 < arity do @@ -105,6 +112,7 @@ def unpack (arity : Nat) (e : Expr) : Option (Array Expr) := do Example: `mkTupleElems a 4` returns `#[a.1, a.2.1, a.2.2.1, a.2.2.2]`. -/ private def mkTupleElems (t : Expr) (arity : Nat) : Array Expr := Id.run do + if arity = 0 then return #[] let mut result := #[] let mut t := t for _ in [:arity - 1] do @@ -117,14 +125,17 @@ Given a type `t` of the form `(x : A) → (y : B[x]) → … → (z : D[x,y]) returns the curried type `(x : A ⊗' B ⊗' … ⊗' D) → R[x.1, x.2.1, x.2.2]`. -/ def uncurryType (varNames : Array Name) (type : Expr) : MetaM Expr := do - forallBoundedTelescope type varNames.size fun xs _ => do - assert! xs.size = varNames.size - let d ← packType xs - let name := if xs.size == 1 then varNames[0]! else `_x - withLocalDeclD name d fun tuple => do - let elems := mkTupleElems tuple xs.size - let codomain ← instantiateForall type elems - mkForallFVars #[tuple] codomain + if varNames.isEmpty then + mkArrow (mkConst ``Unit) type + else + forallBoundedTelescope type varNames.size fun xs _ => do + assert! xs.size = varNames.size + let d ← packType xs + let name := if xs.size == 1 then varNames[0]! else `_x + withLocalDeclD name d fun tuple => do + let elems := mkTupleElems tuple xs.size + let codomain ← instantiateForall type elems + mkForallFVars #[tuple] codomain /-- Iterated `PSigma.casesOn`: @@ -154,21 +165,23 @@ Given expression `e` of type `(x : A) → (y : B[x]) → … → (z : D[x,y]) returns an expression of type `(x : A ⊗' B ⊗' … ⊗' D) → R[x.1, x.2.1, x.2.2]`. -/ def uncurry (varNames : Array Name) (e : Expr) : MetaM Expr := do - let type ← inferType e - let resultType ← uncurryType varNames type - forallBoundedTelescope resultType (some 1) fun xs codomain => do - let #[x] := xs | unreachable! - let u ← getLevel codomain - let value ← casesOn varNames.toList x u codomain e - mkLambdaFVars #[x] value + if varNames.isEmpty then + return mkLambda `x .default (mkConst ``Unit) e + else + let type ← inferType e + let resultType ← uncurryType varNames type + forallBoundedTelescope resultType (some 1) fun xs codomain => do + let #[x] := xs | unreachable! + let u ← getLevel codomain + let value ← casesOn varNames.toList x u codomain e + mkLambdaFVars #[x] value /-- Given `(A ⊗' B ⊗' … ⊗' D) → R` (non-dependent) `R`, return `A → B → … → D → R` -/ -private def curryType (varNames : Array Name) (type : Expr) : - MetaM Expr := do - let some (domain, codomain) := type.arrow? | - throwError "curryType: Expected arrow type, got {type}" - go codomain varNames.toList domain - where +private def curryType (varNames : Array Name) (type : Expr) : MetaM Expr := do + let some (domain, codomain) := type.arrow? | + throwError "curryType: Expected arrow type, got {type}" + go codomain varNames.toList domain +where go (codomain : Expr) : List Name → Expr → MetaM Expr | [], _ => pure codomain | [_], domain => mkArrow domain codomain @@ -184,6 +197,8 @@ Given expression `e` of type `(x : A ⊗' B ⊗' … ⊗' D) → R[x]` return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)]` -/ private partial def curry (varNames : Array Name) (e : Expr) : MetaM Expr := do + if varNames.isEmpty then + return e.beta #[mkConst ``Unit.unit] let type ← whnfForall (← inferType e) unless type.isForall do throwError "curryPSigma: expected forall type, got {type}" @@ -494,7 +509,9 @@ projects to the `i`th function of type, -/ def curryProj (argsPacker : ArgsPacker) (e : Expr) (i : Nat) : MetaM Expr := do let n := argsPacker.numFuncs - let t ← inferType e + let t ← whnf (← inferType e) + unless t.isForall do + panic! "curryProj: expected forall type, got {}" let packedDomain := t.bindingDomain! let unaryTypes ← Mutual.unpackType n packedDomain unless i < unaryTypes.length do diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 0da4e5fde1..2a99c1b726 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -1627,6 +1627,8 @@ def withLocalDeclNoLocalInstanceUpdate (name : Name) (bi : BinderInfo) (type : E - the binder info of the variable - a type constructor for the variable, where the array consists of all of the free variables defined prior to this one. This is needed because the type of the variable may depend on prior variables. + +See `withLocalDeclsD` and `withLocalDeclsDND` for simplier variants. -/ partial def withLocalDecls [Inhabited α] @@ -1642,10 +1644,21 @@ where else k acc +/-- +Variant of `withLocalDecls` using `Binderinfo.default` +-/ def withLocalDeclsD [Inhabited α] (declInfos : Array (Name × (Array Expr → n Expr))) (k : (xs : Array Expr) → n α) : n α := withLocalDecls (declInfos.map (fun (name, typeCtor) => (name, BinderInfo.default, typeCtor))) k +/-- +Simpler variant of `withLocalDeclsD` for brining variables into scope whose types do not depend +on each other. +-/ +def withLocalDeclsDND [Inhabited α] (declInfos : Array (Name × Expr)) (k : (xs : Array Expr) → n α) : n α := + withLocalDeclsD + (declInfos.map (fun (name, typeCtor) => (name, fun _ => pure typeCtor))) k + private def withNewBinderInfosImp (bs : Array (FVarId × BinderInfo)) (k : MetaM α) : MetaM α := do let lctx := bs.foldl (init := (← getLCtx)) fun lctx (fvarId, bi) => lctx.setBinderInfo fvarId bi diff --git a/src/Lean/Meta/Constructions/BRecOn.lean b/src/Lean/Meta/Constructions/BRecOn.lean index cd3c30375a..f950e3619c 100644 --- a/src/Lean/Meta/Constructions/BRecOn.lean +++ b/src/Lean/Meta/Constructions/BRecOn.lean @@ -17,8 +17,8 @@ open Meta private def etaPProd (xs : Array Expr) (e : Expr) : MetaM Expr := do if xs.isEmpty then return e let r := mkAppN e xs - let r₁ ← mkLambdaFVars xs (← mkPProdFst r) - let r₂ ← mkLambdaFVars xs (← mkPProdSnd r) + let r₁ ← mkLambdaFVars xs (← mkPProdFstM r) + let r₂ ← mkLambdaFVars xs (← mkPProdSndM r) mkPProdMk r₁ r₂ /-- @@ -328,7 +328,7 @@ private def mkBRecOnFromRec (recName : Name) (ind reflexive : Bool) (nParams : N val := mkAppN val indices val := mkApp val major -- project out first component - val ← mkPProdFst val + val ← mkPProdFstM val -- All parameters of `.rec` besides the `minors` become parameters of `.bRecOn`, and the `fs` let below_params := params ++ motives ++ indices ++ #[major] ++ fs diff --git a/src/Lean/Meta/PProdN.lean b/src/Lean/Meta/PProdN.lean index 985b3d6e90..9fe7cd5623 100644 --- a/src/Lean/Meta/PProdN.lean +++ b/src/Lean/Meta/PProdN.lean @@ -6,6 +6,7 @@ Authors: Joachim Breitner prelude import Lean.Meta.InferType +import Lean.Meta.Transform /-! This module provides functions to pack and unpack values using nested `PProd` or `And`, @@ -47,48 +48,81 @@ def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2 /-- `PProd.fst` or `And.left` (using `.proj`) -/ -def mkPProdFst (e : Expr) : MetaM Expr := do - let t ← whnf (← inferType e) +def mkPProdFst (t e : Expr) : Expr := match_expr t with - | PProd _ _ => return .proj ``PProd 0 e - | And _ _ => return .proj ``And 0 e - | _ => panic! "mkPProdFst: cannot handle{indentExpr e}\nof type{indentExpr t}" + | PProd _ _ => .proj ``PProd 0 e + | And _ _ => .proj ``And 0 e + | _ => panic! s!"mkPProdFst: cannot handle {e}\nof type {t}" + +/-- `PProd.fst` or `And.left` (using `.proj`), inferring the type of `e` -/ +def mkPProdFstM (e : Expr) : MetaM Expr := do + return mkPProdFst (← whnf (← inferType e)) e + +private def mkTypeSnd (t : Expr) : Expr := + match_expr t with + | PProd _ t => t + | And _ t => t + | _ => panic! s!"mkTypeSnd: cannot handle type {t}" /-- `PProd.snd` or `And.right` (using `.proj`) -/ -def mkPProdSnd (e : Expr) : MetaM Expr := do - let t ← whnf (← inferType e) +def mkPProdSnd (t e : Expr) : Expr := match_expr t with - | PProd _ _ => return .proj ``PProd 1 e - | And _ _ => return .proj ``And 1 e - | _ => panic! "mkPProdSnd: cannot handle{indentExpr e}\nof type{indentExpr t}" - + | PProd _ _ => .proj ``PProd 1 e + | And _ _ => .proj ``And 1 e + | _ => panic! s!"mkPProdSnd: cannot handle {e}\nof type {t}" +/-- `PProd.snd` or `And.right` (using `.proj`), inferring the type of `e` -/ +def mkPProdSndM (e : Expr) : MetaM Expr := do + return mkPProdSnd (← whnf (← inferType e)) e namespace PProdN +/-- +Essentially a form of `foldrM1`. Underlies `pack` and `mk`, and is useful to constuct proofs +that should follow the structure of `pack` and `mk` (e.g. admissibility proofs) +-/ +def genMk {α : Type _} [Inhabited α] (mk : α → α → MetaM α) (xs : Array α) : MetaM α := + assert! !xs.isEmpty + xs.pop.foldrM mk xs.back! + /-- Given types `tᵢ`, produces `t₁ ×' t₂ ×' t₃` -/ def pack (lvl : Level) (xs : Array Expr) : MetaM Expr := do if xs.size = 0 then if lvl matches .zero then return .const ``True [] else return .const ``PUnit [lvl] - let xBack := xs.back! - xs.pop.foldrM mkPProd xBack + genMk mkPProd xs /-- Given values `xᵢ` of type `tᵢ`, produces value of type `t₁ ×' t₂ ×' t₃` -/ def mk (lvl : Level) (xs : Array Expr) : MetaM Expr := do if xs.size = 0 then if lvl matches .zero then return .const ``True.intro [] else return .const ``PUnit.unit [lvl] - let xBack := xs.back! - xs.pop.foldrM mkPProdMk xBack + genMk mkPProdMk xs -/-- Given a value of type `t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ` -/ -def proj (n i : Nat) (e : Expr) : MetaM Expr := do +/-- Given a value `e` of type `t = t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ` -/ +def proj (n i : Nat) (t e : Expr) : Expr := Id.run <| do + unless i < n do panic! "PProdN.proj: {i} not less than {n}" + let mut t := t let mut value := e for _ in [:i] do - value ← mkPProdSnd value + value := mkPProdSnd t value + t := mkTypeSnd t if i+1 < n then - mkPProdFst value + mkPProdFst t value + else + value + +/-- Given a value `e` of type `t = t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return the values of type `tᵢ` -/ +def projs (n : Nat) (t e : Expr) : Array Expr := + Array.ofFn (n := n) fun i => PProdN.proj n i t e + +/-- Given a value of type `t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ` -/ +def projM (n i : Nat) (e : Expr) : MetaM Expr := do + let mut value := e + for _ in [:i] do + value ← mkPProdSndM value + if i+1 < n then + mkPProdFstM value else pure value @@ -140,6 +174,27 @@ def mkLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do mkLambdaFVars xs packed +/-- Strips topplevel `PProd` and `And` projections -/ +def stripProjs (e : Expr) : Expr := + match e with + | .proj ``PProd _ e' => stripProjs e' + | .proj ``And _ e' => stripProjs e' + | e => e + +/-- +Reduces `⟨x,y⟩.1` redexes for `PProd` and `And` +-/ +def reduceProjs (e : Expr) : CoreM Expr := do + Core.transform e (post := fun e => do + if e.isProj then + if e.projExpr!.isAppOfArity ``PProd.mk 4 || e.projExpr!.isAppOfArity ``And.intro 2 then + if e.projIdx! == 0 then + return .continue e.projExpr!.appFn!.appArg! + else + return .continue e.projExpr!.appArg! + return .continue + ) + end PProdN end Lean.Meta diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index d835602bd7..6cabf6eb1e 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/src/Lean/Meta/Tactic/FunInd.lean @@ -355,8 +355,8 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E pure <| .mdata m (← foldAndCollect oldIH newIH isRecCall b) -- These projections can be type changing (to And), so re-infer their type arguments - | .proj ``PProd 0 e => mkPProdFst (← foldAndCollect oldIH newIH isRecCall e) - | .proj ``PProd 1 e => mkPProdSnd (← foldAndCollect oldIH newIH isRecCall e) + | .proj ``PProd 0 e => mkPProdFstM (← foldAndCollect oldIH newIH isRecCall e) + | .proj ``PProd 1 e => mkPProdSndM (← foldAndCollect oldIH newIH isRecCall e) | .proj t i e => pure <| .proj t i (← foldAndCollect oldIH newIH isRecCall e) @@ -651,9 +651,9 @@ def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : M let (_, mvar) ← mvar.revert fvarIds pure mvar trace[Meta.FunInd] "abstractIndependentMVars, reverted mvars: {mvars}" - let decls := mvars.mapIdx fun i mvar => - (.mkSimple s!"case{i+1}", (fun _ => mvar.getType)) - Meta.withLocalDeclsD decls fun xs => do + let names := Array.ofFn (n := mvars.size) fun ⟨i,_⟩ => .mkSimple s!"case{i+1}" + let types ← mvars.mapM MVarId.getType + Meta.withLocalDeclsDND (names.zip types) fun xs => do for mvar in mvars, x in xs do mvar.assign x mkLambdaFVars xs (← instantiateMVars e) @@ -760,7 +760,7 @@ def projectMutualInduct (names : Array Name) (mutualInduct : Name) : MetaM Unit let value ← forallTelescope ci.type fun xs _body => do let value := .const ci.name (levelParams.map mkLevelParam) let value := mkAppN value xs - let value ← PProdN.proj names.size idx value + let value ← PProdN.projM names.size idx value mkLambdaFVars xs value let type ← inferType value addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value } @@ -876,12 +876,6 @@ def deriveUnpackedInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name): Met let unpackedInductName ← unpackMutualInduction eqnInfo unaryInductName projectMutualInduct eqnInfo.declNames unpackedInductName -def stripPProdProjs (e : Expr) : Expr := - match e with - | .proj ``PProd _ e' => stripPProdProjs e' - | .proj ``And _ e' => stripPProdProjs e' - | e => e - def withLetDecls {α} (name : Name) (ts : Array Expr) (es : Array Expr) (k : Array Expr → MetaM α) : MetaM α := do assert! es.size = ts.size go 0 #[] @@ -910,11 +904,11 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit -- The body is of the form (brecOn … ).2.2.1 extra1 extra2 etc; ignore the -- projection here let f' := body.getAppFn - let body' := stripPProdProjs f' + let body' := PProdN.stripProjs f' let f := body'.getAppFn let args := body'.getAppArgs ++ body.getAppArgs - let body := stripPProdProjs body + let body := PProdN.stripProjs body let .const brecOnName us := f | throwError "{infos[0]!.name}: unexpected body:{indentExpr infos[0]!.value}" unless isBRecOnRecursor (← getEnv) brecOnName do @@ -980,11 +974,9 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit mkForallFVars ys (.sort levelZero) let motiveArities ← infos.mapM fun info => do lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size - let motiveDecls ← motiveTypes.mapIdxM fun i motiveType => do - let n := if infos.size = 1 then .mkSimple "motive" - else .mkSimple s!"motive_{i+1}" - pure (n, fun _ => pure motiveType) - withLocalDeclsD motiveDecls fun motives => do + let motiveNames := Array.ofFn (n := infos.size) fun ⟨i, _⟩ => + if infos.size = 1 then .mkSimple "motive" else .mkSimple s!"motive_{i+1}" + withLocalDeclsDND (motiveNames.zip motiveTypes) fun motives => do -- Prepare the `isRecCall` that recognizes recursive calls let fns := infos.map fun info => @@ -1051,7 +1043,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit let e := mkAppN e packedMotives let e := mkAppN e indicesMajor let e := mkAppN e minors' - let e ← PProdN.proj pos.size packIdx e + let e ← PProdN.projM pos.size packIdx e let e := mkAppN e rest let e ← mkLambdaFVars ys e trace[Meta.FunInd] "assembled call for {info.name}: {e}" @@ -1112,15 +1104,11 @@ def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do match s with | "induct" => if let some eqnInfo := WF.eqnInfoExt.find? env p then - unless eqnInfo.hasInduct do - return false return true if (Structural.eqnInfoExt.find? env p).isSome then return true return false | "mutual_induct" => if let some eqnInfo := WF.eqnInfoExt.find? env p then - unless eqnInfo.hasInduct do - return false if h : eqnInfo.declNames.size > 1 then return eqnInfo.declNames[0] = p if let some eqnInfo := Structural.eqnInfoExt.find? env p then diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean index b6734f2157..fe0eb1a96c 100644 --- a/src/Lean/Meta/Tactic/SplitIf.lean +++ b/src/Lean/Meta/Tactic/SplitIf.lean @@ -189,6 +189,7 @@ def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Opti trace[Meta.Tactic.splitIf] "splitting on {decInst}" return some (← mvarId.byCasesDec cond decInst hName) else + trace[Meta.Tactic.splitIf] "could not find if to split:{indentExpr e}" return none end SplitIf diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index be6ef08944..fad0247f99 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -715,15 +715,41 @@ the inferrred termination argument will be suggested. -/ @[builtin_doc] def terminationBy := leading_parser - "termination_by " >> - optional (nonReservedSymbol "structural ") >> - optional (atomic (many (ppSpace >> Term.binderIdent) >> " => ")) >> - termParser + "termination_by " >> ( + (nonReservedSymbol "tailrecursion") <|> + (optional (nonReservedSymbol "structural ") >> + optional (atomic (many (ppSpace >> Term.binderIdent) >> " => ")) >> + termParser)) @[inherit_doc terminationBy, builtin_doc] def terminationBy? := leading_parser "termination_by?" +/-- +Defines a possibly non-terminating function as a fixed-point in a suitable partial order. + +Such a function is compiled as if it was marked `partial`, but its equations are provided as +theorems, so that it can be verified. + +In general it accepts functions whose return type has a `Lean.Order.CCPO` instance and whose +definition is `Lean.Order.monotone` with regard to its recursive calls. + +Common special cases are + +* Functions whose type is inhabited a-priori (as with `partial`), and where all recursive + calls are in tail-call position. +* Monadic in certain “monotone chain-complete monads” (in particular, `Option`) composed using + the bind operator and other supported monadic combinators. + +By default, the onotonicity proof is performed by the compositional `monotonicity` tactic. Using +the syntax `partial_fixpoint monotonicity by $tac` the proof can be done manually. +-/ +@[builtin_doc] def partialFixpoint := leading_parser + withPosition ( + "partial_fixpoint" >> + optional (checkColGt "indentation" >> nonReservedSymbol "monotonicity " >> + checkColGt "indented monotonicity proof" >> termParser)) + /-- Manually prove that the termination argument (as specified with `termination_by` or inferred) decreases at each recursive call. @@ -740,7 +766,7 @@ Forces the use of well-founded recursion and is hence incompatible with Termination hints are `termination_by` and `decreasing_by`, in that order. -/ @[builtin_doc] def suffix := leading_parser - optional (ppDedent ppLine >> (terminationBy? <|> terminationBy)) >> optional decreasingBy + optional (ppDedent ppLine >> (terminationBy? <|> terminationBy <|> partialFixpoint)) >> optional decreasingBy end Termination namespace Term diff --git a/tests/lean/partial_fixpoint_parseerrors.lean b/tests/lean/partial_fixpoint_parseerrors.lean new file mode 100644 index 0000000000..dedd673d64 --- /dev/null +++ b/tests/lean/partial_fixpoint_parseerrors.lean @@ -0,0 +1,17 @@ + +-- Check that indent is required + +def nullary1 (x : Nat) : Option Unit := nullary1 (x + 1) +partial_fixpoint monotonicity +fun _ _ a x => a (x + 1) + +def nullary2 (x : Nat) : Option Unit := nullary2 (x + 1) +partial_fixpoint +monotonicity fun _ _ a x => a (x + 1) + +-- This is allowed: + +def nullary3 (x : Nat) : Option Unit := nullary3 (x + 1) +partial_fixpoint + monotonicity + fun _ _ a x => a (x + 1) diff --git a/tests/lean/partial_fixpoint_parseerrors.lean.expected.out b/tests/lean/partial_fixpoint_parseerrors.lean.expected.out new file mode 100644 index 0000000000..45f5a5abac --- /dev/null +++ b/tests/lean/partial_fixpoint_parseerrors.lean.expected.out @@ -0,0 +1,2 @@ +partial_fixpoint_parseerrors.lean:6:0: error: expected indented monotonicity proof +partial_fixpoint_parseerrors.lean:10:0-10:12: error: unexpected identifier; expected command diff --git a/tests/lean/run/partial_fixpoint.lean b/tests/lean/run/partial_fixpoint.lean new file mode 100644 index 0000000000..765aed9202 --- /dev/null +++ b/tests/lean/run/partial_fixpoint.lean @@ -0,0 +1,401 @@ +def monadic (x : Nat) : Option Unit := monadic (x + 1) +partial_fixpoint + +def loop (x : Nat) : Unit := loop (x + 1) +partial_fixpoint + +def monadic0 : Option Unit := monadic0 +partial_fixpoint + +def loop0 : Unit := loop0 +partial_fixpoint + + +/-- +info: equations: +theorem loop.eq_1 : ∀ (x : Nat), loop x = loop (x + 1) +-/ +#guard_msgs in +#print equations loop + +/-- error: unknown constant 'loop.induct' -/ +#guard_msgs in +#check loop.induct + +def find (P : Nat → Bool) (x : Nat) : Option Nat := + if P x then + some x + else + find P (x +1) +partial_fixpoint + +/-- +info: equations: +theorem find.eq_1 : ∀ (P : Nat → Bool) (x : Nat), find P x = if P x = true then some x else find P (x + 1) +-/ +#guard_msgs in +#print equations find + +/-- +error: failed to compile definition 'notinhabited' using `partial_fixpoint`, could not prove that the type + (n : Nat) → Nat → Fin n +is nonempty. + +This process uses multiple strategies: +- It looks for a parameter that matches the return type. +- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance. +- It tries unfolding the return type. + +If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it. +-/ +#guard_msgs in +def notinhabited (n m : Nat) : Fin n := + notinhabited n (m+1) +partial_fixpoint + +/-- +error: failed to compile definition 'notinhabited_mutual1' using `partial_fixpoint`, could not prove that the type + (n : Nat) → Nat → Fin n +is nonempty. + +This process uses multiple strategies: +- It looks for a parameter that matches the return type. +- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance. +- It tries unfolding the return type. + +If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it. +-/ +#guard_msgs in +mutual +def notinhabited_mutual1 (n m : Nat) : Fin n := + notinhabited_mutual2 n (m+1) +partial_fixpoint +def notinhabited_mutual2 (n m : Nat) : Fin n := + notinhabited_mutual1 n (m+1) +partial_fixpoint +end + + +/-- +error: Could not prove 'notTailRec1' to be monotone in its recursive calls: + Cannot eliminate recursive call `notTailRec1 (n + 1)` enclosed in + notTailRec1 (n + 1) - 1 +-/ +#guard_msgs in +def notTailRec1 (n : Nat) := notTailRec1 (n + 1) - 1 +partial_fixpoint + +/-- +error: Could not prove 'notTailRec2' to be monotone in its recursive calls: + Cannot eliminate recursive call `notTailRec2 n (m + 1)` enclosed in + notTailRec2 n (m + 1) - 1 +-/ +#guard_msgs in +def notTailRec2 (n m : Nat) := notTailRec2 n (m + 1) - 1 +partial_fixpoint + +/-- +error: Could not prove 'notTailRec3' to be monotone in its recursive calls: + Cannot eliminate recursive call `notTailRec3 (m + 1) n` enclosed in + notTailRec3 (m + 1) n - 1 +-/ +#guard_msgs in +def notTailRec3 (n m : Nat) := notTailRec3 (m + 1) n - 1 +partial_fixpoint + +/-- +error: Could not prove 'notTailRec4a' to be monotone in its recursive calls: + Cannot eliminate recursive call `notTailRec4b (m + 1) n` enclosed in + notTailRec4b (m + 1) n - 1 +-/ +#guard_msgs in +mutual +def notTailRec4a (n m : Nat) := notTailRec4b (m + 1) n - 1 +partial_fixpoint +def notTailRec4b (n m : Nat) := notTailRec4a (m + 1) n - 1 +partial_fixpoint +end + +def fib (n : Nat) := go 0 0 1 +where + go i fip fi := + if i = n then + fi + else + go (i + 1) fi (fi + fip) + partial_fixpoint + +local instance (b : Bool) [Nonempty α] [Nonempty β] : Nonempty (if b then α else β) := by + split <;> assumption + +def dependent1 (b : Bool) (n : Nat) : if b then Nat else Bool + := dependent1 b (n + 1) +partial_fixpoint + +def dependent2 (b : Bool) (n : Nat) : if b then Nat else Bool := + if b then dependent2 b (n + 1) else dependent2 b (n + 1) +partial_fixpoint + +def dependent2' (n : Nat) (b : Bool) : if b then Nat else Bool := + if b then dependent2' (n + 1) b else dependent2' (n + 2) b +partial_fixpoint + +def dependent2'' (n : Nat) (b : Bool) : if b then Nat else Bool := + if _ : b then dependent2'' (n + 1) b else dependent2'' (n + 2) b +partial_fixpoint + +local instance (b : Bool) [Nonempty α] [Nonempty β] : Nonempty (cond b α β) := by + cases b <;> assumption + +def dependent3 (b : Bool) (n : Nat) : cond b Nat Bool := + match b with + | true => dependent3 true (n + 1) + | false => dependent3 false (n + 2) +partial_fixpoint + +mutual +def mutualUnary1 (n : Nat) : Unit := mutualUnary2 (n + 1) +partial_fixpoint +def mutualUnary2 (n : Nat) : Unit := mutualUnary1 (n + 1) +partial_fixpoint +end + +mutual +def mutual1 (n m : Nat) : Unit := mutual2 (m + 1) n +partial_fixpoint +def mutual2 (n m : Nat) : Unit := mutual1 (m + 1) n +partial_fixpoint +end + +mutual +def dependent2''a (n : Nat) (b : Bool) : if b then Nat else Bool := + if _ : b then dependent2''a (n + 1) b else dependent2''b (n + 2) b +partial_fixpoint +def dependent2''b (n : Nat) (b : Bool) : if b then Nat else Bool := + if _ : b then dependent2''a (n + 1) b else dependent2''b (n + 2) b +partial_fixpoint +end + +/-- +info: equations: +theorem dependent2''b.eq_1 : ∀ (n : Nat) (b : Bool), + dependent2''b n b = if x : b = true then dependent2''a (n + 1) b else dependent2''b (n + 2) b +-/ +#guard_msgs in #print equations dependent2''b + +/-- +info: dependent2''b.eq_unfold : + dependent2''b = fun n b => if x : b = true then dependent2''a (n + 1) b else dependent2''b (n + 2) b +-/ +#guard_msgs in #check dependent2''b.eq_unfold + +def computeLfp' {α : Type u} [DecidableEq α] (f : α → α) (x : α) : α := + let next := f x + if x ≠ next then + computeLfp' f next + else + x +partial_fixpoint + +/-- +info: equations: +theorem computeLfp'.eq_1.{u} : ∀ {α : Type u} [inst : DecidableEq α] (f : α → α) (x : α), + computeLfp' f x = if x ≠ f x then computeLfp' f (f x) else x +-/ +#guard_msgs in #print equations computeLfp' + +/-- +error: Could not prove 'computeLfp'''' to be monotone in its recursive calls: + Cannot eliminate recursive call `computeLfp''' f next` enclosed in + id (computeLfp''' f next) +-/ +#guard_msgs in +def computeLfp''' {α : Type u} [DecidableEq α] (f : α → α) (x : α) : α := + have next := f x + if x ≠ next then + id $ computeLfp''' f next -- NB: Error message should use correct variable name + else + x +partial_fixpoint + +def whileSome (f : α → Option α) (x : α) : α := + match f x with + | none => x + | some x' => whileSome f x' +partial_fixpoint + +/-- +info: equations: +theorem whileSome.eq_1.{u_1} : ∀ {α : Type u_1} (f : α → Option α) (x : α), + whileSome f x = + match f x with + | none => x + | some x' => whileSome f x' +-/ +#guard_msgs in #print equations whileSome + +def ack : (n m : Nat) → Option Nat + | 0, y => some (y+1) + | x+1, 0 => ack x 1 + | x+1, y+1 => do ack x (← ack (x+1) y) +partial_fixpoint + +/-- +info: equations: +theorem ack.eq_1 : ∀ (x : Nat), ack 0 x = some (x + 1) +theorem ack.eq_2 : ∀ (x_2 : Nat), ack x_2.succ 0 = ack x_2 1 +theorem ack.eq_3 : ∀ (x_2 y : Nat), + ack x_2.succ y.succ = do + let __do_lift ← ack (x_2 + 1) y + ack x_2 __do_lift +-/ +#guard_msgs in #print equations ack + +/-- +info: ack.eq_def (x✝ x✝¹ : Nat) : + ack x✝ x✝¹ = + match x✝, x✝¹ with + | 0, y => some (y + 1) + | x.succ, 0 => ack x 1 + | x.succ, y.succ => do + let __do_lift ← ack (x + 1) y + ack x __do_lift +-/ +#guard_msgs in #check ack.eq_def + +/-- +info: ack.eq_unfold : + ack = fun x x_1 => + match x, x_1 with + | 0, y => some (y + 1) + | x.succ, 0 => ack x 1 + | x.succ, y.succ => do + let __do_lift ← ack (x + 1) y + ack x __do_lift +-/ +#guard_msgs in #check ack.eq_unfold + +/-- +error: Could not prove 'WrongMonad.ack' to be monotone in its recursive calls: + Cannot eliminate recursive call `ack (x + 1) y` enclosed in + do + let __do_lift ← ack (x✝ + 1) y✝ + ack x✝ __do_lift + Tried to apply 'Lean.Order.monotone_bind', but failed. + Possible cause: A missing `Lean.Order.MonoBind` instance. + Use `set_option trace.Elab.Tactic.partial_monotonicity true` to debug. +-/ +#guard_msgs in +def WrongMonad.ack : (n m : Nat) → Id Nat + | 0, y => pure (y+1) + | x+1, 0 => ack x 1 + | x+1, y+1 => do ack x (← ack (x+1) y) +partial_fixpoint + +structure Tree where cs : List Tree + +def Tree.rev (t : Tree) : Option Tree := do + Tree.mk (← t.cs.reverse.mapM (Tree.rev ·)) +partial_fixpoint + +def Tree.rev' (t : Tree) : Option Tree := do + let mut cs := [] + for c in t.cs do + cs := (← c.rev') :: cs + return Tree.mk cs +partial_fixpoint + + + +-- These tests check that the user's variable names are preserved in the goals + +/-- +error: Could not prove 'VarName.computeLfp' to be monotone in its recursive calls: + Cannot eliminate recursive call `computeLfp f next` enclosed in + id (computeLfp f next) +-/ +#guard_msgs in +def VarName.computeLfp {α : Type u} [DecidableEq α] (f : α → Option α) (x : α) : Option α := do + let next ← f x + if x ≠ next then + id $ computeLfp f next --NB: Error message should use correct variable name + else + x +partial_fixpoint + + +opaque mentionsH : ¬ b → α → α := fun _ x => x + +/-- +error: Could not prove 'VarName.dite' to be monotone in its recursive calls: + Cannot eliminate recursive call `dite (n + 2) b` enclosed in + mentionsH this_is_my_h (dite (n + 2) b) +-/ +#guard_msgs in +def VarName.dite (n : Nat) (b : Bool) : if b then Nat else Bool := + if this_is_my_h : b then dite (n + 1) b else mentionsH this_is_my_h (dite (n + 2) b) +partial_fixpoint + + +/-- +error: Could not prove 'Tree.rev_bad' to be monotone in its recursive calls: + Cannot eliminate recursive call `Tree.rev_bad my_name` enclosed in + id my_name.rev_bad +-/ +#guard_msgs in +def Tree.rev_bad (t : Tree) : Option Tree := do + Tree.mk (← t.cs.reverse.mapM (fun my_name => id (Tree.rev_bad my_name))) +partial_fixpoint + +/-- +error: Could not prove 'Tree.rev''' to be monotone in its recursive calls: + Cannot eliminate recursive call `Tree.rev'' my_name` enclosed in + id (if my_idx < 0 then some my_name else my_name.rev'') +-/ +#guard_msgs in +def Tree.rev'' (t : Tree) : Option Tree := do + Tree.mk (← t.cs.reverse.toArray.mapFinIdxM + (fun my_idx my_name _ => id (if my_idx < 0 then my_name else Tree.rev'' my_name))).toList +partial_fixpoint + +/-- +error: Could not prove 'Tree.rev'''' to be monotone in its recursive calls: + Cannot eliminate recursive call `Tree.rev''' my_tree.cs.toArray` enclosed in + ts.reverse.mapFinIdxM fun my_idx my_tree x => + id + (if my_idx < 0 then my_tree + else do + let ts ← rev''' my_tree.cs.toArray + { cs := ts.toList }) + Tried to apply 'Lean.Order.Array.monotone_mapFinIdxM', but failed. + Possible cause: A missing `Lean.Order.MonoBind` instance. + Use `set_option trace.Elab.Tactic.partial_monotonicity true` to debug. +-/ +#guard_msgs in +def Tree.rev''' (ts : Array Tree) : Id (Array Tree) := do + ts.reverse.mapFinIdxM + (fun my_idx my_tree _ => id (if my_idx < 0 then my_tree else (Tree.rev''' my_tree.cs.toArray) >>= (fun ts => ⟨ts.toList⟩))) +partial_fixpoint + +def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with + | [] => none + | x::ys => + if p x then + some 0 + else + (· + 1) <$> List.findIndex ys p +partial_fixpoint + + +-- Applicative operator idioms + +def app (n m : Nat) : Option Nat := (· + ·) <$> app (n - 1) m <*> app n (m - 1) +partial_fixpoint + +def app' (n m : Nat) : Option Nat := pure (· + ·) <*> app' (n - 1) m <*> app' n (m - 1) +partial_fixpoint + +def app'' {α} (n : Nat) : Option (α → α) := do + let _n ← app'' (n+1) <*> pure 5 + pure id +partial_fixpoint diff --git a/tests/lean/run/partial_fixpoint_aeneas.lean b/tests/lean/run/partial_fixpoint_aeneas.lean new file mode 100644 index 0000000000..3b909369af --- /dev/null +++ b/tests/lean/run/partial_fixpoint_aeneas.lean @@ -0,0 +1,149 @@ +/-! +Examples of partial functions taken from +https://github.com/AeneasVerif/aeneas/blob/9d3febaff93ff02756c648561c9ad2b18d5d9b62/backends/lean/Base/Diverge/Elab.lean +and using Option instead of Result +-/ + +abbrev Result := Option +abbrev Result.ok := @Option.some + +def list_nth {a: Type u} (ls : List a) (i : Int) : Option a := + match ls with + | [] => none + | x :: ls => do + if i = 0 then pure x + else pure (← list_nth ls (i - 1)) +partial_fixpoint + +def list_nth_with_back {a: Type} (ls : List a) (i : Int) : + Result (a × (a → Result (List a))) := + match ls with + | [] => none + | x :: ls => + if i = 0 then return (x, (λ ret => return (ret :: ls))) + else do + let (x, back) ← list_nth_with_back ls (i - 1) + return (x, + (λ ret => do + let ls ← back ret + return (x :: ls))) +partial_fixpoint + + +mutual + def is_even (i : Int) : Result Bool := + if i = 0 then return true else return (← is_odd (i - 1)) + partial_fixpoint + + def is_odd (i : Int) : Result Bool := + if i = 0 then return false else return (← is_even (i - 1)) + partial_fixpoint +end + +mutual + def foo (i : Int) : Result Nat := + if i > 10 then return (← foo (i / 10)) + (← bar i) else bar 10 + partial_fixpoint + + def bar (i : Int) : Result Nat := + if i > 20 then foo (i / 20) else .ok 42 + partial_fixpoint +end + +def test1 (_ : Option Bool) (_ : Unit) : Result Unit + := test1 Option.none () +partial_fixpoint + +def infinite_loop : Result Unit := do + let _ ← infinite_loop + Result.ok () +partial_fixpoint + +def infinite_loop1 : Result Unit := + infinite_loop1 +partial_fixpoint + +section HigherOrder + inductive Tree (a : Type u) where + | leaf (x : a) + | node (tl : List (Tree a)) + +def Tree.id {a : Type u} (t : Tree a) : Result (Tree a) := + match t with + | .leaf x => .ok (.leaf x) + | .node tl => + do + let tl ← List.mapM Tree.id tl + .ok (.node tl) +partial_fixpoint + +def id1 {a : Type u} (t : Tree a) : Result (Tree a) := + match t with + | .leaf x => .ok (.leaf x) + | .node tl => + do + let tl ← List.mapM (fun x => id1 x) tl + .ok (.node tl) +partial_fixpoint + +def id2 {a : Type u} (t : Tree a) : Result (Tree a) := + match t with + | .leaf x => .ok (.leaf x) + | .node tl => + do + let tl ← List.mapM (fun x => do let _ ← id2 x; id2 x) tl + .ok (.node tl) +partial_fixpoint + +def incr (t : Tree Nat) : Result (Tree Nat) := + match t with + | .leaf x => .ok (.leaf (x + 1)) + | .node tl => + do + let tl ← List.mapM incr tl + .ok (.node tl) +partial_fixpoint + +def id3 (t : Tree Nat) : Result (Tree Nat) := + match t with + | .leaf x => .ok (.leaf (x + 1)) + | .node tl => + do + let f := id3 + let tl ← List.mapM f tl + .ok (.node tl) +partial_fixpoint + +def id4 (t : Tree Nat) : Result (Tree Nat) := + match t with + | .leaf x => .ok (.leaf (x + 1)) + | .node tl => + do + let f x := do + let x1 ← id4 x + id4 x1 + let tl ← List.mapM f tl + .ok (.node tl) +partial_fixpoint + + +-- Like aeneas, we cannot handle the following + +/-- +error: Could not prove 'id5' to be monotone in its recursive calls: + Cannot eliminate recursive call `id5` enclosed in + Result.ok id5 +-/ +#guard_msgs in +def id5 (t : Tree Nat) : Result (Tree Nat) := + match t with + | .leaf x => .ok (.leaf (x + 1)) + | .node tl => + do + let f ← .ok id5 + let tl ← List.mapM f tl + .ok (.node tl) +partial_fixpoint + + +end HigherOrder diff --git a/tests/lean/run/partial_fixpoint_aeneas2.lean b/tests/lean/run/partial_fixpoint_aeneas2.lean new file mode 100644 index 0000000000..2c515b5051 --- /dev/null +++ b/tests/lean/run/partial_fixpoint_aeneas2.lean @@ -0,0 +1,1497 @@ +import Lean + +/-! + +Provided by Son Ho + +I put together some of the files generated by Aeneas (they come from the models generated for a +hashmap, an AVL tree and a b-epsilon tree) into a single self-contained file: from what I remember +some definitions there triggered issues with divergent, so I think they should be good test cases +for partial_def, at least to see whether your implementation covers all my use cases. :-) + +Note that many definitions are actually structurally terminating (I still added termination clauses +to them so that you can easily find them): they also are good test cases for partial_def. Also, as a +side note: whenever Aeneas generates a recursive definition, it adds the divergent keyword (because +I haven't implemented a termination checker, and I actually don't see the point of doing that). +-/ + +/- Duplicating some basic definitions -/ +namespace Primitives + inductive Error where + | assertionFailure: Error + | integerOverflow: Error + | divisionByZero: Error + | arrayOutOfBounds: Error + | maximumSizeExceeded: Error + | panic: Error + -- Addded by Joachim + | nontermination : Error + + + + inductive Result (α : Type u) where + | ok (v: α): Result α + | fail (e: Error): Result α + | div + + open Result + + def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β := + match x with + | ok v => f v + | fail v => fail v + | div => div + + instance : Bind Result where + bind := bind + + instance : Pure Result where + pure := fun x => ok x + + + -- Added by Joachim + section Order + open Lean.Order + + instance : PartialOrder (Result α) := inferInstanceAs (PartialOrder (FlatOrder (.fail .nontermination))) + noncomputable instance : CCPO (Result α) := inferInstanceAs (CCPO (FlatOrder (.fail .nontermination))) + noncomputable instance : MonoBind Result where + bind_mono_left h := by + cases h + · exact FlatOrder.rel.bot + · exact FlatOrder.rel.refl + bind_mono_right h := by + cases ‹Result _› + · exact h _ + · exact FlatOrder.rel.refl + · exact FlatOrder.rel.refl + end Order + + structure Isize where + val : Int + hmin : -2147483648 ≤ val + hmax : val ≤ 2147483647 + + @[reducible] def Isize.ofInt (x : Int) + (hInBounds : -2147483648 ≤ x ∧ x ≤ 2147483647) : Isize := + ⟨ x, by simp [*], by simp [*] ⟩ + + macro:max x:term:max noWs "#isize" : term => `(Isize.ofInt $x (by decide)) + + instance : LT Isize where lt a b := LT.lt a.val b.val + instance : LE Isize where le a b := LE.le a.val b.val + instance Isize.decLt (a b : Isize) : Decidable (LT.lt a b) := Int.decLt .. + instance Isize.decLe (a b : Isize) : Decidable (LE.le a b) := Int.decLe .. + + theorem Isize.eq_of_val_eq : ∀ {i j : Isize}, Eq i.val j.val → Eq i j + | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl + + theorem Isize.val_eq_of_eq {i j : Isize} (h : Eq i j) : Eq i.val j.val := + h ▸ rfl + + theorem Isize.ne_of_val_ne {i j : Isize} (h : Not (Eq i.val j.val)) : Not (Eq i j) := + fun h' => absurd (val_eq_of_eq h') h + + instance : DecidableEq Isize := + fun i j => + match decEq i.val j.val with + | isTrue h => isTrue (Isize.eq_of_val_eq h) + | isFalse h => isFalse (Isize.ne_of_val_ne h) + + -- Using `sorry` rather than axiom so that I don't have to mark definitions as `noncomputable` + -- We could also use variables... + def Isize.add : Isize → Isize → Result Isize := sorry + def Isize.sub : Isize → Isize → Result Isize := sorry + def Isize.mul : Isize → Isize → Result Isize := sorry + def Isize.mod : Isize → Isize → Result Isize := sorry + def Isize.div : Isize → Isize → Result Isize := sorry + + instance : HAdd Isize Isize (Result Isize) where + hAdd x y := Isize.add x y + + instance : HSub Isize Isize (Result Isize) where + hSub x y := Isize.sub x y + + instance : HMul Isize Isize (Result Isize) where + hMul x y := Isize.mul x y + + instance : HMod Isize Isize (Result Isize) where + hMod x y := Isize.mod x y + + instance : HDiv Isize Isize (Result Isize) where + hDiv x y := Isize.div x y + + def alloc.vec.Vec (T : Type) : Type := sorry + def alloc.vec.Vec.len {T : Type} : alloc.vec.Vec T → Isize := sorry + def alloc.vec.Vec.new : (T:Type) → alloc.vec.Vec T := sorry + def alloc.vec.Vec.push {T : Type} : alloc.vec.Vec T → T → Result (alloc.vec.Vec T) := sorry + def alloc.vec.Vec.index_isize {α : Type} (v: Vec α) (i: Isize) : Result α := sorry + def alloc.vec.Vec.index_mut_isize {α : Type} (v: Vec α) (i: Isize) : Result (α × (α → Vec α)) := sorry + + opaque core.mem.replace {T : Type} : T → T → T × T := fun x _ => (x, x) + def core.option.Option.unwrap {T : Type} : Option T → Result T := sorry + + def core_isize_max : Isize := 2147483647#isize + + structure core.clone.Clone (T : Type) where + clone : T → Result T + + structure core.marker.Copy (T : Type) where + cloneInst : core.clone.Clone T +end Primitives + +open Primitives + +/- Hashmap -/ +namespace hashmap + inductive AList (T : Type) where + | Cons : Isize → T → AList T → AList T + | Nil : AList T + + structure Fraction where + dividend : Isize + divisor : Isize + + structure HashMap (T : Type) where + num_entries : Isize + max_load_factor : Fraction + max_load : Isize + saturated : Bool + slots : alloc.vec.Vec (AList T) + + def hash_key (k : Isize) : Result Isize := + Result.ok k + + def ClonehashmapFraction.clone (self : Fraction) : Result Fraction := + Result.ok self + + @[reducible] + def core.clone.ClonehashmapFraction : core.clone.Clone Fraction := { + clone := ClonehashmapFraction.clone + } + + @[reducible] + def core.marker.CopyhashmapFraction : core.marker.Copy Fraction := { + cloneInst := core.clone.ClonehashmapFraction + } + + def HashMap.allocate_slots_loop + {T : Type} (slots : alloc.vec.Vec (AList T)) (n : Isize) : + Result (alloc.vec.Vec (AList T)) + := + if n > 0#isize + then + do + let slots1 ← alloc.vec.Vec.push slots AList.Nil + let n1 ← n - 1#isize + HashMap.allocate_slots_loop slots1 n1 + else Result.ok slots + partial_fixpoint + + def HashMap.allocate_slots + {T : Type} (slots : alloc.vec.Vec (AList T)) (n : Isize) : + Result (alloc.vec.Vec (AList T)) + := + HashMap.allocate_slots_loop slots n + + def HashMap.new_with_capacity + (T : Type) (capacity : Isize) (max_load_factor : Fraction) : + Result (HashMap T) + := + do + let slots ← HashMap.allocate_slots (alloc.vec.Vec.new (AList T)) capacity + let i ← capacity * max_load_factor.dividend + let i1 ← i / max_load_factor.divisor + Result.ok + { + num_entries := 0#isize, + max_load_factor, + max_load := i1, + saturated := false, + slots + } + + def HashMap.new (T : Type) : Result (HashMap T) := + HashMap.new_with_capacity T 32#isize + { dividend := 4#isize, divisor := 5#isize } + + def HashMap.clear_loop + {T : Type} (slots : alloc.vec.Vec (AList T)) (i : Isize) : + Result (alloc.vec.Vec (AList T)) + := + let i1 := alloc.vec.Vec.len slots + if i < i1 + then + do + let (_, index_mut_back) ← alloc.vec.Vec.index_mut_isize slots i + let i2 ← i + 1#isize + let slots1 := index_mut_back AList.Nil + HashMap.clear_loop slots1 i2 + else Result.ok slots + partial_fixpoint + + def HashMap.clear {T : Type} (self : HashMap T) : Result (HashMap T) := + do + let hm ← HashMap.clear_loop self.slots 0#isize + Result.ok { self with num_entries := 0#isize, slots := hm } + + def HashMap.len {T : Type} (self : HashMap T) : Result Isize := + Result.ok self.num_entries + + def HashMap.insert_in_list_loop + {T : Type} (key : Isize) (value : T) (ls : AList T) : + Result (Bool × (AList T)) + := + match ls with + | AList.Cons ckey cvalue tl => + if ckey = key + then Result.ok (false, AList.Cons ckey value tl) + else + do + let (b, tl1) ← HashMap.insert_in_list_loop key value tl + Result.ok (b, AList.Cons ckey cvalue tl1) + | AList.Nil => Result.ok (true, AList.Cons key value AList.Nil) + partial_fixpoint + + def HashMap.insert_in_list + {T : Type} (key : Isize) (value : T) (ls : AList T) : + Result (Bool × (AList T)) + := + HashMap.insert_in_list_loop key value ls + + def HashMap.insert_no_resize + {T : Type} (self : HashMap T) (key : Isize) (value : T) : + Result (HashMap T) + := + do + let hash ← hash_key key + let i := alloc.vec.Vec.len self.slots + let hash_mod ← hash % i + let (a, index_mut_back) ← alloc.vec.Vec.index_mut_isize self.slots hash_mod + let (inserted, a1) ← HashMap.insert_in_list key value a + if inserted + then + do + let i1 ← self.num_entries + 1#isize + let v := index_mut_back a1 + Result.ok { self with num_entries := i1, slots := v } + else + let v := index_mut_back a1 + Result.ok { self with slots := v } + + def HashMap.move_elements_from_list_loop + {T : Type} (ntable : HashMap T) (ls : AList T) : Result (HashMap T) := + match ls with + | AList.Cons k v tl => + do + let ntable1 ← HashMap.insert_no_resize ntable k v + HashMap.move_elements_from_list_loop ntable1 tl + | AList.Nil => Result.ok ntable + partial_fixpoint + + def HashMap.move_elements_from_list + {T : Type} (ntable : HashMap T) (ls : AList T) : Result (HashMap T) := + HashMap.move_elements_from_list_loop ntable ls + + def HashMap.move_elements_loop + {T : Type} (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) (i : Isize) + : + Result ((HashMap T) × (alloc.vec.Vec (AList T))) + := + let i1 := alloc.vec.Vec.len slots + if i < i1 + then + do + let (a, index_mut_back) ← alloc.vec.Vec.index_mut_isize slots i + let (ls, a1) := core.mem.replace a AList.Nil + let ntable1 ← HashMap.move_elements_from_list ntable ls + let i2 ← i + 1#isize + let slots1 := index_mut_back a1 + HashMap.move_elements_loop ntable1 slots1 i2 + else Result.ok (ntable, slots) + partial_fixpoint + set_option pp.proofs true in + #print HashMap.move_elements_loop.proof_2 + + def HashMap.move_elements + {T : Type} (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) : + Result ((HashMap T) × (alloc.vec.Vec (AList T))) + := + HashMap.move_elements_loop ntable slots 0#isize + + def HashMap.try_resize {T : Type} (self : HashMap T) : Result (HashMap T) := + do + let capacity := alloc.vec.Vec.len self.slots + let n1 ← core_isize_max / 2#isize + let i ← n1 / self.max_load_factor.dividend + if capacity <= i + then + do + let i1 ← capacity * 2#isize + let ntable ← HashMap.new_with_capacity T i1 self.max_load_factor + let p ← HashMap.move_elements ntable self.slots + let (ntable1, _) := p + Result.ok + { self with max_load := ntable1.max_load, slots := ntable1.slots } + else Result.ok { self with saturated := true } + + def HashMap.insert + {T : Type} (self : HashMap T) (key : Isize) (value : T) : + Result (HashMap T) + := + do + let self1 ← HashMap.insert_no_resize self key value + let i ← HashMap.len self1 + if i > self1.max_load + then + if self1.saturated + then Result.ok self1 + else HashMap.try_resize self1 + else Result.ok self1 + + def HashMap.contains_key_in_list_loop + {T : Type} (key : Isize) (ls : AList T) : Result Bool := + match ls with + | AList.Cons ckey _ tl => + if ckey = key + then Result.ok true + else HashMap.contains_key_in_list_loop key tl + | AList.Nil => Result.ok false + partial_fixpoint + + def HashMap.contains_key_in_list + {T : Type} (key : Isize) (ls : AList T) : Result Bool := + HashMap.contains_key_in_list_loop key ls + + def HashMap.contains_key + {T : Type} (self : HashMap T) (key : Isize) : Result Bool := + do + let hash ← hash_key key + let i := alloc.vec.Vec.len self.slots + let hash_mod ← hash % i + let a ← alloc.vec.Vec.index_isize self.slots hash_mod + HashMap.contains_key_in_list key a + + def HashMap.get_in_list_loop + {T : Type} (key : Isize) (ls : AList T) : Result (Option T) := + match ls with + | AList.Cons ckey cvalue tl => + if ckey = key + then Result.ok (some cvalue) + else HashMap.get_in_list_loop key tl + | AList.Nil => Result.ok none + partial_fixpoint + + def HashMap.get_in_list + {T : Type} (key : Isize) (ls : AList T) : Result (Option T) := + HashMap.get_in_list_loop key ls + + def HashMap.get + {T : Type} (self : HashMap T) (key : Isize) : Result (Option T) := + do + let hash ← hash_key key + let i := alloc.vec.Vec.len self.slots + let hash_mod ← hash % i + let a ← alloc.vec.Vec.index_isize self.slots hash_mod + HashMap.get_in_list key a + + def HashMap.get_mut_in_list_loop + {T : Type} (ls : AList T) (key : Isize) : + Result ((Option T) × (Option T → AList T)) + := + match ls with + | AList.Cons ckey cvalue tl => + if ckey = key + then + let back := + fun ret => + let t := match ret with + | some t1 => t1 + | _ => cvalue + AList.Cons ckey t tl + Result.ok (some cvalue, back) + else + do + let (o, back) ← HashMap.get_mut_in_list_loop tl key + let back1 := fun ret => let tl1 := back ret + AList.Cons ckey cvalue tl1 + Result.ok (o, back1) + | AList.Nil => let back := fun _ret => AList.Nil + Result.ok (none, back) + partial_fixpoint + + def HashMap.get_mut_in_list + {T : Type} (ls : AList T) (key : Isize) : + Result ((Option T) × (Option T → AList T)) + := + HashMap.get_mut_in_list_loop ls key + + def HashMap.get_mut + {T : Type} (self : HashMap T) (key : Isize) : + Result ((Option T) × (Option T → HashMap T)) + := + do + let hash ← hash_key key + let i := alloc.vec.Vec.len self.slots + let hash_mod ← hash % i + let (a, index_mut_back) ← alloc.vec.Vec.index_mut_isize self.slots hash_mod + let (o, get_mut_in_list_back) ← HashMap.get_mut_in_list a key + let back := + fun ret => + let a1 := get_mut_in_list_back ret + let v := index_mut_back a1 + { self with slots := v } + Result.ok (o, back) + + def HashMap.remove_from_list_loop + {T : Type} (key : Isize) (ls : AList T) : Result ((Option T) × (AList T)) := + match ls with + | AList.Cons ckey t tl => + if ckey = key + then + let (mv_ls, _) := core.mem.replace ls AList.Nil + match mv_ls with + | AList.Cons _ cvalue tl1 => Result.ok (some cvalue, tl1) + | AList.Nil => Result.fail .panic + else + do + let (o, tl1) ← HashMap.remove_from_list_loop key tl + Result.ok (o, AList.Cons ckey t tl1) + | AList.Nil => Result.ok (none, AList.Nil) + partial_fixpoint + + def HashMap.remove_from_list + {T : Type} (key : Isize) (ls : AList T) : Result ((Option T) × (AList T)) := + HashMap.remove_from_list_loop key ls + + def HashMap.remove + {T : Type} (self : HashMap T) (key : Isize) : + Result ((Option T) × (HashMap T)) + := + do + let hash ← hash_key key + let i := alloc.vec.Vec.len self.slots + let hash_mod ← hash % i + let (a, index_mut_back) ← alloc.vec.Vec.index_mut_isize self.slots hash_mod + let (x, a1) ← HashMap.remove_from_list key a + match x with + | none => + let v := index_mut_back a1 + Result.ok (none, { self with slots := v }) + | some _ => + do + let i1 ← self.num_entries - 1#isize + let v := index_mut_back a1 + Result.ok (x, { self with num_entries := i1, slots := v }) + +end hashmap + +namespace betree + + inductive betree.List (T : Type) where + | Cons : T → betree.List T → betree.List T + | Nil : betree.List T + + inductive betree.UpsertFunState where + | Add : Isize → betree.UpsertFunState + | Sub : Isize → betree.UpsertFunState + + inductive betree.Message where + | Insert : Isize → betree.Message + | Delete : betree.Message + | Upsert : betree.UpsertFunState → betree.Message + + structure betree.Leaf where + id : Isize + size : Isize + + mutual + + inductive betree.Internal where + | mk : Isize → Isize → betree.Node → betree.Node → betree.Internal + + inductive betree.Node where + | Internal : betree.Internal → betree.Node + | Leaf : betree.Leaf → betree.Node + + end + + @[reducible] + def betree.Internal.id (x : betree.Internal) := + match x with | betree.Internal.mk x1 _ _ _ => x1 + + @[reducible] + def betree.Internal.pivot (x : betree.Internal) := + match x with | betree.Internal.mk _ x1 _ _ => x1 + + @[reducible] + def betree.Internal.left (x : betree.Internal) := + match x with | betree.Internal.mk _ _ x1 _ => x1 + + @[reducible] + def betree.Internal.right (x : betree.Internal) := + match x with | betree.Internal.mk _ _ _ x1 => x1 + + /- [betree::betree::Params] + Source: 'src/betree.rs', lines 187:0-199:1 -/ + structure betree.Params where + min_flush_size : Isize + split_size : Isize + + /- [betree::betree::NodeIdCounter] + Source: 'src/betree.rs', lines 201:0-203:1 -/ + structure betree.NodeIdCounter where + next_node_id : Isize + + /- [betree::betree::BeTree] + Source: 'src/betree.rs', lines 218:0-225:1 -/ + structure betree.BeTree where + params : betree.Params + node_id_cnt : betree.NodeIdCounter + root : betree.Node + + def betree_utils.load_internal_node + : + Isize → State → Result (State × (betree.List (Isize × betree.Message))) := + fun _ _ => .fail .panic + + def betree_utils.store_internal_node + : + Isize → betree.List (Isize × betree.Message) → State → Result (State + × Unit) := + fun _ _ _ => .fail .panic + + def betree_utils.load_leaf_node + : Isize → State → Result (State × (betree.List (Isize × Isize))) := + fun _ _ => .fail .panic + + def betree_utils.store_leaf_node + : Isize → betree.List (Isize × Isize) → State → Result (State × Unit) := + fun _ _ _ => .fail .panic + + def betree.load_internal_node + (id : Isize) (st : State) : + Result (State × (betree.List (Isize × betree.Message))) + := + betree_utils.load_internal_node id st + + def betree.store_internal_node + (id : Isize) (content : betree.List (Isize × betree.Message)) (st : State) : + Result (State × Unit) + := + betree_utils.store_internal_node id content st + + def betree.load_leaf_node + (id : Isize) (st : State) : Result (State × (betree.List (Isize × Isize))) := + betree_utils.load_leaf_node id st + + def betree.store_leaf_node + (id : Isize) (content : betree.List (Isize × Isize)) (st : State) : + Result (State × Unit) + := + betree_utils.store_leaf_node id content st + + def betree.fresh_node_id (counter : Isize) : Result (Isize × Isize) := + do + let counter1 ← counter + 1#isize + Result.ok (counter, counter1) + + def betree.NodeIdCounter.new : Result betree.NodeIdCounter := + Result.ok { next_node_id := 0#isize } + + def betree.NodeIdCounter.fresh_id + (self : betree.NodeIdCounter) : Result (Isize × betree.NodeIdCounter) := + do + let i ← self.next_node_id + 1#isize + Result.ok (self.next_node_id, { next_node_id := i }) + + def betree.upsert_update + (prev : Option Isize) (st : betree.UpsertFunState) : Result Isize := + match prev with + | none => + match st with + | betree.UpsertFunState.Add v => Result.ok v + | betree.UpsertFunState.Sub _ => Result.ok 0#isize + | some prev1 => + match st with + | betree.UpsertFunState.Add v => + do + let margin ← core_isize_max - prev1 + if margin >= v + then prev1 + v + else Result.ok core_isize_max + | betree.UpsertFunState.Sub v => + if prev1 >= v + then prev1 - v + else Result.ok 0#isize + + def betree.List.len_loop + {T : Type} (self : betree.List T) (len : Isize) : Result Isize := + match self with + | betree.List.Cons _ tl => + do + let len1 ← len + 1#isize + betree.List.len_loop tl len1 + | betree.List.Nil => Result.ok len + partial_fixpoint + + def betree.List.len {T : Type} (self : betree.List T) : Result Isize := + betree.List.len_loop self 0#isize + + def betree.List.reverse_loop + {T : Type} (self : betree.List T) (out : betree.List T) : + Result (betree.List T) + := + match self with + | betree.List.Cons hd tl => + betree.List.reverse_loop tl (betree.List.Cons hd out) + | betree.List.Nil => Result.ok out + partial_fixpoint + + def betree.List.reverse + {T : Type} (self : betree.List T) : Result (betree.List T) := + betree.List.reverse_loop self betree.List.Nil + + def betree.List.split_at_loop + {T : Type} (n : Isize) (beg : betree.List T) (self : betree.List T) : + Result ((betree.List T) × (betree.List T)) + := + if n > 0#isize + then + match self with + | betree.List.Cons hd tl => + do + let n1 ← n - 1#isize + betree.List.split_at_loop n1 (betree.List.Cons hd beg) tl + | betree.List.Nil => Result.fail .panic + else do + let l ← betree.List.reverse beg + Result.ok (l, self) + partial_fixpoint + + def betree.List.split_at + {T : Type} (self : betree.List T) (n : Isize) : + Result ((betree.List T) × (betree.List T)) + := + betree.List.split_at_loop n betree.List.Nil self + + def betree.List.push_front + {T : Type} (self : betree.List T) (x : T) : Result (betree.List T) := + let (tl, _) := core.mem.replace self betree.List.Nil + Result.ok (betree.List.Cons x tl) + + def betree.List.pop_front + {T : Type} (self : betree.List T) : Result (T × (betree.List T)) := + let (ls, _) := core.mem.replace self betree.List.Nil + match ls with + | betree.List.Cons x tl => Result.ok (x, tl) + | betree.List.Nil => Result.fail .panic + + def betree.List.hd {T : Type} (self : betree.List T) : Result T := + match self with + | betree.List.Cons hd _ => Result.ok hd + | betree.List.Nil => Result.fail .panic + + def betree.ListPairIsizeT.head_has_key + {T : Type} (self : betree.List (Isize × T)) (key : Isize) : Result Bool := + match self with + | betree.List.Cons hd _ => + let (i, _) := hd + Result.ok (i = key) + | betree.List.Nil => + Result.ok false + + def betree.ListPairIsizeT.partition_at_pivot_loop + {T : Type} (pivot : Isize) (beg : betree.List (Isize × T)) + (end1 : betree.List (Isize × T)) (self : betree.List (Isize × T)) : + Result ((betree.List (Isize × T)) × (betree.List (Isize × T))) + := + match self with + | betree.List.Cons hd tl => + let (i, _) := hd + if i >= pivot + then + betree.ListPairIsizeT.partition_at_pivot_loop pivot beg (betree.List.Cons + hd end1) tl + else + betree.ListPairIsizeT.partition_at_pivot_loop pivot (betree.List.Cons hd + beg) end1 tl + | betree.List.Nil => + do + let l ← betree.List.reverse beg + let l1 ← betree.List.reverse end1 + Result.ok (l, l1) + partial_fixpoint + + def betree.ListPairIsizeT.partition_at_pivot + {T : Type} (self : betree.List (Isize × T)) (pivot : Isize) : + Result ((betree.List (Isize × T)) × (betree.List (Isize × T))) + := + betree.ListPairIsizeT.partition_at_pivot_loop pivot betree.List.Nil + betree.List.Nil self + + def betree.Leaf.split + (self : betree.Leaf) (content : betree.List (Isize × Isize)) + (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) : + Result (State × (betree.Internal × betree.NodeIdCounter)) + := + do + let p ← betree.List.split_at content params.split_size + let (content0, content1) := p + let p1 ← betree.List.hd content1 + let (pivot, _) := p1 + let (id0, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (id1, node_id_cnt2) ← betree.NodeIdCounter.fresh_id node_id_cnt1 + let (st1, _) ← betree.store_leaf_node id0 content0 st + let (st2, _) ← betree.store_leaf_node id1 content1 st1 + let n := betree.Node.Leaf { id := id0, size := params.split_size } + let n1 := betree.Node.Leaf { id := id1, size := params.split_size } + Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2)) + + def betree.Node.lookup_in_bindings_loop + (key : Isize) (bindings : betree.List (Isize × Isize)) : Result (Option Isize) := + match bindings with + | betree.List.Cons hd tl => + let (i, i1) := hd + if i = key + then Result.ok (some i1) + else + if i > key + then Result.ok none + else betree.Node.lookup_in_bindings_loop key tl + | betree.List.Nil => Result.ok none + partial_fixpoint + + def betree.Node.lookup_in_bindings + (key : Isize) (bindings : betree.List (Isize × Isize)) : Result (Option Isize) := + betree.Node.lookup_in_bindings_loop key bindings + + def betree.Node.lookup_first_message_for_key_loop + (key : Isize) (msgs : betree.List (Isize × betree.Message)) : + Result ((betree.List (Isize × betree.Message)) × (betree.List (Isize × + betree.Message) → betree.List (Isize × betree.Message))) + := + match msgs with + | betree.List.Cons x next_msgs => + let (i, _) := x + if i >= key + then Result.ok (msgs, fun ret => ret) + else + do + let (l, back) ← + betree.Node.lookup_first_message_for_key_loop key next_msgs + let back1 := + fun ret => let next_msgs1 := back ret + betree.List.Cons x next_msgs1 + Result.ok (l, back1) + | betree.List.Nil => Result.ok (betree.List.Nil, fun ret => ret) + partial_fixpoint + + def betree.Node.lookup_first_message_for_key + (key : Isize) (msgs : betree.List (Isize × betree.Message)) : + Result ((betree.List (Isize × betree.Message)) × (betree.List (Isize × + betree.Message) → betree.List (Isize × betree.Message))) + := + betree.Node.lookup_first_message_for_key_loop key msgs + + def betree.Node.apply_upserts_loop + (msgs : betree.List (Isize × betree.Message)) (prev : Option Isize) (key : Isize) + : + Result (Isize × (betree.List (Isize × betree.Message))) + := + do + let b ← betree.ListPairIsizeT.head_has_key msgs key + if b + then + do + let (msg, msgs1) ← betree.List.pop_front msgs + let (_, m) := msg + match m with + | betree.Message.Insert _ => Result.fail .panic + | betree.Message.Delete => Result.fail .panic + | betree.Message.Upsert s => + do + let v ← betree.upsert_update prev s + betree.Node.apply_upserts_loop msgs1 (some v) key + else + do + let v ← core.option.Option.unwrap prev + let msgs1 ← betree.List.push_front msgs (key, betree.Message.Insert v) + Result.ok (v, msgs1) + partial_fixpoint + + def betree.Node.apply_upserts + (msgs : betree.List (Isize × betree.Message)) (prev : Option Isize) (key : Isize) + : + Result (Isize × (betree.List (Isize × betree.Message))) + := + betree.Node.apply_upserts_loop msgs prev key + + mutual + def betree.Internal.lookup_in_children + (self : betree.Internal) (key : Isize) (st : State) : + Result (State × ((Option Isize) × betree.Internal)) + := + if key < self.pivot + then + do + let (st1, (o, n)) ← betree.Node.lookup self.left key st + Result.ok (st1, (o, betree.Internal.mk self.id self.pivot n self.right)) + else + do + let (st1, (o, n)) ← betree.Node.lookup self.right key st + Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n)) + partial_fixpoint + + def betree.Node.lookup + (self : betree.Node) (key : Isize) (st : State) : + Result (State × ((Option Isize) × betree.Node)) + := + match self with + | betree.Node.Internal node => + do + let (st1, msgs) ← betree.load_internal_node node.id st + let (pending, lookup_first_message_for_key_back) ← + betree.Node.lookup_first_message_for_key key msgs + match pending with + | betree.List.Cons p _ => + let (k, msg) := p + if k != key + then + do + let (st2, (o, node1)) ← + betree.Internal.lookup_in_children node key st1 + Result.ok (st2, (o, betree.Node.Internal node1)) + else + match msg with + | betree.Message.Insert v => Result.ok (st1, (some v, self)) + | betree.Message.Delete => Result.ok (st1, (none, self)) + | betree.Message.Upsert _ => + do + let (st2, (v, node1)) ← + betree.Internal.lookup_in_children node key st1 + let (v1, pending1) ← betree.Node.apply_upserts pending v key + let msgs1 := lookup_first_message_for_key_back pending1 + let (st3, _) ← betree.store_internal_node node1.id msgs1 st2 + Result.ok (st3, (some v1, betree.Node.Internal node1)) + | betree.List.Nil => + do + let (st2, (o, node1)) ← betree.Internal.lookup_in_children node key st1 + Result.ok (st2, (o, betree.Node.Internal node1)) + | betree.Node.Leaf node => + do + let (st1, bindings) ← betree.load_leaf_node node.id st + let o ← betree.Node.lookup_in_bindings key bindings + Result.ok (st1, (o, self)) + partial_fixpoint + + end + + def betree.Node.filter_messages_for_key_loop + (key : Isize) (msgs : betree.List (Isize × betree.Message)) : + Result (betree.List (Isize × betree.Message)) + := + match msgs with + | betree.List.Cons p _ => + let (k, _) := p + if k = key + then + do + let (_, msgs1) ← betree.List.pop_front msgs + betree.Node.filter_messages_for_key_loop key msgs1 + else Result.ok msgs + | betree.List.Nil => Result.ok betree.List.Nil + partial_fixpoint + + def betree.Node.filter_messages_for_key + (key : Isize) (msgs : betree.List (Isize × betree.Message)) : + Result (betree.List (Isize × betree.Message)) + := + betree.Node.filter_messages_for_key_loop key msgs + + def betree.Node.lookup_first_message_after_key_loop + (key : Isize) (msgs : betree.List (Isize × betree.Message)) : + Result ((betree.List (Isize × betree.Message)) × (betree.List (Isize × + betree.Message) → betree.List (Isize × betree.Message))) + := + match msgs with + | betree.List.Cons p next_msgs => + let (k, _) := p + if k = key + then + do + let (l, back) ← + betree.Node.lookup_first_message_after_key_loop key next_msgs + let back1 := + fun ret => let next_msgs1 := back ret + betree.List.Cons p next_msgs1 + Result.ok (l, back1) + else Result.ok (msgs, fun ret => ret) + | betree.List.Nil => Result.ok (betree.List.Nil, fun ret => ret) + partial_fixpoint + + def betree.Node.lookup_first_message_after_key + (key : Isize) (msgs : betree.List (Isize × betree.Message)) : + Result ((betree.List (Isize × betree.Message)) × (betree.List (Isize × + betree.Message) → betree.List (Isize × betree.Message))) + := + betree.Node.lookup_first_message_after_key_loop key msgs + + def betree.Node.apply_to_internal + (msgs : betree.List (Isize × betree.Message)) (key : Isize) + (new_msg : betree.Message) : + Result (betree.List (Isize × betree.Message)) + := + do + let (msgs1, lookup_first_message_for_key_back) ← + betree.Node.lookup_first_message_for_key key msgs + let b ← betree.ListPairIsizeT.head_has_key msgs1 key + if b + then + match new_msg with + | betree.Message.Insert _ => + do + let msgs2 ← betree.Node.filter_messages_for_key key msgs1 + let msgs3 ← betree.List.push_front msgs2 (key, new_msg) + Result.ok (lookup_first_message_for_key_back msgs3) + | betree.Message.Delete => + do + let msgs2 ← betree.Node.filter_messages_for_key key msgs1 + let msgs3 ← betree.List.push_front msgs2 (key, betree.Message.Delete) + Result.ok (lookup_first_message_for_key_back msgs3) + | betree.Message.Upsert s => + do + let p ← betree.List.hd msgs1 + let (_, m) := p + match m with + | betree.Message.Insert prev => + do + let v ← betree.upsert_update (some prev) s + let (_, msgs2) ← betree.List.pop_front msgs1 + let msgs3 ← + betree.List.push_front msgs2 (key, betree.Message.Insert v) + Result.ok (lookup_first_message_for_key_back msgs3) + | betree.Message.Delete => + do + let (_, msgs2) ← betree.List.pop_front msgs1 + let v ← betree.upsert_update none s + let msgs3 ← + betree.List.push_front msgs2 (key, betree.Message.Insert v) + Result.ok (lookup_first_message_for_key_back msgs3) + | betree.Message.Upsert _ => + do + let (msgs2, lookup_first_message_after_key_back) ← + betree.Node.lookup_first_message_after_key key msgs1 + let msgs3 ← betree.List.push_front msgs2 (key, new_msg) + let msgs4 := lookup_first_message_after_key_back msgs3 + Result.ok (lookup_first_message_for_key_back msgs4) + else + do + let msgs2 ← betree.List.push_front msgs1 (key, new_msg) + Result.ok (lookup_first_message_for_key_back msgs2) + + def betree.Node.apply_messages_to_internal_loop + (msgs : betree.List (Isize × betree.Message)) + (new_msgs : betree.List (Isize × betree.Message)) : + Result (betree.List (Isize × betree.Message)) + := + match new_msgs with + | betree.List.Cons new_msg new_msgs_tl => + do + let (i, m) := new_msg + let msgs1 ← betree.Node.apply_to_internal msgs i m + betree.Node.apply_messages_to_internal_loop msgs1 new_msgs_tl + | betree.List.Nil => Result.ok msgs + partial_fixpoint + + def betree.Node.apply_messages_to_internal + (msgs : betree.List (Isize × betree.Message)) + (new_msgs : betree.List (Isize × betree.Message)) : + Result (betree.List (Isize × betree.Message)) + := + betree.Node.apply_messages_to_internal_loop msgs new_msgs + + def betree.Node.lookup_mut_in_bindings_loop + (key : Isize) (bindings : betree.List (Isize × Isize)) : + Result ((betree.List (Isize × Isize)) × (betree.List (Isize × Isize) → + betree.List (Isize × Isize))) + := + match bindings with + | betree.List.Cons hd tl => + let (i, _) := hd + if i >= key + then Result.ok (bindings, fun ret => ret) + else + do + let (l, back) ← betree.Node.lookup_mut_in_bindings_loop key tl + let back1 := fun ret => let tl1 := back ret + betree.List.Cons hd tl1 + Result.ok (l, back1) + | betree.List.Nil => Result.ok (betree.List.Nil, fun ret => ret) + partial_fixpoint + + def betree.Node.lookup_mut_in_bindings + (key : Isize) (bindings : betree.List (Isize × Isize)) : + Result ((betree.List (Isize × Isize)) × (betree.List (Isize × Isize) → + betree.List (Isize × Isize))) + := + betree.Node.lookup_mut_in_bindings_loop key bindings + + def betree.Node.apply_to_leaf + (bindings : betree.List (Isize × Isize)) (key : Isize) (new_msg : betree.Message) + : + Result (betree.List (Isize × Isize)) + := + do + let (bindings1, lookup_mut_in_bindings_back) ← + betree.Node.lookup_mut_in_bindings key bindings + let b ← betree.ListPairIsizeT.head_has_key bindings1 key + if b + then + do + let (hd, bindings2) ← betree.List.pop_front bindings1 + match new_msg with + | betree.Message.Insert v => + do + let bindings3 ← betree.List.push_front bindings2 (key, v) + Result.ok (lookup_mut_in_bindings_back bindings3) + | betree.Message.Delete => + Result.ok (lookup_mut_in_bindings_back bindings2) + | betree.Message.Upsert s => + do + let (_, i) := hd + let v ← betree.upsert_update (some i) s + let bindings3 ← betree.List.push_front bindings2 (key, v) + Result.ok (lookup_mut_in_bindings_back bindings3) + else + match new_msg with + | betree.Message.Insert v => + do + let bindings2 ← betree.List.push_front bindings1 (key, v) + Result.ok (lookup_mut_in_bindings_back bindings2) + | betree.Message.Delete => + Result.ok (lookup_mut_in_bindings_back bindings1) + | betree.Message.Upsert s => + do + let v ← betree.upsert_update none s + let bindings2 ← betree.List.push_front bindings1 (key, v) + Result.ok (lookup_mut_in_bindings_back bindings2) + + def betree.Node.apply_messages_to_leaf_loop + (bindings : betree.List (Isize × Isize)) + (new_msgs : betree.List (Isize × betree.Message)) : + Result (betree.List (Isize × Isize)) + := + match new_msgs with + | betree.List.Cons new_msg new_msgs_tl => + do + let (i, m) := new_msg + let bindings1 ← betree.Node.apply_to_leaf bindings i m + betree.Node.apply_messages_to_leaf_loop bindings1 new_msgs_tl + | betree.List.Nil => Result.ok bindings + partial_fixpoint + + def betree.Node.apply_messages_to_leaf + (bindings : betree.List (Isize × Isize)) + (new_msgs : betree.List (Isize × betree.Message)) : + Result (betree.List (Isize × Isize)) + := + betree.Node.apply_messages_to_leaf_loop bindings new_msgs + + mutual def betree.Internal.flush + (self : betree.Internal) (params : betree.Params) + (node_id_cnt : betree.NodeIdCounter) + (content : betree.List (Isize × betree.Message)) (st : State) : + Result (State × ((betree.List (Isize × betree.Message)) × (betree.Internal + × betree.NodeIdCounter))) + := + do + let p ← betree.ListPairIsizeT.partition_at_pivot content self.pivot + let (msgs_left, msgs_right) := p + let len_left ← betree.List.len msgs_left + if len_left >= params.min_flush_size + then + do + let (st1, p1) ← + betree.Node.apply_messages self.left params node_id_cnt msgs_left st + let (n, node_id_cnt1) := p1 + let len_right ← betree.List.len msgs_right + if len_right >= params.min_flush_size + then + do + let (st2, p2) ← + betree.Node.apply_messages self.right params node_id_cnt1 msgs_right + st1 + let (n1, node_id_cnt2) := p2 + Result.ok (st2, (betree.List.Nil, (betree.Internal.mk self.id self.pivot + n n1, node_id_cnt2))) + else + Result.ok (st1, (msgs_right, (betree.Internal.mk self.id self.pivot n + self.right, node_id_cnt1))) + else + do + let (st1, p1) ← + betree.Node.apply_messages self.right params node_id_cnt msgs_right st + let (n, node_id_cnt1) := p1 + Result.ok (st1, (msgs_left, (betree.Internal.mk self.id self.pivot + self.left n, node_id_cnt1))) + partial_fixpoint + + def betree.Node.apply_messages + (self : betree.Node) (params : betree.Params) + (node_id_cnt : betree.NodeIdCounter) + (msgs : betree.List (Isize × betree.Message)) (st : State) : + Result (State × (betree.Node × betree.NodeIdCounter)) + := + match self with + | betree.Node.Internal node => + do + let (st1, content) ← betree.load_internal_node node.id st + let content1 ← betree.Node.apply_messages_to_internal content msgs + let num_msgs ← betree.List.len content1 + if num_msgs >= params.min_flush_size + then + do + let (st2, (content2, p)) ← + betree.Internal.flush node params node_id_cnt content1 st1 + let (node1, node_id_cnt1) := p + let (st3, _) ← betree.store_internal_node node1.id content2 st2 + Result.ok (st3, (betree.Node.Internal node1, node_id_cnt1)) + else + do + let (st2, _) ← betree.store_internal_node node.id content1 st1 + Result.ok (st2, (self, node_id_cnt)) + | betree.Node.Leaf node => + do + let (st1, content) ← betree.load_leaf_node node.id st + let content1 ← betree.Node.apply_messages_to_leaf content msgs + let len ← betree.List.len content1 + let i ← 2#isize * params.split_size + if len >= i + then + do + let (st2, (new_node, node_id_cnt1)) ← + betree.Leaf.split node content1 params node_id_cnt st1 + let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2 + Result.ok (st3, (betree.Node.Internal new_node, node_id_cnt1)) + else + do + let (st2, _) ← betree.store_leaf_node node.id content1 st1 + Result.ok (st2, (betree.Node.Leaf { node with size := len }, + node_id_cnt)) + partial_fixpoint + + end + + def betree.Node.apply + (self : betree.Node) (params : betree.Params) + (node_id_cnt : betree.NodeIdCounter) (key : Isize) (new_msg : betree.Message) + (st : State) : + Result (State × (betree.Node × betree.NodeIdCounter)) + := + betree.Node.apply_messages self params node_id_cnt (betree.List.Cons (key, + new_msg) betree.List.Nil) st + + def betree.BeTree.new + (min_flush_size : Isize) (split_size : Isize) (st : State) : + Result (State × betree.BeTree) + := + do + let node_id_cnt ← betree.NodeIdCounter.new + let (id, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (st1, _) ← betree.store_leaf_node id betree.List.Nil st + Result.ok (st1, + { + params := { min_flush_size, split_size }, + node_id_cnt := node_id_cnt1, + root := (betree.Node.Leaf { id, size := 0#isize }) + }) + + def betree.BeTree.apply + (self : betree.BeTree) (key : Isize) (msg : betree.Message) (st : State) : + Result (State × betree.BeTree) + := + do + let (st1, p) ← + betree.Node.apply self.root self.params self.node_id_cnt key msg st + let (n, nic) := p + Result.ok (st1, { self with node_id_cnt := nic, root := n }) + + def betree.BeTree.insert + (self : betree.BeTree) (key : Isize) (value : Isize) (st : State) : + Result (State × betree.BeTree) + := + betree.BeTree.apply self key (betree.Message.Insert value) st + + def betree.BeTree.delete + (self : betree.BeTree) (key : Isize) (st : State) : + Result (State × betree.BeTree) + := + betree.BeTree.apply self key betree.Message.Delete st + + def betree.BeTree.upsert + (self : betree.BeTree) (key : Isize) (upd : betree.UpsertFunState) (st : State) + : + Result (State × betree.BeTree) + := + betree.BeTree.apply self key (betree.Message.Upsert upd) st + + def betree.BeTree.lookup + (self : betree.BeTree) (key : Isize) (st : State) : + Result (State × ((Option Isize) × betree.BeTree)) + := + do + let (st1, (o, n)) ← betree.Node.lookup self.root key st + Result.ok (st1, (o, { self with root := n })) + +end betree + +namespace avl + + inductive Ordering where + | Less : Ordering + | Equal : Ordering + | Greater : Ordering + + structure Ord (Self : Type) where + cmp : Self → Self → Result Ordering + + inductive Node (T : Type) where + | mk : T → Option (Node T) → Option (Node T) → Isize → Node T + + @[reducible] + def Node.value {T : Type} (x : Node T) := + match x with | Node.mk x1 _ _ _ => x1 + + @[reducible] + def Node.left {T : Type} (x : Node T) := + match x with | Node.mk _ x1 _ _ => x1 + + @[reducible] + def Node.right {T : Type} (x : Node T) := + match x with | Node.mk _ _ x1 _ => x1 + + @[reducible] + def Node.balance_factor {T : Type} (x : Node T) := + match x with | Node.mk _ _ _ x1 => x1 + + structure Tree (T : Type) where + root : Option (Node T) + + def OrdIsize.cmp (self : Isize) (other : Isize) : Result Ordering := + if self < other + then Result.ok Ordering.Less + else + if self = other + then Result.ok Ordering.Equal + else Result.ok Ordering.Greater + + /- Trait implementation: [avl::{avl::Ord for Isize}] + Source: 'src/avl.rs', lines 7:0-17:1 -/ + @[reducible] + def OrdIsize : Ord Isize := { + cmp := OrdIsize.cmp + } + + /- [avl::{avl::Node}#1::rotate_left]: + Source: 'src/avl.rs', lines 41:4-90:5 -/ + def Node.rotate_left + {T : Type} (root : Node T) (z : Node T) : Result (Node T) := + let (b, o) := core.mem.replace z.left none + let (x, root1) := + core.mem.replace (Node.mk root.value root.left b root.balance_factor) + (Node.mk z.value o z.right z.balance_factor) + if root1.balance_factor = 0#isize + then + Result.ok (Node.mk root1.value (some (Node.mk x.value x.left x.right 1#isize)) + root1.right (-1)#isize) + else + Result.ok (Node.mk root1.value (some (Node.mk x.value x.left x.right 0#isize)) + root1.right 0#isize) + + /- [avl::{avl::Node}#1::rotate_right]: + Source: 'src/avl.rs', lines 92:4-136:5 -/ + def Node.rotate_right + {T : Type} (root : Node T) (z : Node T) : Result (Node T) := + let (b, o) := core.mem.replace z.right none + let (x, root1) := + core.mem.replace (Node.mk root.value b root.right root.balance_factor) + (Node.mk z.value z.left o z.balance_factor) + if root1.balance_factor = 0#isize + then + Result.ok (Node.mk root1.value root1.left (some (Node.mk x.value + x.left x.right (-1)#isize)) 1#isize) + else + Result.ok (Node.mk root1.value root1.left (some (Node.mk x.value + x.left x.right 0#isize)) 0#isize) + + /- [avl::{avl::Node}#1::rotate_left_right]: + Source: 'src/avl.rs', lines 138:4-186:5 -/ + def Node.rotate_left_right + {T : Type} (root : Node T) (z : Node T) : Result (Node T) := + do + let (o, _) := core.mem.replace z.right none + let y ← core.option.Option.unwrap o + let (a, o1) := core.mem.replace y.left none + let (b, o2) := core.mem.replace y.right none + let (x, root1) := + core.mem.replace (Node.mk root.value b root.right root.balance_factor) + (Node.mk y.value o1 o2 y.balance_factor) + if root1.balance_factor = 0#isize + then + Result.ok (Node.mk root1.value (some (Node.mk z.value z.left a 0#isize)) (some + (Node.mk x.value x.left x.right 0#isize)) 0#isize) + else + if root1.balance_factor < 0#isize + then + Result.ok (Node.mk root1.value (some (Node.mk z.value z.left a 0#isize)) + (some (Node.mk x.value x.left x.right 1#isize)) 0#isize) + else + Result.ok (Node.mk root1.value (some (Node.mk z.value z.left a (-1)#isize)) + (some (Node.mk x.value x.left x.right 0#isize)) 0#isize) + + /- [avl::{avl::Node}#1::rotate_right_left]: + Source: 'src/avl.rs', lines 188:4-236:5 -/ + def Node.rotate_right_left + {T : Type} (root : Node T) (z : Node T) : Result (Node T) := + do + let (o, _) := core.mem.replace z.left none + let y ← core.option.Option.unwrap o + let (b, o1) := core.mem.replace y.left none + let (a, o2) := core.mem.replace y.right none + let (x, root1) := + core.mem.replace (Node.mk root.value root.left b root.balance_factor) + (Node.mk y.value o1 o2 y.balance_factor) + if root1.balance_factor = 0#isize + then + Result.ok (Node.mk root1.value (some (Node.mk x.value x.left x.right 0#isize)) + (some (Node.mk z.value a z.right 0#isize)) 0#isize) + else + if root1.balance_factor > 0#isize + then + Result.ok (Node.mk root1.value (some (Node.mk x.value x.left x.right + (-1)#isize)) (some (Node.mk z.value a z.right 0#isize)) 0#isize) + else + Result.ok (Node.mk root1.value (some (Node.mk x.value x.left x.right + 0#isize)) (some (Node.mk z.value a z.right 1#isize)) 0#isize) + + /- [avl::{avl::Node}#2::insert_in_left]: + Source: 'src/avl.rs', lines 240:4-275:5 -/ + mutual def Node.insert_in_left + {T : Type} (OrdInst : Ord T) (node : Node T) (value : T) : + Result (Bool × (Node T)) + := + do + let (b, o) ← Tree.insert_in_opt_node OrdInst node.left value + if b + then + do + let i ← node.balance_factor - 1#isize + if i = (-2)#isize + then + do + let (o1, o2) := core.mem.replace o none + let left ← core.option.Option.unwrap o1 + if left.balance_factor <= 0#isize + then + do + let node1 ← + Node.rotate_right (Node.mk node.value o2 node.right i) left + Result.ok (false, node1) + else + do + let node1 ← + Node.rotate_left_right (Node.mk node.value o2 node.right i) left + Result.ok (false, node1) + else Result.ok (i != 0#isize, Node.mk node.value o node.right i) + else Result.ok (false, Node.mk node.value o node.right node.balance_factor) + partial_fixpoint + + def Tree.insert_in_opt_node + {T : Type} (OrdInst : Ord T) (node : Option (Node T)) (value : T) : + Result (Bool × (Option (Node T))) + := + match node with + | none => let n := Node.mk value none none 0#isize + Result.ok (true, some n) + | some node1 => + do + let (b, node2) ← Node.insert OrdInst node1 value + Result.ok (b, some node2) + partial_fixpoint + + def Node.insert_in_right + {T : Type} (OrdInst : Ord T) (node : Node T) (value : T) : + Result (Bool × (Node T)) + := + do + let (b, o) ← Tree.insert_in_opt_node OrdInst node.right value + if b + then + do + let i ← node.balance_factor + 1#isize + if i = 2#isize + then + do + let (o1, o2) := core.mem.replace o none + let right ← core.option.Option.unwrap o1 + if right.balance_factor >= 0#isize + then + do + let node1 ← + Node.rotate_left (Node.mk node.value node.left o2 i) right + Result.ok (false, node1) + else + do + let node1 ← + Node.rotate_right_left (Node.mk node.value node.left o2 i) right + Result.ok (false, node1) + else Result.ok (i != 0#isize, Node.mk node.value node.left o i) + else Result.ok (false, Node.mk node.value node.left o node.balance_factor) + partial_fixpoint + + def Node.insert + {T : Type} (OrdInst : Ord T) (node : Node T) (value : T) : + Result (Bool × (Node T)) + := + do + let ordering ← OrdInst.cmp value node.value + match ordering with + | Ordering.Less => Node.insert_in_left OrdInst node value + | Ordering.Equal => Result.ok (false, node) + | Ordering.Greater => Node.insert_in_right OrdInst node value + partial_fixpoint + + end + + def Tree.new {T : Type} (_OrdInst : Ord T) : Result (Tree T) := + Result.ok { root := none } + + def Tree.find_loop + {T : Type} (OrdInst : Ord T) (value : T) (current_tree : Option (Node T)) : + Result Bool + := + match current_tree with + | none => Result.ok false + | some current_node => + do + let o ← OrdInst.cmp current_node.value value + match o with + | Ordering.Less => Tree.find_loop OrdInst value current_node.right + | Ordering.Equal => Result.ok true + | Ordering.Greater => Tree.find_loop OrdInst value current_node.left + partial_fixpoint + + def Tree.find + {T : Type} (OrdInst : Ord T) (self : Tree T) (value : T) : Result Bool := + Tree.find_loop OrdInst value self.root + + def Tree.insert + {T : Type} (OrdInst : Ord T) (self : Tree T) (value : T) : + Result (Bool × (Tree T)) + := + do + let (b, o) ← Tree.insert_in_opt_node OrdInst self.root value + Result.ok (b, { root := o }) + +end avl diff --git a/tests/lean/run/partial_fixpoint_coinductive_pred.lean b/tests/lean/run/partial_fixpoint_coinductive_pred.lean new file mode 100644 index 0000000000..6cb5861649 --- /dev/null +++ b/tests/lean/run/partial_fixpoint_coinductive_pred.lean @@ -0,0 +1,97 @@ +/-! +Johannes Hölzl pointed out that the `partial_fixpoint` machinery can be applied to `Prop` to define +inductive or (when using the dual order) coinductive predicates. + +Without an induction principle this isn't so useful, though. +-/ + +open Lean.Order + +instance : PartialOrder Prop where + rel x y := y → x -- NB: Dual + rel_refl := fun x => x + rel_trans h₁ h₂ := fun x => h₁ (h₂ x) + rel_antisymm h₁ h₂ := propext ⟨h₂, h₁⟩ + +instance : CCPO Prop where + csup c := ∀ p, c p → p + csup_spec := fun _ => + ⟨fun h y hcy hx => h hx y hcy, fun h hx y hcy => h y hcy hx ⟩ + +@[partial_fixpoint_monotone] theorem monotone_exists + {α} [PartialOrder α] {β} (f : α → β → Prop) + (h : monotone f) : + monotone (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 monotone_and + {α} [PartialOrder α] (f₁ : α → Prop) (f₂ : α → Prop) + (h₁ : monotone f₁) (h₂ : monotone f₂) : + monotone (fun x => f₁ x ∧ f₂ x) := + fun x y hxy ⟨hfx₁, hfx₂⟩ => ⟨h₁ x y hxy hfx₁, h₂ x y hxy hfx₂⟩ + +def univ (n : Nat) : Prop := + univ (n + 1) +partial_fixpoint + +/- +The following models a coinductive predicate defined as +``` +coinductive infinite_chain step : α → Prop where +| intro : ∀ y x, step x = some y → infinite_chain step y → infinite_chain step +``` +-/ +def infinite_chain {α} (step : α → Option α) (x : α) : Prop := + ∃ y, step x = some y ∧ infinite_chain step y +partial_fixpoint + +theorem infinite_chain.intro {α} (step : α → Option α) (y x : α) : + step x = some y → infinite_chain step y → infinite_chain step x := by + intros; unfold infinite_chain; simp [*] + +theorem infinite_chain.coinduct {α} (P : α → Prop) (step : α → Option α) + (h : ∀ (x : α), P x → ∃ y, step x = some y ∧ P y) : + ∀ x, P x → infinite_chain step x := by + apply infinite_chain.fixpoint_induct step + (motive := fun i => ∀ (x : α), P x → i x) + case adm => + clear h step + apply admissible_pi + intro a + intro c hchain h hPa Q ⟨f, hcf, hfaQ⟩ + subst Q + apply h f hcf hPa + case h => + intro ic hPic x hPx + obtain ⟨y, hstepx, h⟩ := h x hPx + exact ⟨y, hstepx, hPic y h⟩ + +/-- +Isabelle generates a stronger coinduction theorem from +``` +coinductive infinite_chain :: "('a ⇒ 'a option) ⇒ 'a ⇒ bool" for step :: "'a ⇒ 'a option" where + intro: "infinite_chain step x" if "step x = Some y" and "infinite_chain step y" +``` +Note the occurrence of `infinite_chain` in the step: +``` + Scratch.infinite_chain.coinduct: + ?X ?x ⟹ + (⋀x. ?X x ⟹ ∃xa y. x = xa ∧ ?step xa = Some y ∧ (?X y ∨ infinite_chain ?step y)) ⟹ + infinite_chain ?step ?x +``` +We can prove that from the one above. +-/ +theorem infinite_chain.coinduct_strong {α} (P : α → Prop) (step : α → Option α) + (h : ∀ (x : α), P x → ∃ y, step x = some y ∧ (P y ∨ infinite_chain step y)) : + ∀ x, P x → infinite_chain step x := by + suffices ∀ x, (P x ∨ infinite_chain step x) → infinite_chain step x by + intro x hPx + exact this x (.inl hPx) + apply infinite_chain.coinduct + intro x hor + cases hor + next hPx => exact h _ hPx + next hicx => + unfold infinite_chain at hicx + obtain ⟨y, hstepx, h⟩ := hicx + exact ⟨y, hstepx, .inr h⟩ diff --git a/tests/lean/run/partial_fixpoint_explicit.lean b/tests/lean/run/partial_fixpoint_explicit.lean new file mode 100644 index 0000000000..99c38fcc7c --- /dev/null +++ b/tests/lean/run/partial_fixpoint_explicit.lean @@ -0,0 +1,64 @@ +/-! +Tests for `partial_fixpoint` with explicit proofs +-/ + +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +def nullary (x : Nat) : Option Unit := nullary (x + 1) +partial_fixpoint monotonicity sorry + +-- Check for metavariables + +set_option pp.mvars.anonymous false in +/-- +error: don't know how to synthesize placeholder for argument 'a' +context: +⊢ Lean.Order.monotone fun f x => f (x + 1) +-/ +#guard_msgs in +def nullarya (x : Nat) : Option Unit := nullarya (x + 1) +partial_fixpoint monotonicity id _ + +def nullaryb (x : Nat) : Option Unit := nullaryb (x + 1) +partial_fixpoint monotonicity fun _ _ a _ => a _ + +/-- info: nullaryb.eq_1 (x : Nat) : nullaryb x = nullaryb (x + 1) -/ +#guard_msgs in #check nullaryb.eq_1 + +-- Type error + +/-- +error: type mismatch + () +has type + Unit : Type +but is expected to have type + Lean.Order.monotone fun f x => f (x + 1) : Prop +-/ +#guard_msgs in +def nullary2 (x : Nat) : Option Unit := nullary2 (x + 1) +partial_fixpoint monotonicity () + + +-- Good indent (bad indents are tested in partial_fixpoint_parseerrors + +def nullary4 (x : Nat) : Option Unit := nullary4 (x + 1) +partial_fixpoint monotonicity + fun _ _ a x => a (x + 1) + + +-- Tactics + +/-- info: Try this: exact fun x y a x => a (x + 1) -/ +#guard_msgs in +def nullary6 (x : Nat) : Option Unit := nullary6 (x + 1) +partial_fixpoint monotonicity by + exact? + +#guard_msgs in +def nullary7 (x : Nat) : Option Unit := nullary7 (x + 1) +partial_fixpoint monotonicity by + apply Lean.Order.monotone_of_monotone_apply + intro y + apply Lean.Order.monotone_apply + apply Lean.Order.monotone_id diff --git a/tests/lean/run/partial_fixpoint_induct.lean b/tests/lean/run/partial_fixpoint_induct.lean new file mode 100644 index 0000000000..d0a5f4e6cc --- /dev/null +++ b/tests/lean/run/partial_fixpoint_induct.lean @@ -0,0 +1,195 @@ +def loop (x : Nat) : Unit := loop (x + 1) +partial_fixpoint + +/-- +info: loop.fixpoint_induct (motive : (Nat → Unit) → Prop) (adm : Lean.Order.admissible motive) + (h : ∀ (loop : Nat → Unit), motive loop → motive fun x => loop (x + 1)) : motive loop +-/ +#guard_msgs in #check loop.fixpoint_induct + + +/-- error: unknown constant 'loop.partial_correctness' -/ +#guard_msgs in #check loop.partial_correctness + + +def find (P : Nat → Bool) (x : Nat) : Option Nat := + if P x then + some x + else + find P (x +1) +partial_fixpoint + +/-- +info: find.fixpoint_induct (P : Nat → Bool) (motive : (Nat → Option Nat) → Prop) (adm : Lean.Order.admissible motive) + (h : ∀ (find : Nat → Option Nat), motive find → motive fun x => if P x = true then some x else find (x + 1)) : + motive (find P) +-/ +#guard_msgs in #check find.fixpoint_induct + +/-- +info: find.partial_correctness (P : Nat → Bool) (motive : Nat → Nat → Prop) + (h : + ∀ (find : Nat → Option Nat), + (∀ (x r : Nat), find x = some r → motive x r) → + ∀ (x r : Nat), (if P x = true then some x else find (x + 1)) = some r → motive x r) + (x r✝ : Nat) : find P x = some r✝ → motive x r✝ +-/ +#guard_msgs in #check find.partial_correctness + +def fib (n : Nat) := go 0 0 1 +where + go i fip fi := + if i = n then + fi + else + go (i + 1) fi (fi + fip) + partial_fixpoint + +/-- +info: fib.go.fixpoint_induct (n : Nat) (motive : (Nat → Nat → Nat → Nat) → Prop) (adm : Lean.Order.admissible motive) + (h : + ∀ (go : Nat → Nat → Nat → Nat), motive go → motive fun i fip fi => if i = n then fi else go (i + 1) fi (fi + fip)) : + motive (fib.go n) +-/ +#guard_msgs in #check fib.go.fixpoint_induct + + +local instance (b : Bool) [Nonempty α] [Nonempty β] : Nonempty (cond b α β) := by + cases b <;> assumption +local instance (b : Bool) [Nonempty α] [Nonempty β] : Nonempty (if b then α else β) := by + split <;> assumption + +mutual +def dependent2''a (m n : Nat) (b : Bool) : if b then Nat else Bool := + if _ : b then dependent2''a m (n + 1) b else dependent2''b m m (n + m) b +partial_fixpoint +def dependent2''b (m k n : Nat) (b : Bool) : if b then Nat else Bool := + if b then dependent2''b m k n b else dependent2''c m (.last _) (n + m) b +partial_fixpoint +def dependent2''c (m : Nat) (i : Fin (m+1)) (n : Nat) (b : Bool) : if b then Nat else Bool := + if b then dependent2''c m i n b else dependent2''a m i b +partial_fixpoint +end + +/-- +info: dependent2''a.fixpoint_induct (m : Nat) (motive_1 : (Nat → (b : Bool) → if b = true then Nat else Bool) → Prop) + (motive_2 : (Nat → Nat → (b : Bool) → if b = true then Nat else Bool) → Prop) + (motive_3 : (Fin (m + 1) → Nat → (b : Bool) → if b = true then Nat else Bool) → Prop) + (adm_1 : Lean.Order.admissible motive_1) (adm_2 : Lean.Order.admissible motive_2) + (adm_3 : Lean.Order.admissible motive_3) + (h_1 : + ∀ (dependent2''a : Nat → (b : Bool) → if b = true then Nat else Bool) + (dependent2''b : Nat → Nat → (b : Bool) → if b = true then Nat else Bool), + motive_1 dependent2''a → + motive_2 dependent2''b → + motive_1 fun n b => if x : b = true then dependent2''a (n + 1) b else dependent2''b m (n + m) b) + (h_2 : + ∀ (dependent2''b : Nat → Nat → (b : Bool) → if b = true then Nat else Bool) + (dependent2''c : Fin (m + 1) → Nat → (b : Bool) → if b = true then Nat else Bool), + motive_2 dependent2''b → + motive_3 dependent2''c → + motive_2 fun k n b => if b = true then dependent2''b k n b else dependent2''c (Fin.last m) (n + m) b) + (h_3 : + ∀ (dependent2''a : Nat → (b : Bool) → if b = true then Nat else Bool) + (dependent2''c : Fin (m + 1) → Nat → (b : Bool) → if b = true then Nat else Bool), + motive_1 dependent2''a → + motive_3 dependent2''c → motive_3 fun i n b => if b = true then dependent2''c i n b else dependent2''a (↑i) b) : + motive_1 (dependent2''a m) ∧ motive_2 (dependent2''b m) ∧ motive_3 (dependent2''c m) +-/ +#guard_msgs in #check dependent2''a.fixpoint_induct + +/-- error: unknown constant 'dependent2''b.fixpoint_induct' -/ +#guard_msgs in #check dependent2''b.fixpoint_induct + + +mutual +def dependent3''a (m n : Nat) (b : Bool) : Option (if b then Nat else Bool) := + if _ : b then dependent3''a m (n + 1) b else dependent3''b m m (n + m) b +partial_fixpoint +def dependent3''b (m k n : Nat) (b : Bool) : Option (if b then Nat else Bool) := + if b then dependent3''b m k n b else dependent3''c m (.last _) (n + m) b +partial_fixpoint +def dependent3''c (m : Nat) (i : Fin (m+1)) (n : Nat) (b : Bool) : Option (if b then Nat else Bool) := + if b then dependent3''c m i n b else dependent3''a m i b +partial_fixpoint +end + +/-- +info: dependent3''a.partial_correctness (m : Nat) (motive_1 : Nat → (b : Bool) → (if b = true then Nat else Bool) → Prop) + (motive_2 : Nat → Nat → (b : Bool) → (if b = true then Nat else Bool) → Prop) + (motive_3 : Fin (m + 1) → Nat → (b : Bool) → (if b = true then Nat else Bool) → Prop) + (h_1 : + ∀ (dependent3''a : Nat → (b : Bool) → Option (if b = true then Nat else Bool)) + (dependent3''b : Nat → Nat → (b : Bool) → Option (if b = true then Nat else Bool)), + (∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''a n b = some r → motive_1 n b r) → + (∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool), + dependent3''b k n b = some r → motive_2 k n b r) → + ∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), + (if x : b = true then dependent3''a (n + 1) b else dependent3''b m (n + m) b) = some r → motive_1 n b r) + (h_2 : + ∀ (dependent3''b : Nat → Nat → (b : Bool) → Option (if b = true then Nat else Bool)) + (dependent3''c : Fin (m + 1) → Nat → (b : Bool) → Option (if b = true then Nat else Bool)), + (∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''b k n b = some r → motive_2 k n b r) → + (∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), + dependent3''c i n b = some r → motive_3 i n b r) → + ∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool), + (if b = true then dependent3''b k n b else dependent3''c (Fin.last m) (n + m) b) = some r → + motive_2 k n b r) + (h_3 : + ∀ (dependent3''a : Nat → (b : Bool) → Option (if b = true then Nat else Bool)) + (dependent3''c : Fin (m + 1) → Nat → (b : Bool) → Option (if b = true then Nat else Bool)), + (∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''a n b = some r → motive_1 n b r) → + (∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), + dependent3''c i n b = some r → motive_3 i n b r) → + ∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), + (if b = true then dependent3''c i n b else dependent3''a (↑i) b) = some r → motive_3 i n b r) : + (∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''a m n b = some r → motive_1 n b r) ∧ + (∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''b m k n b = some r → motive_2 k n b r) ∧ + ∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), + dependent3''c m i n b = some r → motive_3 i n b r +-/ +#guard_msgs in #check dependent3''a.partial_correctness + +-- The following example appears in the manual; having it here alerts us early of breakage + +def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with + | [] => none + | x::ys => + if p x then + some 0 + else + (· + 1) <$> List.findIndex ys p +partial_fixpoint + +/-- +info: List.findIndex.partial_correctness.{u_1} {α : Type u_1} (motive : List α → (α → Bool) → Nat → Prop) + (h : + ∀ (findIndex : List α → (α → Bool) → Option Nat), + (∀ (xs : List α) (p : α → Bool) (r : Nat), findIndex xs p = some r → motive xs p r) → + ∀ (xs : List α) (p : α → Bool) (r : Nat), + (match xs with + | [] => none + | x :: ys => if p x = true then some 0 else (fun x => x + 1) <$> findIndex ys p) = + some r → + motive xs p r) + (xs : List α) (p : α → Bool) (r✝ : Nat) : xs.findIndex p = some r✝ → motive xs p r✝ +-/ +#guard_msgs in +#check List.findIndex.partial_correctness + +theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) : + xs.findIndex p = some i → xs[i]?.any p := by + apply List.findIndex.partial_correctness (motive := fun xs p i => xs[i]?.any p) + intro findIndex ih xs p r hsome + split at hsome + next => contradiction + next x ys => + split at hsome + next => + have : r = 0 := by simp_all + simp_all + next => + simp only [Option.map_eq_map, Option.map_eq_some'] at hsome + obtain ⟨r', hr, rfl⟩ := hsome + specialize ih _ _ _ hr + simpa diff --git a/tests/lean/run/partial_fixpoint_monotonicity.lean b/tests/lean/run/partial_fixpoint_monotonicity.lean index b6dee1799c..d3513a2055 100644 --- a/tests/lean/run/partial_fixpoint_monotonicity.lean +++ b/tests/lean/run/partial_fixpoint_monotonicity.lean @@ -1,12 +1,5 @@ -- Tests the `monotonicity` tactic --- These can move to Init after a stage0 update -open Lean.Order in -attribute [partial_fixpoint_monotone] - monotone_ite - monotone_dite - monotone_bind - /- Should test that the tactic syntax is scoped, but cannot use #guard_msgs to catch “tactic not known” errors, it seems: @@ -27,3 +20,18 @@ example : monotone (fun (f : Nat → Option Unit) => do {do f 1; f 2; f 3}) := b example : monotone (fun (f : Option Unit) => do {do f; f; f}) := by repeat monotonicity + +example : monotone + (fun (f : Nat → Option Unit) => do + for x in [1,2,3] do f x) := by + repeat' monotonicity + +example : monotone + (fun (f : Nat → Option Nat) => do + let mut acc := 0 + for x in [1,2,3] do + acc := acc + (← f x) + if acc > 10 then + return 5 + pure acc) := by + repeat' monotonicity diff --git a/tests/lean/run/partial_fixpoint_mutual.lean b/tests/lean/run/partial_fixpoint_mutual.lean new file mode 100644 index 0000000000..b46d6b60ba --- /dev/null +++ b/tests/lean/run/partial_fixpoint_mutual.lean @@ -0,0 +1,36 @@ +axiom A : Type +axiom B : Type + +axiom A.toB : A → B +axiom B.toA : B → A + +open Lean.Order + +instance : PartialOrder A := sorry +-- It’s important that the CCPO instance isn't completely axiomatic, so that +-- `instCCPO.toOrder` is defeq to `instOrder` +instance : CCPO A where + csup := sorry + csup_spec := sorry +instance : PartialOrder B := sorry +instance : CCPO B where + csup := sorry + csup_spec := sorry + +@[partial_fixpoint_monotone] axiom monotone_toA : + ∀ {α} [PartialOrder α] (f : α → B), monotone f → monotone (fun x => B.toA (f x)) +@[partial_fixpoint_monotone] axiom monotone_toB : + ∀ {α} [PartialOrder α] (f : α → A), monotone f → monotone (fun x => A.toB (f x)) + +mutual +noncomputable def f : A := g.toA +partial_fixpoint +noncomputable def g : B := f.toB +partial_fixpoint +end + +/-- +info: equations: +theorem f.eq_1 : f = g.toA +-/ +#guard_msgs in #print equations f diff --git a/tests/lean/run/partial_fixpoint_probability.lean b/tests/lean/run/partial_fixpoint_probability.lean new file mode 100644 index 0000000000..33d6509392 --- /dev/null +++ b/tests/lean/run/partial_fixpoint_probability.lean @@ -0,0 +1,135 @@ +-- Since we do not have ENNReal in core, we just axiomatize it all for this test + +opaque ENNReal : Type + +axiom ENNReal.sup : ∀ {α}, (α → ENNReal) → ENNReal +axiom ENNReal.sum : ∀ {α}, (α → ENNReal) → ENNReal +axiom ENNReal.add : ENNReal → ENNReal → ENNReal +axiom ENNReal.mul : ENNReal → ENNReal → ENNReal + +noncomputable instance : Add ENNReal where add := .add +noncomputable instance : Mul ENNReal where mul := .mul +@[instance] axiom ENNReal.zero : Zero ENNReal +axiom ENNReal.one : ENNReal +axiom ENNReal.one_half : ENNReal + +@[simp] axiom ENNReal.mul_one : ∀ x, x * ENNReal.one = x +@[simp] axiom ENNReal.mul_zero : ∀ (x : ENNReal), x * 0 = 0 +@[simp] axiom ENNReal.add_zero : ∀ (x : ENNReal), x + 0 = x +@[simp] axiom ENNReal.zero_add : ∀ (x : ENNReal), 0 + x = x +@[simp] axiom ENNReal.sum_bool : ∀ f, sum f = f true + f false +@[simp] axiom ENNReal.sum_const_zero : ∀ α, ENNReal.sum (fun (_ : α) => 0) = 0 +@[simp] axiom ENNReal.sum_dirac : ∀ α [DecidableEq α] (f : α → ENNReal) y, + ENNReal.sum (fun x => if x = y then f x else 0) = f y + +@[instance] axiom ENNReal.le : LE ENNReal +axiom ENNReal.le_refl : ∀ (x : ENNReal), x ≤ x +axiom ENNReal.le_trans : ∀ {x y z: ENNReal}, x ≤ y → y ≤ z → x ≤ z +axiom ENNReal.le_antisymm : ∀ {x y : ENNReal}, x ≤ y → y ≤ x → x = y + +section +set_option linter.unusedVariables false +axiom ENNReal.sum_mono : ∀ {α} (s₁ s₂ : α → ENNReal) (h : ∀ x, s₁ x ≤ s₂ x), + ENNReal.sum s₁ ≤ ENNReal.sum s₂ +axiom ENNReal.sup_mono : ∀ {α} (s₁ s₂ : α → ENNReal) (h : ∀ x, s₁ x ≤ s₂ x), + ENNReal.sup s₁ ≤ ENNReal.sup s₂ +axiom ENNReal.mul_mono : ∀ (a b c Distr : ENNReal) (h₁ : a ≤ c) (h₂ : b ≤ Distr), + a * b ≤ c * Distr + +axiom ENNReal.le_sup : ∀ {α} (a : ENNReal) (s : α → ENNReal) (i : α) (h : a ≤ s i), + a ≤ ENNReal.sup s +axiom ENNReal.sup_le : ∀ {α} (a : ENNReal) (s : α → ENNReal) (h : ∀ (i : α), s i ≤ a), + ENNReal.sup s ≤ a +end + + +/-- Distribtions (not normalized, which is curcial, else we don't have ⊥.) -/ +def Distr (α : Type) : Type := α → ENNReal + +noncomputable def Distr.join : Distr (Distr α) → Distr α := fun dd x => + ENNReal.sum (fun Distr => Distr x * dd Distr ) + +noncomputable instance : Functor Distr where + map f Distr := fun x => ENNReal.sum (fun y => open Classical in if f y = x then Distr y else 0) + +noncomputable instance : Pure Distr where + pure x := fun y => open Classical in if x = y then .one else 0 + +noncomputable instance : Bind Distr where + bind Distr f := fun x => ENNReal.sum (fun y => Distr y * f y x) + +open Lean.Order + +noncomputable instance : PartialOrder (Distr α) where + rel d1 d2 := ∀ x, d1 x ≤ d2 x + rel_refl _ := ENNReal.le_refl _ + rel_trans h1 h2 _ := ENNReal.le_trans (h1 _) (h2 _) + rel_antisymm h1 h2 := funext (fun _ => ENNReal.le_antisymm (h1 _) (h2 _)) + +noncomputable instance : CCPO (Distr α) where + csup c x := ENNReal.sup fun (Distr : Subtype c) => Distr.val x + csup_spec := by + intros d₁ c hchain + constructor + next => + intro h d₂ hd₂ x + apply ENNReal.le_trans ?_ (h x) + apply ENNReal.le_sup (i := ⟨d₂, hd₂⟩) + apply ENNReal.le_refl + next => + intro h x + apply ENNReal.sup_le + intros Distr + apply h Distr.1 Distr.2 x + +noncomputable instance : MonoBind Distr where + bind_mono_left := by + intro α β d₁ d₂ f h₁₂ y + unfold bind instBindDistr + dsimp + apply ENNReal.sum_mono + intro x + apply ENNReal.mul_mono + · apply h₁₂ + · apply ENNReal.le_refl + + bind_mono_right := by + intro α β Distr f₁ f₂ h₁₂ y + apply ENNReal.sum_mono + intro x + apply ENNReal.mul_mono + · apply ENNReal.le_refl + · apply h₁₂ + + +noncomputable def coin : Distr Bool := fun _ => .one_half + +noncomputable def geom : Distr Nat := do + let head ← coin + if head then + return 0 + else + let n ← geom + return (n + 1) +partial_fixpoint + +/-- +info: geom.eq_1 : + geom = do + let head ← coin + if head = true then pure 0 + else do + let n ← geom + pure (n + 1) +-/ +#guard_msgs in +#check geom.eq_1 + +-- And we can can do proofs about this + +theorem geom_0 : geom 0 = .one_half := by + rw [geom]; simp [bind, coin, pure] + +theorem geom_succ : geom (n+1) = .one_half * geom n := by + conv => lhs; rw [geom] + simp [bind, coin, pure, apply_ite] diff --git a/tests/lean/run/partial_fixpoint_split.lean b/tests/lean/run/partial_fixpoint_split.lean new file mode 100644 index 0000000000..5c02184647 --- /dev/null +++ b/tests/lean/run/partial_fixpoint_split.lean @@ -0,0 +1,22 @@ +/- +This test case explores the interaction between the `split` tactic and the +tailrecursion checking: + +If `split` would rewrite matches with identical targets together, and thus clear out +dead code, this would be accepted, despite a non-tailrecursive call there. +-/ + +/-- +error: Could not prove 'whileSome' to be monotone in its recursive calls: + Cannot eliminate recursive call `whileSome some x'` enclosed in + id (whileSome some x'✝) +-/ +#guard_msgs in +def whileSome (f : α → Option α) (x : α) : α := + match f x with + | none => x + | some x' => + match f x with + | none => id $ whileSome some x' + | some x' => whileSome f x' +partial_fixpoint diff --git a/tests/lean/termination_by.lean.expected.out b/tests/lean/termination_by.lean.expected.out index b438c7f682..88750dfc46 100644 --- a/tests/lean/termination_by.lean.expected.out +++ b/tests/lean/termination_by.lean.expected.out @@ -11,11 +11,11 @@ termination_by.lean:40:4-40:20: warning: unused `termination_by`, function is no termination_by.lean:44:4-44:20: warning: unused `termination_by`, function is not recursive termination_by.lean:54:2-54:18: warning: unused `termination_by`, function is not recursive termination_by.lean:62:2-62:23: error: incomplete set of `termination_by` annotations: -This function is mutually with isOdd, which does not have a `termination_by` clause. +This function is mutually recursive with isOdd, which does not have a `termination_by` clause. The present clause is ignored. Try this: termination_by x1 => x1 termination_by.lean:79:2-79:27: error: incomplete set of `termination_by` annotations: -This function is mutually with Test.f, Test.h and Test.i, which do not have a `termination_by` clause. +This function is mutually recursive with Test.f, Test.h and Test.i, which do not have a `termination_by` clause. The present clause is ignored. termination_by.lean:101:2-101:27: error: Invalid `termination_by`; this function is mutually recursive with Test2.f, which is marked as `termination_by structural` so this one also needs to be marked `structural`. termination_by.lean:120:2-120:38: error: Invalid `termination_by`; this function is mutually recursive with Test3.f, which is not marked as `structural` so this one cannot be `structural` either.