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

feat: partial_fixpoint: partial functions with equations (#6355)

Browse source 
This PR adds the ability to define possibly non-terminating functions
and still be able to reason about them equationally, as long as they are
tail-recursive or monadic.

Typical uses of this feature are
```lean4
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_fixpiont

def whileSome (f : α → Option α) (x : α) : α :=
  match f x with
  | none => x
  | some x' => whileSome f x'
partial_fixpiont

def computeLfp {α : Type u} [DecidableEq α] (f : α → α) (x : α) : α :=
  let next := f x
  if x ≠ next then
    computeLfp f next
  else
    x
partial_fixpiont

noncomputable def geom : Distr Nat := do
  let head ← coin
  if head then
    return 0
  else
    let n ← geom
    return (n + 1)
partial_fixpiont
```

This PR contains

* The necessary fragment of domain theory, up to (a variant of)
Knaster–Tarski theorem (merged as
https://github.com/leanprover/lean4/pull/6477)
* A tactic to solve monotonicity goals compositionally (a bit like
mathlib’s `fun_prop`) (merged as
https://github.com/leanprover/lean4/pull/6506)
* An attribute to extend that tactic (merged as
https://github.com/leanprover/lean4/pull/6506)
* A “derecursifier” that uses that machinery to define recursive
function, including support for dependent functions and mutual
recursion.
* Fixed-point induction principles (technical, tedious to use)
* For `Option`-valued functions: Partial correctness induction theorems
that hide all the domain theory

This is heavily inspired by [Isabelle’s `partial_function`
command](https://isabelle.in.tum.de/doc/codegen.pdf).
This commit is contained in:
Joachim Breitner 2025-01-21 10:54:30 +01:00 • committed by GitHub
parent edeae18f5e
commit 7b813d4f5d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
36 changed files with 4394 additions and 259 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Data/List/Control.lean
View file

@ -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 ..)

1
src/Init/Internal/Order.lean
View file

@ -5,4 +5,5 @@ Authors: Joachim Breitner
-/
prelude
import Init.Internal.Order.Basic
import Init.Internal.Order.Lemmas
import Init.Internal.Order.Tactic

46
src/Init/Internal/Order/Basic.lean
View file

@ -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

685
src/Init/Internal/Order/Lemmas.lean Normal file
View file

@ -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

40
src/Lean/Elab/PreDefinition/Main.lean
View file

@ -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

92
src/Lean/Elab/PreDefinition/Mutual.lean Normal file
View file

@ -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 <decl>]`
attribute would check whether the `unaryPreDef` type matches with `<decl>`'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

9
src/Lean/Elab/PreDefinition/PartialFixpoint.lean Normal file
View file

@ -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

117
src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean Normal file
View file

@ -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

292
src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean Normal file
View file

@ -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

188
src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean Normal file
View file

@ -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

2
src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
View file

@ -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

37
src/Lean/Elab/PreDefinition/TerminationHint.lean
View file

@ -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

18
src/Lean/Elab/PreDefinition/WF/Eqns.lean
View file

@ -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

113
src/Lean/Elab/PreDefinition/WF/Main.lean
View file

@ -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 <decl>]`
attribute would check whether the `unaryPreDef` type matches with `<decl>`'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

98
src/Lean/Elab/PreDefinition/WF/PackMutual.lean
View file

@ -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

25
src/Lean/Elab/Tactic/Monotonicity.lean
View file

@ -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

63
src/Lean/Meta/ArgsPacker.lean
View file

@ -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

13
src/Lean/Meta/Basic.lean
View file

@ -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

6
src/Lean/Meta/Constructions/BRecOn.lean
View file

@ -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

93
src/Lean/Meta/PProdN.lean
View file

@ -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

36
src/Lean/Meta/Tactic/FunInd.lean
View file

@ -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

1
src/Lean/Meta/Tactic/SplitIf.lean
View file

@ -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

36
src/Lean/Parser/Term.lean
View file

@ -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

17
tests/lean/partial_fixpoint_parseerrors.lean Normal file
View file

@ -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)

2
tests/lean/partial_fixpoint_parseerrors.lean.expected.out Normal file
View file

@ -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

401
tests/lean/run/partial_fixpoint.lean Normal file
View file

@ -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

149
tests/lean/run/partial_fixpoint_aeneas.lean Normal file
View file

@ -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

1497
tests/lean/run/partial_fixpoint_aeneas2.lean Normal file
View file

File diff suppressed because it is too large Load diff

97
tests/lean/run/partial_fixpoint_coinductive_pred.lean Normal file
View file

@ -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⟩

64
tests/lean/run/partial_fixpoint_explicit.lean Normal file
View file

@ -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

195
tests/lean/run/partial_fixpoint_induct.lean Normal file
View file

@ -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

22
tests/lean/run/partial_fixpoint_monotonicity.lean
View file

@ -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

36
tests/lean/run/partial_fixpoint_mutual.lean Normal file
View file

@ -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

135
tests/lean/run/partial_fixpoint_probability.lean Normal file
View file

@ -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]

22
tests/lean/run/partial_fixpoint_split.lean Normal file
View file

@ -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

4
tests/lean/termination_by.lean.expected.out
View file

@ -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.