96fcc94acb
This PR adds support for inductive and coinductive predicates defined using lattice theoretic structures on `Prop`. These are syntactically defined using `greatest_fixpoint` or `least_fixpoint` termination clauses for recursive `Prop`-valued functions. The functionality relies on `partial_fixpoint` machinery and requires function definitions to be monotone. For non-mutually recursive predicates, an appropriate (co)induction proof principle (given by Park induction) is generated. Summary of changes: - `Interal.Order.Basic` now contains `CompleteLattice` class, as well as version of Knaster-Tarski fixpoint theorem (with an associated Park induction principle) for the internal use for defining (co)inductive predicates. `Prop` is shown to have two complete lattice structures (one given by implication order for defining inductive predicates, and one given by reverse implication for defining coinductive predicates). Additionally, proofs that lattices are closed under products and function spaces are included. - Partial fixpoint's `EqnInfo` now additionally carries an information whether something is defined as a lattice-theoretic fixpoint or via CCPOs. - When constructing a (co)inductive predicate,`PartialFixpoint/Main` builds an appropriate lattice structure on the type of the predicate using product lattice, function space lattice and an appropriate lattice instance on `Prop`. - `PartialFixpoint/Eqns` is modified to be able to perform rewrite under lattice-theoretic fixpoint construction - `PartialFixpoint/Induction`contains a case split for handling of the (co)inductive predicates. In the case of lattice-theoretic fixpoints, it appropriately desugars the Park induction principle.
216 lines
5.2 KiB
Text
216 lines
5.2 KiB
Text
|
||
namespace Test
|
||
/--
|
||
error: incomplete set of termination hints:
|
||
This function is mutually recursive with Test.f, Test.h and Test.i, which do not have a termination hint.
|
||
The present clause is ignored.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f : Nat → α → α → α
|
||
| 0, a, b => a
|
||
| n+1, a, b => g n a b |>.1
|
||
|
||
def g : Nat → α → α → (α × α)
|
||
| 0, a, b => (a, b)
|
||
| n+1, a, b => (h n a b, a)
|
||
termination_by n _ _ => n -- Error
|
||
|
||
def h : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => i n a b
|
||
|
||
def i : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => f n a b
|
||
end
|
||
end Test
|
||
|
||
namespace Test2
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test2.f, which is marked as `termination_by structural` so this one also needs to be marked `structural`.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f : Nat → α → α → α
|
||
| 0, a, b => a
|
||
| n+1, a, b => g n a b |>.1
|
||
termination_by structural n _ _ => n
|
||
|
||
def g : Nat → α → α → (α × α)
|
||
| 0, a, b => (a, b)
|
||
| n+1, a, b => (h n a b, a)
|
||
termination_by n _ _ => n -- Error
|
||
|
||
def h : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => f n a b
|
||
termination_by n _ _ => n
|
||
end
|
||
end Test2
|
||
|
||
namespace Test3
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test3.f, which is not marked as `structural` so this one cannot be `structural` either.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f : Nat → α → α → α
|
||
| 0, a, b => a
|
||
| n+1, a, b => g n a b |>.1
|
||
termination_by n _ _ => n
|
||
|
||
def g : Nat → α → α → (α × α)
|
||
| 0, a, b => (a, b)
|
||
| n+1, a, b => (h n a b, a)
|
||
termination_by structural n _ _ => n -- Error
|
||
|
||
def h : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => f n a b
|
||
termination_by structural n _ _ => n
|
||
end
|
||
end Test3
|
||
|
||
namespace Test4
|
||
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test4.f, which is not marked as `structural` so this one cannot be `structural` either.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f : Nat → α → α → α
|
||
| 0, a, b => a
|
||
| n+1, a, b => g n a b |>.1
|
||
termination_by n _ _ => n
|
||
|
||
def g : Nat → α → α → (α × α)
|
||
| 0, a, b => (a, b)
|
||
| n+1, a, b => (h n a b, a)
|
||
termination_by n _ _ => n
|
||
|
||
def h : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => f n a b
|
||
termination_by structural n _ _ => n -- Error
|
||
end
|
||
end Test4
|
||
|
||
namespace Test5
|
||
/--
|
||
error: Incompatible termination hint; this function is marked as structurally recursive, so no explicit termination proof is needed.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f : Nat → α → α → α
|
||
| 0, a, b => a
|
||
| n+1, a, b => g n a b |>.1
|
||
termination_by structural n _ _ => n
|
||
|
||
def g : Nat → α → α → (α × α)
|
||
| 0, a, b => (a, b)
|
||
| n+1, a, b => (h n a b, a)
|
||
termination_by structural n _ _ => n
|
||
decreasing_by sorry -- Error
|
||
|
||
def h : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => f n a b
|
||
termination_by structural n _ _ => n
|
||
end
|
||
end Test5
|
||
|
||
namespace Test6
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test6.f, which is marked as `partial_fixpoint` so this one also needs to be marked `partial_fixpoint`.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x + 1)
|
||
partial_fixpoint
|
||
|
||
def g (x : Nat) : Prop := f (x + 1)
|
||
least_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`.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x + 1)
|
||
greatest_fixpoint
|
||
|
||
def g (x : Nat) : Prop :=
|
||
f (x + 1)
|
||
partial_fixpoint
|
||
end
|
||
end Test7
|
||
|
||
namespace Test8
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test8.f, which is not also marked as `partial_fixpoint`, so this one cannot be either.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x + 1)
|
||
termination_by?
|
||
|
||
def g (x : Nat) : Prop :=
|
||
f (x + 1)
|
||
partial_fixpoint
|
||
end
|
||
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.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x + 1)
|
||
termination_by?
|
||
|
||
def g (x : Nat) : Prop :=
|
||
f (x + 1)
|
||
least_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`.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x + 1)
|
||
greatest_fixpoint
|
||
|
||
def g (x : Nat) : Prop :=
|
||
f (x + 1)
|
||
termination_by?
|
||
end
|
||
end Test10
|
||
|
||
namespace Test11
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test11.f, which is marked as `partial_fixpoint` so this one also needs to be marked `partial_fixpoint`.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x +1)
|
||
partial_fixpoint
|
||
|
||
def g (x : Nat) : Prop :=
|
||
f (x + 1)
|
||
end
|
||
end Test11
|