chore: rename keywords for (co)inductive predicates and the names of their associated (co)induction principles
chore: rename `fixpoint_induct` to `induct` and `coinduct` for (co)inductive predicates
This commit is contained in:
Wojciech Rozowski
Joachim Breitner
parent
dd64678f07
commit
07c398e441
10 changed files with 124 additions and 107 deletions
|
|
@ -184,25 +184,25 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
|
|||
let preDefsWithout := preDefs.filter (·.termination.terminationBy?.isNone)
|
||||
let structural :=
|
||||
preDefWith.termination.terminationBy? matches some {structural := true, ..}
|
||||
-- Information whether the current one is partial, least or greatest
|
||||
let partialFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isPartial x.fixpointType
|
||||
let leastFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isLeast x.fixpointType
|
||||
let greatestFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isGreatest x.fixpointType
|
||||
-- Information whether the current one is partial, inductive or coinductive
|
||||
let partialFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isPartialFixpoint x.fixpointType
|
||||
let inductiveFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isInductiveFixpoint x.fixpointType
|
||||
let coinductiveFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isCoinductiveFixpoint x.fixpointType
|
||||
for preDef in preDefs do
|
||||
-- if some has at termination by clause
|
||||
if let .some termBy := preDef.termination.terminationBy? then
|
||||
-- but something in the clique is partial/least/greatest, then we report error
|
||||
-- but something in the clique is partial/inductive/coinductive, then we report error
|
||||
if let .some partialFixpointStx := preDef.termination.partialFixpoint? then
|
||||
match partialFixpointStx.fixpointType with
|
||||
| .partialFixpoint => throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \
|
||||
be both terminating and a partial fixpoint"
|
||||
| .leastFixpoint => throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \
|
||||
be both terminating and a least fixpoint"
|
||||
| .greatestFixpoint => throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \
|
||||
be both terminating and a greatest fixpoint"
|
||||
| .inductiveFixpoint => throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \
|
||||
be both terminating and an inductive fixpoint"
|
||||
| .coinductiveFixpoint => throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \
|
||||
be both terminating and a coinductive fixpoint"
|
||||
|
||||
-- if has no annotations
|
||||
if !structural && !partialFixpoint && !leastFixpoint && !greatestFixpoint && !preDefsWithout.isEmpty then
|
||||
if !structural && !partialFixpoint && !inductiveFixpoint && !coinductiveFixpoint && !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 hints:\n\
|
||||
|
|
@ -224,57 +224,57 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
|
|||
structurally recursive, so no explicit termination proof is needed."
|
||||
|
||||
-- If one is partial, but others are not
|
||||
if partialFixpoint && !preDef.termination.partialFixpoint?.any fun x => isPartial x.fixpointType then
|
||||
if partialFixpoint && !preDef.termination.partialFixpoint?.any fun x => isPartialFixpoint x.fixpointType then
|
||||
throwErrorAt preDef.ref m!"Incompatible termination hint; this function is mutually \
|
||||
recursive with {preDefWith.declName}, which is marked as \
|
||||
`partial_fixpoint` so this one also needs to be marked \
|
||||
`partial_fixpoint`."
|
||||
|
||||
-- If one is least, but others are not
|
||||
if leastFixpoint && !preDef.termination.partialFixpoint?.any fun x => isLatticeTheoretic x.fixpointType then
|
||||
if inductiveFixpoint && !preDef.termination.partialFixpoint?.any fun x => isLatticeTheoretic x.fixpointType then
|
||||
throwErrorAt preDef.ref m!"Incompatible termination hint; this function is mutually \
|
||||
recursive with {preDefWith.declName}, which is marked as
|
||||
`least_fixpoint` so this one also needs to be marked \
|
||||
`least_fixpoint` or `greatest_fixpoint`."
|
||||
`inductive_fixpoint` so this one also needs to be marked \
|
||||
`inductive_fixpoint` or `coinductive_fixpoint`."
|
||||
|
||||
-- If one is greatest, but others are not
|
||||
if greatestFixpoint && !preDef.termination.partialFixpoint?.any fun x => isLatticeTheoretic x.fixpointType then
|
||||
if coinductiveFixpoint && !preDef.termination.partialFixpoint?.any fun x => isLatticeTheoretic x.fixpointType then
|
||||
throwErrorAt preDef.ref m!"Incompatible termination hint; this function is mutually \
|
||||
recursive with {preDefWith.declName}, which is marked as \
|
||||
`greatest_fixpoint` so this one also needs to be marked \
|
||||
`least_fixpoint` or `greatest_fixpoint`."
|
||||
`coinductive_fixpoint` so this one also needs to be marked \
|
||||
`inductive_fixpoint` or `coinductive_fixpoint`."
|
||||
|
||||
-- checking for unnecessary `decreasing_by` clause
|
||||
if preDef.termination.partialFixpoint?.any fun x => isPartial x.fixpointType then
|
||||
if preDef.termination.partialFixpoint?.any fun x => isPartialFixpoint x.fixpointType then
|
||||
if let .some decr := preDef.termination.decreasingBy? then
|
||||
logErrorAt decr.ref m!"Invalid `decreasing_by`; this function is marked as \
|
||||
partial_fixpoint, so no explicit termination proof is needed."
|
||||
|
||||
if preDef.termination.partialFixpoint?.any fun x => isLeast x.fixpointType then
|
||||
if preDef.termination.partialFixpoint?.any fun x => isInductiveFixpoint x.fixpointType then
|
||||
if let .some decr := preDef.termination.decreasingBy? then
|
||||
logErrorAt decr.ref m!"Invalid `decreasing_by`; this function is marked as \
|
||||
least_fixpoint, so no explicit termination proof is needed."
|
||||
inductive_fixpoint, so no explicit termination proof is needed."
|
||||
|
||||
if preDef.termination.partialFixpoint?.any fun x => isLeast x.fixpointType then
|
||||
if preDef.termination.partialFixpoint?.any fun x => isInductiveFixpoint x.fixpointType then
|
||||
if let .some decr := preDef.termination.decreasingBy? then
|
||||
logErrorAt decr.ref m!"Invalid `decreasing_by`; this function is marked as \
|
||||
greatest_fixpoint, so no explicit termination proof is needed."
|
||||
coinductive_fixpoint, so no explicit termination proof is needed."
|
||||
|
||||
-- if the selected one is not marked as partial fixpoint
|
||||
if !partialFixpoint then
|
||||
if let some stx := preDef.termination.partialFixpoint? then
|
||||
if isPartial stx.fixpointType then
|
||||
if isPartialFixpoint stx.fixpointType then
|
||||
throwErrorAt stx.ref m!"Incompatible termination hint; this function is mutually \
|
||||
recursive with {preDefWith.declName}, which is not also marked as \
|
||||
`partial_fixpoint`, so this one cannot be either."
|
||||
|
||||
-- if the selected one is not marked as partial fixpoint
|
||||
unless leastFixpoint || greatestFixpoint do
|
||||
unless inductiveFixpoint || coinductiveFixpoint do
|
||||
if let some stx := preDef.termination.partialFixpoint? then
|
||||
if isLatticeTheoretic stx.fixpointType then
|
||||
throwErrorAt stx.ref m!"Incompatible termination hint; this function is mutually \
|
||||
recursive with {preDefWith.declName}, which is not also marked as \
|
||||
`least_fixpoint` or `greatest_fixpoint`, so this one cannot be either."
|
||||
`inductive_fixpoint` or `coinductive_fixpoint`, so this one cannot be either."
|
||||
|
||||
/--
|
||||
Elaborates the `TerminationHint` in the clique to `TerminationMeasures`
|
||||
|
|
|
|||
|
|
@ -53,14 +53,13 @@ def CCPOProdProjs (n : Nat) (inst : Expr) : Array Expr := Id.run do
|
|||
Unfolds an appropriate `PartialOrder` instance on predicates to quantifications and implications.
|
||||
I.e. `ImplicationOrder.instPartialOrder.rel P Q` becomes
|
||||
`∀ x y, P x y → Q x y`.
|
||||
|
||||
In the premise of the Park induction principle (`lfp_le_of_le_monotone`) we use a monotone map defining the predicate in the eta expanded form. In such a case, besides desugaring the predicate, we need to perform a weak head reduction.
|
||||
The optional parameter `reduceConclusion` (false by default) indicates whether we need to perform this reduction.
|
||||
-/
|
||||
def unfoldPredRel (predType : Expr) (body : Expr) (fixpointType : PartialFixpointType) (reduceConclusion : Bool := false) : MetaM Expr := do
|
||||
match fixpointType with
|
||||
| .partialFixpoint => throwError "Trying to apply lattice induction to a non-lattice fixpoint. Please report this issue."
|
||||
| .leastFixpoint | .greatestFixpoint =>
|
||||
| .inductiveFixpoint | .coinductiveFixpoint =>
|
||||
unless body.isAppOfArity ``PartialOrder.rel 4 do
|
||||
throwError "{body} is not an application of partial order"
|
||||
let lhsTypes ← forallTelescope predType fun ts _ => ts.mapM inferType
|
||||
|
|
@ -68,15 +67,15 @@ def unfoldPredRel (predType : Expr) (body : Expr) (fixpointType : PartialFixpoin
|
|||
let bodyArgs := body.getAppArgs
|
||||
withLocalDeclsDND (names.zip lhsTypes) fun exprs => do
|
||||
let mut applied := match fixpointType with
|
||||
| .leastFixpoint => (bodyArgs[2]!, bodyArgs[3]!)
|
||||
| .greatestFixpoint => (bodyArgs[3]!, bodyArgs[2]!)
|
||||
| .inductiveFixpoint => (bodyArgs[2]!, bodyArgs[3]!)
|
||||
| .coinductiveFixpoint => (bodyArgs[3]!, bodyArgs[2]!)
|
||||
| .partialFixpoint => panic! "Cannot apply lattice induction to a non-lattice fixpoint"
|
||||
for e in exprs do
|
||||
applied := (mkApp applied.1 e, mkApp applied.2 e)
|
||||
if reduceConclusion then
|
||||
match fixpointType with
|
||||
| .leastFixpoint => applied := ((←whnf applied.1), applied.2)
|
||||
| .greatestFixpoint => applied := (applied.1, (←whnf applied.2))
|
||||
| .inductiveFixpoint => applied := ((←whnf applied.1), applied.2)
|
||||
| .coinductiveFixpoint => applied := (applied.1, (←whnf applied.2))
|
||||
| .partialFixpoint => throwError "Cannot apply lattice induction to a non-lattice fixpoint"
|
||||
mkForallFVars exprs (←mkArrow applied.1 applied.2)
|
||||
|
||||
|
|
@ -93,8 +92,18 @@ 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 :=
|
||||
let inductName := name ++ `fixpoint_induct
|
||||
def getInductionPrinciplePostfix (name : Name) : MetaM Name := do
|
||||
let some eqnInfo := eqnInfoExt.find? (← getEnv) name | throwError "{name} is not defined by partial_fixpoint, inductive_fixpoint, nor coinductive_fixpoint"
|
||||
let idx := eqnInfo.declNames.idxOf name
|
||||
let some res := eqnInfo.fixpointType[idx]? | throwError "Cannot get fixpoint type for {name}"
|
||||
match res with
|
||||
| .partialFixpoint => return `fixpoint_induct
|
||||
| .inductiveFixpoint => return `induct
|
||||
| .coinductiveFixpoint => return `coinduct
|
||||
|
||||
def deriveInduction (name : Name) : MetaM Unit := do
|
||||
let postFix ← getInductionPrinciplePostfix name
|
||||
let inductName := name ++ postFix
|
||||
realizeConst name inductName do
|
||||
trace[Elab.definition.partialFixpoint] "Called deriveInduction for {inductName}"
|
||||
prependError m!"Cannot derive fixpoint induction principle (please report this issue)" do
|
||||
|
|
@ -250,7 +259,17 @@ def isInductName (env : Environment) (name : Name) : Bool := Id.run do
|
|||
match s with
|
||||
| "fixpoint_induct" =>
|
||||
if let some eqnInfo := eqnInfoExt.find? env p then
|
||||
return p == eqnInfo.declNames[0]!
|
||||
return p == eqnInfo.declNames[0]! && isPartialFixpoint (eqnInfo.fixpointType[0]!)
|
||||
return false
|
||||
| "coinduct" =>
|
||||
if let some eqnInfo := eqnInfoExt.find? env p then
|
||||
let idx := eqnInfo.declNames.idxOf p
|
||||
return isCoinductiveFixpoint eqnInfo.fixpointType[idx]!
|
||||
return false
|
||||
| "induct" =>
|
||||
if let some eqnInfo := eqnInfoExt.find? env p then
|
||||
let idx := eqnInfo.declNames.idxOf p
|
||||
return isInductiveFixpoint eqnInfo.fixpointType[idx]!
|
||||
return false
|
||||
| _ => return false
|
||||
|
||||
|
|
|
|||
|
|
@ -75,7 +75,7 @@ private def mkMonoPProd : (hmono₁ hmono₂ : Expr × Expr) → MetaM (Expr ×
|
|||
return (← inferType hmonoProof, hmonoProof)
|
||||
|
||||
def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
|
||||
-- We expect all functions in the clique to have `partial_fixpoint` or `greatest_fixpoint` syntax
|
||||
-- We expect all functions in the clique to have `partial_fixpoint`, `inductive_fixpoint` or `coinductive_fixpoint` syntax
|
||||
let hints := preDefs.filterMap (·.termination.partialFixpoint?)
|
||||
assert! preDefs.size = hints.size
|
||||
-- We check if any fixpoints were defined lattice-theoretically
|
||||
|
|
@ -90,13 +90,13 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
|
|||
let type ← instantiateForall preDef.type xs
|
||||
let inst ←
|
||||
match hints[i]!.fixpointType with
|
||||
| .greatestFixpoint =>
|
||||
| .coinductiveFixpoint =>
|
||||
unless type.isProp do
|
||||
throwError "`greatest_fixpoint` can be only used to define predicates"
|
||||
throwError "`coinductive_fixpoint` can be only used to define predicates"
|
||||
pure (mkConst ``ReverseImplicationOrder.instCompleteLattice)
|
||||
| .leastFixpoint =>
|
||||
| .inductiveFixpoint =>
|
||||
unless type.isProp do
|
||||
throwError "`least_fixpoint` can be only used to define predicates"
|
||||
throwError "`inductive_fixpoint` can be only used to define predicates"
|
||||
pure (mkConst ``ImplicationOrder.instCompleteLattice)
|
||||
| .partialFixpoint => try
|
||||
synthInstance (← mkAppM ``CCPO #[type])
|
||||
|
|
|
|||
|
|
@ -35,11 +35,11 @@ structure DecreasingBy where
|
|||
|
||||
inductive PartialFixpointType where
|
||||
| partialFixpoint
|
||||
| greatestFixpoint
|
||||
| leastFixpoint
|
||||
| coinductiveFixpoint
|
||||
| inductiveFixpoint
|
||||
deriving Inhabited
|
||||
|
||||
/-- A single `partial_fixpoint`, `greatest_fixpoint` or `least_fixpoint` clause -/
|
||||
/-- A single `partial_fixpoint`, `inductive_fixpoint` or `coinductive_fixpoint` clause -/
|
||||
structure PartialFixpoint where
|
||||
ref : Syntax
|
||||
term? : Option Term
|
||||
|
|
@ -69,20 +69,20 @@ structure TerminationHints where
|
|||
extraParams : Nat
|
||||
deriving Inhabited
|
||||
|
||||
def isLeast : PartialFixpointType → Bool
|
||||
| .leastFixpoint => true
|
||||
def isInductiveFixpoint : PartialFixpointType → Bool
|
||||
| .inductiveFixpoint => true
|
||||
| _ => false
|
||||
|
||||
def isGreatest : PartialFixpointType → Bool
|
||||
| .greatestFixpoint => true
|
||||
def isCoinductiveFixpoint : PartialFixpointType → Bool
|
||||
| .coinductiveFixpoint => true
|
||||
| _ => false
|
||||
|
||||
def isPartial : PartialFixpointType → Bool
|
||||
def isPartialFixpoint : PartialFixpointType → Bool
|
||||
| .partialFixpoint => true
|
||||
| _ => false
|
||||
|
||||
def isLatticeTheoretic (p : PartialFixpointType ) : Bool :=
|
||||
isLeast p ∨ isGreatest p
|
||||
def isLatticeTheoretic (p : PartialFixpointType) : Bool :=
|
||||
isInductiveFixpoint p ∨ isCoinductiveFixpoint p
|
||||
|
||||
def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, .none, 0⟩
|
||||
|
||||
|
|
@ -99,8 +99,8 @@ def TerminationHints.ensureNone (hints : TerminationHints) (reason : String) : C
|
|||
| .none, .none, .none, .some partialFixpoint =>
|
||||
match partialFixpoint.fixpointType with
|
||||
| .partialFixpoint => logWarningAt partialFixpoint.ref m!"unused `partial_fixpoint`, function is {reason}"
|
||||
| .greatestFixpoint => logWarningAt partialFixpoint.ref m!"unused `greatest_fixpoint`, function is {reason}"
|
||||
| .leastFixpoint => logWarningAt partialFixpoint.ref m!"unused `least_fixpoint`, function is {reason}"
|
||||
| .coinductiveFixpoint => logWarningAt partialFixpoint.ref m!"unused `coinductive_fixpoint`, function is {reason}"
|
||||
| .inductiveFixpoint => logWarningAt partialFixpoint.ref m!"unused `inductive_fixpoint`, function is {reason}"
|
||||
| _, _, _, _=>
|
||||
logWarningAt hints.ref m!"unused termination hints, function is {reason}"
|
||||
|
||||
|
|
@ -160,14 +160,14 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
|
|||
pure (some {ref := t, structural := s.isSome, vars := #[], body})
|
||||
| `(terminationBy?|termination_by?) => pure none
|
||||
| `(partialFixpoint|partial_fixpoint $[monotonicity $_]?) => pure none
|
||||
| `(greatestFixpoint|greatest_fixpoint $[monotonicity $_]?) => pure none
|
||||
| `(leastFixpoint|least_fixpoint $[monotonicity $_]?) => pure none
|
||||
| `(coinductiveFixpoint|coinductive_fixpoint $[monotonicity $_]?) => pure none
|
||||
| `(inductiveFixpoint|inductive_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?, fixpointType := .partialFixpoint})
|
||||
| `(greatestFixpoint|greatest_fixpoint $[monotonicity $term?]?) => pure (some {ref := t, term?, fixpointType := .greatestFixpoint})
|
||||
| `(leastFixpoint|least_fixpoint $[monotonicity $term?]?) => pure (some {ref := t, term?, fixpointType := .leastFixpoint})
|
||||
| `(coinductiveFixpoint|coinductive_fixpoint $[monotonicity $term?]?) => pure (some {ref := t, term?, fixpointType := .coinductiveFixpoint})
|
||||
| `(inductiveFixpoint|inductive_fixpoint $[monotonicity $term?]?) => pure (some {ref := t, term?, fixpointType := .inductiveFixpoint})
|
||||
| _ => pure none
|
||||
else pure none
|
||||
let decreasingBy? ← d?.mapM fun d => match d with
|
||||
|
|
|
|||
|
|
@ -802,9 +802,9 @@ The coinductive predicate is defined as the greatest fixed point of a monotone f
|
|||
By default, monotonicity is verified automatically. However, users can provide custom proofs
|
||||
of monotonicity if needed.
|
||||
-/
|
||||
def greatestFixpoint := leading_parser
|
||||
def coinductiveFixpoint := leading_parser
|
||||
withPosition (
|
||||
"greatest_fixpoint" >>
|
||||
"coinductive_fixpoint" >>
|
||||
optional (checkColGt "indentation" >> nonReservedSymbol "monotonicity " >>
|
||||
checkColGt "indented monotonicity proof" >> termParser))
|
||||
|
||||
|
|
@ -819,9 +819,9 @@ The inductive predicate is defined as the least fixed point of a monotone functi
|
|||
By default, monotonicity is verified automatically. However, users can provide custom proofs
|
||||
of monotonicity if needed.
|
||||
-/
|
||||
def leastFixpoint := leading_parser
|
||||
def inductiveFixpoint := leading_parser
|
||||
withPosition (
|
||||
"least_fixpoint" >>
|
||||
"inductive_fixpoint" >>
|
||||
optional (checkColGt "indentation" >> nonReservedSymbol "monotonicity " >>
|
||||
checkColGt "indented monotonicity proof" >> termParser))
|
||||
|
||||
|
|
@ -841,7 +841,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 <|> partialFixpoint <|> greatestFixpoint <|> leastFixpoint)) >> optional decreasingBy
|
||||
optional (ppDedent ppLine >> (terminationBy? <|> terminationBy <|> partialFixpoint <|> coinductiveFixpoint <|> inductiveFixpoint)) >> optional decreasingBy
|
||||
|
||||
end Termination
|
||||
namespace Term
|
||||
|
|
|
|||
|
|
@ -1,27 +1,25 @@
|
|||
-- Coinductive predicate definition
|
||||
def infseq {α} (R : α → α → Prop) : α → Prop :=
|
||||
λ x : α => ∃ y, R x y ∧ infseq R y
|
||||
greatest_fixpoint
|
||||
coinductive_fixpoint
|
||||
|
||||
-- Application of the rewrite rule
|
||||
def infseq_fixpoint {α} (R : α → α → Prop) (x : α) :
|
||||
infseq R x = ∃ y, R x y ∧ infseq R y := by
|
||||
rw [infseq]
|
||||
|
||||
#check infseq.coinduct
|
||||
|
||||
-- The associated coinduction principle
|
||||
theorem infseq.coind {α} (h : α → Prop) (R : α → α → Prop)
|
||||
(prem : ∀ (x : α), h x → ∃ y, R x y ∧ h y) : ∀ x, h x → infseq R x := by
|
||||
apply infseq.fixpoint_induct
|
||||
exact prem
|
||||
/--
|
||||
info: infseq.fixpoint_induct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α → Prop)
|
||||
(y : ∀ (x_1 : α), x x_1 → ∃ y, R x_1 y ∧ x y) (x✝ : α) : x x✝ → infseq R x✝
|
||||
info: infseq.coinduct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α → Prop) (y : ∀ (x_1 : α), x x_1 → ∃ y, R x_1 y ∧ x y)
|
||||
(x✝ : α) : x x✝ → infseq R x✝
|
||||
-/
|
||||
#guard_msgs in #check infseq.fixpoint_induct
|
||||
#guard_msgs in #check infseq.coinduct
|
||||
|
||||
-- Simple proof by coinduction
|
||||
theorem cycle_infseq {R : α → α → Prop} (x : α) : R x x → infseq R x := by
|
||||
apply @infseq.fixpoint_induct α R (λ m => R m m)
|
||||
apply @infseq.coinduct α R (λ m => R m m)
|
||||
intro x _
|
||||
apply Exists.intro x
|
||||
trivial
|
||||
|
|
@ -34,13 +32,13 @@ inductive star (R : α → α → Prop) : α → α → Prop where
|
|||
-- Inductive predicate, as a least fixpoint
|
||||
def star_ind (tr : α → α → Prop) (q₁ q₂ : α) : Prop :=
|
||||
∃ (z : α), q₁ = q₂ ∨ (tr q₁ z ∧ star_ind tr z q₂)
|
||||
least_fixpoint
|
||||
inductive_fixpoint
|
||||
|
||||
/--
|
||||
info: star_ind.fixpoint_induct.{u_1} {α : Sort u_1} (tr : α → α → Prop) (q₂ : α) (x : α → Prop)
|
||||
info: star_ind.induct.{u_1} {α : Sort u_1} (tr : α → α → Prop) (q₂ : α) (x : α → Prop)
|
||||
(y : ∀ (x_1 : α), (∃ z, x_1 = q₂ ∨ tr x_1 z ∧ x z) → x x_1) (x✝ : α) : (fun q₁ => star_ind tr q₁ q₂) x✝ → x x✝
|
||||
-/
|
||||
#guard_msgs in #check star_ind.fixpoint_induct
|
||||
#guard_msgs in #check star_ind.induct
|
||||
|
||||
-- From one you can prove the other
|
||||
theorem star_implies_star' (R : α → α → Prop) : ∀ a b : α, star R a b → star_ind R a b := by
|
||||
|
|
@ -109,7 +107,7 @@ def all_seq_inf (R : α → α → Prop) (x : α) : Prop :=
|
|||
∀ y : α, star R x y → ∃ z, R y z
|
||||
|
||||
def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x → infseq R x := by
|
||||
apply infseq.fixpoint_induct
|
||||
apply infseq.coinduct
|
||||
intro x H
|
||||
unfold all_seq_inf at H
|
||||
have H' := H x (by simp [star.star_refl])
|
||||
|
|
@ -132,7 +130,7 @@ theorem infseq_coinduction_principle_2:
|
|||
∀ (a : α), x a → infseq R a := by
|
||||
intro X
|
||||
intro h₁ a rel
|
||||
apply @infseq.fixpoint_induct _ _ (fun a => ∃ b, star R a b ∧ X b)
|
||||
apply @infseq.coinduct _ _ (fun a => ∃ b, star R a b ∧ X b)
|
||||
case x =>
|
||||
apply Exists.elim (h₁ a rel)
|
||||
intro a' ⟨h₁, h₂⟩
|
||||
|
|
@ -164,10 +162,10 @@ def language_equivalent (automaton : DFA Q A) (q₁ q₂ : Q) : Prop :=
|
|||
let ⟨o₁, t₁⟩ := automaton q₁
|
||||
let ⟨o₂, t₂⟩ := automaton q₂
|
||||
o₁ = o₂ ∧ (∀ a : A, language_equivalent automaton (t₁ a) (t₂ a))
|
||||
greatest_fixpoint
|
||||
coinductive_fixpoint
|
||||
|
||||
/--
|
||||
info: language_equivalent.fixpoint_induct {Q A : Type} (automaton : DFA Q A) (x : Q → Q → Prop)
|
||||
info: language_equivalent.coinduct {Q A : Type} (automaton : DFA Q A) (x : Q → Q → Prop)
|
||||
(y :
|
||||
∀ (x_1 x_2 : Q),
|
||||
x x_1 x_2 →
|
||||
|
|
@ -175,17 +173,17 @@ info: language_equivalent.fixpoint_induct {Q A : Type} (automaton : DFA Q A) (x
|
|||
(x✝ x✝¹ : Q) : x x✝ x✝¹ → language_equivalent automaton x✝ x✝¹
|
||||
-/
|
||||
#guard_msgs in
|
||||
#check language_equivalent.fixpoint_induct
|
||||
#check language_equivalent.coinduct
|
||||
|
||||
namespace mixed1
|
||||
mutual
|
||||
def tick : Prop :=
|
||||
¬tock
|
||||
greatest_fixpoint
|
||||
coinductive_fixpoint
|
||||
|
||||
def tock : Prop :=
|
||||
¬tick
|
||||
least_fixpoint
|
||||
inductive_fixpoint
|
||||
end
|
||||
end mixed1
|
||||
|
||||
|
|
@ -193,11 +191,11 @@ namespace mixed2
|
|||
mutual
|
||||
def tick : Prop :=
|
||||
¬tock
|
||||
greatest_fixpoint
|
||||
inductive_fixpoint
|
||||
|
||||
def tock : Prop :=
|
||||
¬tick
|
||||
least_fixpoint
|
||||
coinductive_fixpoint
|
||||
end
|
||||
end mixed2
|
||||
|
||||
|
|
@ -205,11 +203,11 @@ namespace mixed3
|
|||
mutual
|
||||
def tick : Prop :=
|
||||
tock → tick
|
||||
greatest_fixpoint
|
||||
coinductive_fixpoint
|
||||
|
||||
def tock : Prop :=
|
||||
tick → tock
|
||||
least_fixpoint
|
||||
inductive_fixpoint
|
||||
end
|
||||
end mixed3
|
||||
|
||||
|
|
@ -217,10 +215,10 @@ namespace mixed4
|
|||
mutual
|
||||
def tick : Prop :=
|
||||
tock → tick
|
||||
least_fixpoint
|
||||
inductive_fixpoint
|
||||
|
||||
def tock : Prop :=
|
||||
tick → tock
|
||||
greatest_fixpoint
|
||||
coinductive_fixpoint
|
||||
end
|
||||
end mixed4
|
||||
|
|
|
|||
|
|
@ -1,36 +1,36 @@
|
|||
/-!
|
||||
This file contains tests for typical mistakes one might do when using `least_fixpoint`/`greatest_fixpoint`/`partial_fixpoint` machinery, that is:
|
||||
- Try to use `greatest_fixpoint`/`least_fixpoint` to define functions instead of predicates
|
||||
- Apply `greatest_fixpoint`/`least_fixpoint` to non-recursive functions
|
||||
- Mix `partial_fixpoint` with `greatest_fixpoint`/`least_fixpoint` in the same clique
|
||||
This file contains tests for typical mistakes one might do when using `inductive_fixpoint`/`coinductive_fixpoint`/`partial_fixpoint` machinery, that is:
|
||||
- Try to use `coinductive_fixpoint`/`inductive_fixpoint` to define functions instead of predicates
|
||||
- Apply `coinductive_fixpoint`/`inductive_fixpoint` to non-recursive functions
|
||||
- Mix `partial_fixpoint` with `coinductive_fixpoint`/`inductive_fixpoint` in the same clique
|
||||
-/
|
||||
|
||||
/--
|
||||
error: `greatest_fixpoint` can be only used to define predicates
|
||||
error: `coinductive_fixpoint` can be only used to define predicates
|
||||
-/
|
||||
#guard_msgs in
|
||||
def f (x : Nat) : Nat :=
|
||||
f (x + 1)
|
||||
greatest_fixpoint
|
||||
coinductive_fixpoint
|
||||
|
||||
/--
|
||||
error: `least_fixpoint` can be only used to define predicates
|
||||
error: `inductive_fixpoint` can be only used to define predicates
|
||||
-/
|
||||
#guard_msgs in
|
||||
def g (x : Nat) : Nat :=
|
||||
g (x + 1)
|
||||
least_fixpoint
|
||||
inductive_fixpoint
|
||||
|
||||
/--
|
||||
warning: unused `greatest_fixpoint`, function is not recursive
|
||||
warning: unused `coinductive_fixpoint`, function is not recursive
|
||||
-/
|
||||
#guard_msgs in
|
||||
def h (x : Nat) : Prop := x > 42
|
||||
greatest_fixpoint
|
||||
coinductive_fixpoint
|
||||
|
||||
/--
|
||||
warning: unused `least_fixpoint`, function is not recursive
|
||||
warning: unused `inductive_fixpoint`, function is not recursive
|
||||
-/
|
||||
#guard_msgs in
|
||||
def h' (x : Nat) : Prop := x > 42
|
||||
least_fixpoint
|
||||
inductive_fixpoint
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ def asimp_const : Aexp -> Aexp
|
|||
@[simp]
|
||||
def optimal' (a : Aexp) : Prop :=
|
||||
optimal' a ∧ True
|
||||
least_fixpoint
|
||||
inductive_fixpoint
|
||||
|
||||
/-- info: Try this: simp_all only [asimp_const, reduceCtorEq] -/
|
||||
#guard_msgs in
|
||||
|
|
|
|||
|
|
@ -131,20 +131,20 @@ mutual
|
|||
partial_fixpoint
|
||||
|
||||
def g (x : Nat) : Prop := f (x + 1)
|
||||
least_fixpoint
|
||||
inductive_fixpoint
|
||||
end
|
||||
end Test6
|
||||
|
||||
|
||||
namespace Test7
|
||||
/--
|
||||
error: Incompatible termination hint; this function is mutually recursive with Test7.f, which is marked as `greatest_fixpoint` so this one also needs to be marked `least_fixpoint` or `greatest_fixpoint`.
|
||||
error: Incompatible termination hint; this function is mutually recursive with Test7.f, which is marked as `coinductive_fixpoint` so this one also needs to be marked `inductive_fixpoint` or `coinductive_fixpoint`.
|
||||
-/
|
||||
#guard_msgs in
|
||||
mutual
|
||||
def f (x : Nat) : Prop :=
|
||||
g (x + 1)
|
||||
greatest_fixpoint
|
||||
coinductive_fixpoint
|
||||
|
||||
def g (x : Nat) : Prop :=
|
||||
f (x + 1)
|
||||
|
|
@ -170,7 +170,7 @@ end Test8
|
|||
|
||||
namespace Test9
|
||||
/--
|
||||
error: Incompatible termination hint; this function is mutually recursive with Test9.f, which is not also marked as `least_fixpoint` or `greatest_fixpoint`, so this one cannot be either.
|
||||
error: Incompatible termination hint; this function is mutually recursive with Test9.f, which is not also marked as `inductive_fixpoint` or `coinductive_fixpoint`, so this one cannot be either.
|
||||
-/
|
||||
#guard_msgs in
|
||||
mutual
|
||||
|
|
@ -180,19 +180,19 @@ mutual
|
|||
|
||||
def g (x : Nat) : Prop :=
|
||||
f (x + 1)
|
||||
least_fixpoint
|
||||
inductive_fixpoint
|
||||
end
|
||||
end Test9
|
||||
|
||||
namespace Test10
|
||||
/--
|
||||
error: Incompatible termination hint; this function is mutually recursive with Test10.f, which is marked as `greatest_fixpoint` so this one also needs to be marked `least_fixpoint` or `greatest_fixpoint`.
|
||||
error: Incompatible termination hint; this function is mutually recursive with Test10.f, which is marked as `coinductive_fixpoint` so this one also needs to be marked `inductive_fixpoint` or `coinductive_fixpoint`.
|
||||
-/
|
||||
#guard_msgs in
|
||||
mutual
|
||||
def f (x : Nat) : Prop :=
|
||||
g (x + 1)
|
||||
greatest_fixpoint
|
||||
coinductive_fixpoint
|
||||
|
||||
def g (x : Nat) : Prop :=
|
||||
f (x + 1)
|
||||
|
|
|
|||
|
|
@ -5,11 +5,11 @@ Tests that `partial_fixpoint` is not picking up the partial order structure on P
|
|||
-- This works as `∨` is monotone in its arguments with respect to the (`ImplicationOrder`/`ReverseImplicationOrder` on `Prop`.
|
||||
def f (x : Nat) : Prop :=
|
||||
f (x + 1) ∨ f ( x + 2)
|
||||
greatest_fixpoint
|
||||
coinductive_fixpoint
|
||||
|
||||
def f' (x : Nat) : Prop :=
|
||||
f' (x + 1) ∨ f' ( x + 2)
|
||||
least_fixpoint
|
||||
inductive_fixpoint
|
||||
|
||||
/--
|
||||
error: Could not prove 'f''' to be monotone in its recursive calls:
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue