Coinductive Uniform Proofs
Ekaterina Komendantskaya, Yue Li
TL;DR
This paper introduces a unified proof-theoretic framework for coinductive reasoning in Horn clause logic, addressing proofs of circular properties and infinite data construction with formal soundness guarantees.
Contribution
It presents a novel coinductive extension of the uniform proof framework, systematically analyzing two types of coinductive proofs and establishing their soundness.
Findings
Unified framework for coinductive proofs in Horn clause logic
Proof of soundness relative to coinductive models
Formal analysis of circular and infinite data proofs
Abstract
Coinduction occurs in two guises in Horn clause logic: in proofs of circular properties and relations, and in proofs involving construction of infinite data. Both instances of coinductive reasoning appeared in the literature before, but a systematic analysis of these two kinds of proofs and of their relation was lacking. We propose a general proof-theoretic framework for handling both kinds of coinduction arising in Horn clause logic. To this aim, we propose a coinductive extension of Miller et al framework of uniform proofs and prove its soundness relative to coinductive models of Horn clause logic.
| Program Clauses | Goals | |
|---|---|---|
| co-fohc | ||
| co-hohc | ||
| co-fohh | ||
| co-hohh |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification
Coinductive Uniform Proofs
E. Komendantskaya and Y. Li Heriot-Watt University, Edinburgh, Scotland, UK1111
Abstract
Coinduction occurs in two guises in Horn clause logic: in proofs of circular properties and relations, and in proofs involving construction of infinite data. Both instances of coinductive reasoning appeared in the literature before, but a systematic analysis of these two kinds of proofs and of their relation was lacking. We propose a general proof-theoretic framework for handling both kinds of coinduction arising in Horn clause logic. To this aim, we propose a coinductive extension of Miller et al’s framework of uniform proofs and prove its soundness relative to coinductive models of Horn clause logic.
This paper is a preliminary version of [6] and contains a simpler version of the soundness proof that appeared later in [6].
Keywords: Horn Clause Logic, Coinduction, Uniform Proofs.
1 Introduction
Horn clause logic is a fragment of predicate logic, in which all formulae are written in clausal form. For example, the two clauses below inductively define a list membership property:
(1)
(2)
We use notation for list and stream constructors throughout this paper. Generally, a Horn clause has a shape , where each and are atomic formulae. The clause (1) above should be read as having an empty antecedent. This syntax implicitly restricts the syntax of a goal clause (or goal), i.e. a clause with empty consequent. Firstly, all goals are existentially quantified. Secondly, they may only contain conjunctions. Thus we can have as a goal e.g. , and prove it with , but not an implicative or a universally quantified formula, e.g. not or .
Initially introduced by Horn in the 30s, Horn clause logic gained popularity for yielding efficient proofs by resolution [16], which made it the logic of choice for first implementations of Prolog in 70s and 80s [25], as well as several resolution-based provers in the 90s. The next big step was made in the 90s by Miller, Nadathur et. al [27, 28] who studied proof-theoretic properties of Horn clause logic, introducing the notion of a uniform proof. Within that framework, three extensions to Horn clause logic were suggested. Taking first-order Horn clauses (fohc) as a starting point, they extended it with lambda abstraction, obtaining higher-order Horn clauses (hohc). Allowing not only conjunctions, but also implications, disjunctions and quantified formulae in the antecedent of gave hereditary Harrop logic, which, too can have first-order or higher order syntax resulting in first-order hereditary Harrop clause logic (fohh) and higher-order hereditary Harrop clause logic (hohh). For example, we can express and prove and in fohh, taking clauses (0) and (1) as axioms. Figure 1 shows the “uniform proof diamond” (the arrows show syntactic extensions).
To name a few most recent appearances of these logics in the literature, higher-order Horn clauses are gaining popularity in verification of functional programs and in refinement types [21, 13]; and first-order hereditary Harrop clause logic has been used in extensions of Haskell type classes [11]. There are of course Prolog/Teyjus [29] and Abella [2] influenced by uniform proofs, as well as an extensive SMT-solving literature on applications of Horn clauses in verification [8]. The uniform proof diamond thus gives a useful proof-theoretic classification for a set of computationally tractable and interesting fragments of first-order and higher-order logics.
Coinductive properties of first-order Horn clause logic are not equally well understood proof-theoretically. Firstly, we can define coinductive (or infinite) data structures, such as streams or infinite trees, in this logic. For example an infinite stream of bits can be defined as follows:
(3)
(4)
(5)
Given a suitable coinductive proof principle, we can prove , substituting with a suitable recursive term. Some such derivations can be performed in CoLP [20, 33].
Secondly, first-order Horn clauses can be used to state and prove circular properties and relations. These do not have to involve infinite data structures. We may state the following circular property of the (finite) list membership:
(6)
(7)
Again, given a suitable coinductive proof principle, the goal could be proven coinductively by using just the clauses (6) and (7), without inductively analysing the list structure as clauses (1) and (2) suggest. Interesting cases of such circular proofs were reported in implementation of Haskell type classes [23, 18].
Thridly, the existing literature tends to regard coinduction in Horn clause logic mainly operationally, as a process of loop detection. The question is thus two-fold: Can we formulate a coinductive proof principle for Horn clause logic, complementing the work of Miller et al. on systematisation of proof-theoretic properties of Horn clause logic? What would be the “suitable coinductive proof principle” to cover both cases of coinduction? This question has not been raised or answered in the literature in this generality. And this is where this paper fills the gap.
Suppose we simply take fohc and extend it with a standard coinductive proof rule à la Coquand and Gimenez [14, 19]. Would this resulting coinductive calculus, lets call it co-fohc, be suitable to prove coinductive properties of fohc formulae? – It turns out not: we would be able to prove given the clauses (6)-(7), but not for clauses (3)-(5). To instantiate the existential quantifier, we would need to define the stream of zeros using a fixed-point operator, and for this we need at least the language of hohc.
Next, suppose we take co-hohc, i.e. a coinductive version of hohc. Would it give us a suitable coinductive calculus? – The answer is again negative. It would cover our earlier examples, but not the following example, defining an infinite stream of successive numbers:
(8)
Given as a goal, would be an intended answer for . For this clause, we cannot prove directly, but we have to prove a more general lemma first, i.e. , where is a fixed point definition of a stream of successive numbers starting with . But, by the earlier discussion, this universal goal does not belong to hohc! It is a goal of hereditary Harrop clause logic, that is, we need at least the syntax and rules of hohh, with additional coinductive rule (i.e. we need a calculus co-hohh).
To complete the picture with a fourth calculus, we consider an example of a coinductive property whose proof falls within the remits of co-fohh. Suppose we are given a definition of a comembership property, i.e. a property that an element occurs in a stream infinitely many times111It can be defined for example as follows:
. Suppose now a function is defined to take streams of bits as input and return streams of bits as an output. Therefore, its application would not affect the property of a bit comembership:
(9)
Again, using a suitable coinductive proof principle, we could prove the lemma . This lemma would belong to co-fohh, as its syntax is expressed in first-order hereditary Harrop clause logic. A fohc version of the lemma, e.g. is not provable by coinduction (whatever is), but would follow from if we prove that first. Many more examples of this kind of coinductive reasoning are given in [18].
In Section 3, we introduce these four calculi formally and thereby establish a uniform proof framework for systematic study of coinduction that arises in Horn clause logic (cf. Figure 1). We show that these four calculi characterize four different classes of coinductive properties arising from Horn clause definitions: co-fohc and co-fohh are required when proofs do not involve construction of infinite data, whereas co-hohc and co-hohh are needed for proofs involving infinite data construction. These cases further sub-divide: co-fohc and co-hohc are suitable for regular proofs of atomic coinductive properties (like ). Co-fohh and co-hohh will be needed to construct proofs that exhibit irregularity and require more general coinductive hypotheses (like or ). As if by magic, Miller et al’s “uniform proof diamond” happens to give a perfect basis for systematic description of coinductive proofs and properties arising in Horn clause logic.
Let us call a set of first-order Horn clauses a logic program. In Section 4 we show that, given a logic program , the proofs obtained for in co-fohc, co-fohh, co-hohc, co-hohh are coinductively sound, i.e. sound relative to the greatest Herbrand model of . We also show that it is coinductively sound to use coinductively proven lemmas in other proofs, as was illustrated in the final example of this section.
First-order Horn clause logic is Turing complete and therefore any sound calculus for it will fail to decide some recursive cases. In Section 5, we discuss examples of logic programs that define coinductive properties beyond the power of our “coinductive diamond”.
The uniform proofs in general, and their coinductive version in particular, are not designed to compete in expressivity or power with richer logics, such as e.g. the calculus of (coinductive) constructions [14, 19]. The motivation behind uniform proofs is to give an elegant and thorough proof theoretic analysis of automated reasoning with Horn clauses. Taking this perspective, the presented work advances the state of knowledge in several ways:
- •
The “coinductive diamond” covers and extends the currently available coinductive algorithms for Horn clause logic. For example, Co-LP [20, 33] is equivalent to co-fohc plus co-hohc, productive corecursion of [22] is equivalent to co-hohc, but neither extends to co-fohh or co-hohh. Methods introduced in [23, 18] are subsumed by co-fohc and co-fohh, but cannot work with infinite data, thus fall short of co-hohc and co-hohh.
- •
This paper shows a novel application of the coinductive proof principle known in functional programming [14, 19] to uniform proofs. We take this principle to a terrain where it has considerably less support than in Coq to ensure its soundness: e.g. we cannot rely on (co)-inductive data types or proof terms (on which guardedness checks are usually imposed, cf. [19]).
- •
Our soundness result for co-hohh is conceptually novel, and, when restricted to the other three calculi, addresses limitations of similar results published in the literature: we replace the operational soundness of co-fohh given in [18] with soundness relative to coinductive models; we replace non-constructive proof of soundness of co-fohh given in [17] with a constructive proof; we extend soundness results of [20, 33] to co-hohh and co-fohh.
- •
Overall, the presented results advance our understanding of coinductive properties expressible in first-order logic. We thus hope that this work will give a solid formal support for new implementations of coinduction in automated proving based on first-order logic.
The paper proceeds as follows. Section 2 gives the necessary background definitions. Section 3 introduces the four original coinductive calculi based on uniform proofs. Section 4 proves that our coinductive calculi are sound relative to the coinductive model of Horn clause logic. Finally, Section 5 concludes and discusses related and future work.
2 Preliminaries, Fixed-point Terms
We first recall some essential definitions concerning the syntax of uniform proofs [28]. In order to be able to work with infinite data structures like streams, we extend that original syntax with fixed-point combinators in a standard way, following [31, 30].
Let be a countable set of type variables, and be the set of all simple types (in short, types) in the abstract syntax:
[TABLE]
We use and variants thereof to denote an arbitrary type. A type is called a non-functional type. A type of the form is called a functional type. Given the right associativity of the functional type constructor (), we can remove all redundant parentheses and depict a type in the form , where the non-functional type is the target type of , and are argument types of .
Definition 1 (Terms)
Let be a countable set of (term) variables, and – a countable set of constants . The set of all lambda terms (in short: terms) is defined by
[TABLE]
A term of the form is called an application, and a term of the form – abstraction. A term of the form is called a fixed-point term. We use letters and variants thereof to denote members of .
Given a term , the set of free variables and the set of sub-terms of are defined as standard, cf. Appendix 0.A. Term is closed, if . Otherwise, is open. We define , called a signature, be a partial function mapping from to the set of simple types, and , called a context, be a partial function mapping from to . A term is well typed if it satisfies type judgment for some and , using the standard typing rules given in Appendix 0.A. We will only work with well typed terms. All free variables in a term must have their types assigned by . Therefore, we use to imply that is a closed term.
We use the symbols for conjunction, for disjunction, for implication, and for the true proposition. Given some type , we use for universal quantification, and for existential quantification, over terms of type . These symbols are special constants, called logical constants and their types are as follows: , and , and . Quantification over a term is a short hand for applying the quantifier to an abstraction over . We assume that a signature always contains at least all logical constants.
Definition 2 (First-order types and terms)
The order of a type , denoted , is
[TABLE]
A term is called first order if the following conditions are satisfied.
, and 2. 2.
, and 3. 3.
, and 4. 4.
, and 5. 5.
.
A predicate is a variable or a non-logical constant of type such that either or the target type of is . We say that a predicate is first order if it is a non-logical constant, whose type expression is of order at most 1, and the type does not occur as its argument type. Otherwise a predicate is of higher order. A signature is first-order if for all non-logical constants in , (i) the type expression of is at most of order , and (ii) the type is involved in the type expression of only if is a first order predicate.
Substitution of all free occurrences of a variable in a term by a term , denoted , and the notion of -equivalence are defined as standard, see Appendix 0.A. We use to denote the relation of syntactical identity modulo -equivalence. We call a substitution when we have (the latter denotes ).
One step -reduction, denoted , is defined as . Moreover, it is defined that if , then , , and . If there is no term such that , then is -normal. We define -equivalence, denoted , as a transitive and reflexive closure of . Because the primitive is treated as a constant symbol when doing -reduction, it does not affect strong normalisation of -reduction. In this paper we assume that all terms are in -normal form unless otherwise stated.
One step -reduction, denoted , is defined as
[TABLE]
Moreover, we require that, if , then for arbitrary and , , , and . -equivalence, denoted , is defined as: if there is and there are terms to such that , , and for all such that , or or .
Example 1 (Stream of zeros)
Given non-logical constants and (scons can be identified with ), we represent the stream of zeros in the form of a fixed-point term . The following relations justify that models the stream of zeros:
[TABLE]
Example 2 (Constant stream)
The stream of zeros can be generalised to a stream of any particular number, as follows: . It takes a term as parameter and returns a stream of ’s:
[TABLE]
Example 3 (Stream of successive numbers)
We add a successor function to the signature of Example 1. We represent, in the form of a fixed-point term, the family of streams of successive natural numbers: .
Again, the following relations hold for all (for instance, can be [math], , …):
[TABLE]
In line with the standard literature on this subject [7, 9], we now need to introduce guardedness conditions on fixed-point definitions, otherwise some of them may not define any infinite objects. A detailed discussion of term productivity or various guardedness conditions that insure this property are beyond the scope of this paper. We simply adapt standard guardedness conditions [19], although other methods available in the literature (e.g. [9]) may work as well.
Definition 3 (Guarded fixed point terms)
A guarded fixed point term has the form
[TABLE]
is a variable of type , where and . 2. 2.
is a constant of type where and . 3. 3.
are first order terms of type . 4. 4.
.
Clearly, the generic guarded fixed point term in Definition 3 is closed and has type . All fixed point terms shown in examples above are guarded.
Definition 4 (Guarded full terms)
A guarded full term is either a first order term, or a higher order term in the form where is a guarded fixed point term, and are first order terms, provided and .
An atomic formula (in short, atom) is a lambda term of type , in the form , where , is a predicate, and are lambda terms; if is a variable, then we say the atom is flexible; if is a non-logical constant, then the atom is rigid; if is a first order predicate, and are first order terms, then the atom is of first order. If is a first order predicate, and are guarded full terms, then the atom is guarded, and all atoms such that are guarded.
3 Coinductive Uniform Proofs
We start with introducing the formal languages of four uniform proof calculi by Miller and Nadathur [28]. As in the original setting, the distinction between Horn clauses and hereditary Harrop clauses lies in enriched syntax for goals: the latter admits universally quantified and implicative goals. The distinction between first-order and higher-order logics is made by allowing or disallowing higher-order terms, as defined in the previous section.
Assume a signature . Let be the set of all terms over that do not contain the logical constants and , and be the set of all terms over that do not contain the logical constant 222Miller and Nadathur called the sets and “Herbrand universes” [28, §5.2]. Here we reserve the name “Herbrand” for later modal-theoretic study of the languages.. Further, let and denote the sets of atoms and rigid atoms, respectively, on . In the setting of co-fohc and co-fohh, let be first order (we will denote this fact by in Table 1). In the setting of co-hohc, let and be from ; in the setting of co-hohh, let and be from . Using the sets , , and , Table 1 defines, for each of the four calculi, the set of program clauses and the set of goals.
Given a signature , a logic program is a finite set of -formulae over . In the rest of this paper, we will assume that the signature is determined by a given logic program and is always first-order. We can still build higher-order terms (including guarded fixed point terms) over a first-order signature as we place no restriction on types of variables. A sequent is an expression of the form , encoding the proposition that the goal formula is provable from the logic program based on the signature . We recall the uniform proof rules in Figure 2.
We can now proceed to introduce the main rule of this paper, i.e. the coinductive proof rule. We take inspiration from [14, 19], but make a few adaptations to the uniform proof syntax. We distinguish coinductive entailment from entailment by the original uniform rules. An expression of the form , also called a sequent, means: the goal formula is coinductively provable from the logic program on the signature . The co-fix rule for is given in Figure 3.
This simple step already gives a useful insight into suitable coinductive proof principles for the four logics we introduced. Namely, because the same formula must occur both as a coinductive hypothesis on the left of and the coinductive goal on the right of in the rule co-fix, this restricts the syntax of the coinductive hypothesis to core formulae, i.e. formulae satisfying the definition of both program clauses and goals:
[TABLE]
To the best of our knowledge such precise relationship between the power of the calculus in question and the expressivity of the coinductive hypotheses it admits has not been described in the literature before. Coq, for example, imposes some restrictions on the shape of coinductive hypotheses (e.g. existential formulae cannot be taken as coinductive hypotheses in Coq), but those restrictions are motivated differently.
The next problem is how to guard the coinductive rule from unsound applications. To this aim, we introduce the guarding notation within the co-fix rule, signifying the guarded status of this goal. In order to be able to construct proofs with guarded formulae, we introduce a set of rules in Figure 4. A similar approach to guarding coinductive proofs has recently been suggested independently (and in a different calculus) by Basold [4].
The coinductive uniform proof rules are given in Figures 2, 3, 4. A proof for a sequent is a finite tree constructed using coinductive uniform proof rules and such that the root is labelled with or , and leaves are labelled with initial sequents (i.e. sequents that can occur as a lower sequent in the rules initial or ). We say that a proof is constructed in co-fohc, co-fohh, co-hohc or co-hohh depending on whether the set of all formulae occuring in its tree satisfy the syntax of co-fohc, co-fohh, co-hohc or co-hohh.
We now demonstrate the coinductive proofs in these four calculi using the running examples from Introduction. In all examples, we use symbol to denote the logic program that conists of clauses (1) – (9) given in Introduction. When we want to refer to a particular clause in , we will use notation .
Example 4 (Coinductive rules in co-fohc)
Figure 5 shows a proof involving clauses (6) and (7) from Introduction, and not involving infinite stream construction. The coinductive hypothesis and the goal is expressed in co-fohc. Notice how the coinductive goal remains guarded until the application of the rule , after which the coinductive hypothesis can be safely applied. As usual for coinductive proofs in co-fohc, the proof is regular, in the sense that the coinductive hypothesis taken at the start of the proof applies verbatim later in the proof.
Example 5 (Coinductive rules in co-hohc)
The next proof (for clauses (3) and (4)) is given in Figure 6. It is similar to the proof of Figure 5, in that it is also regular, and requires a coinductive hypothesis satisfying the syntax of Horn clause logic. However, this time the coinductive hypothesis involves construction of a stream of zeros, given as , where the fixed point term is defined in Example 2. In Introduction, we actually wanted to prove , but existential formulae are not allowed to be coinductive hypotheses, by the previous discussion. We can only prove if we add the coinductively proven lemma to . Thus, we can infer by the standard rules of hohc given in Figure 2.
In the next section, we will prove that such manipulation with proven lemmas is sound. Our proof can be seen as a semantic version of cut admissibility. However, we follow the uniform proof tradition and do not introduce a cut rule directly into the calculus.
Example 6 (Coinductive rules in co-hohh)
The next example of a coinductive uniform proof (for clause (8)) is given in Figure 7. It is again more complicated than the previous examples, in that it requires not just fixed point terms, but also the syntax of hereditary Harrop logic for its coinductive hypothesis and goal (given by ). To see this, suppose we tried to prove directly, following Example 5, and suppose we took the coinductive hypothesis . After resolving with the clause (8) via the rule , we would reach a goal to which the given coinductive hypothesis would not apply. The reason is irregularity of the stream in question, that requires us to prove a more general coinductive goal. As in the previous example, if we wanted to obtain a proof for , we can derive it by the rules of Figure 2 from .
Example 7 (Coinductive rules in co-fohh)
Finally, to complete the picture, we give an example of a proof in co-fohh in Figure 8. This example uses clause (9) and does not require infinite data construction via fixed-point terms, but unlike all other examples, it shows that implicative coinductive hypotheses may play an important role. If we wanted to coinductively prove that a bit [math] and some given stream, say , satisfy the relation , we would not be able to prove it directly: similarly to the case of Example 6, the proof is irregular. I.e., taking the coinductive hypothesis and goal , we would resolve it with the clause (9), only to get a subgoal , to which the given coinductive hypothesis would not apply. But we would be able to prove , if we coinductively prove first, as Figure 8 shows, and then use the extended logic program and the rules of Figure 2.
Although the last example looks somewhat artificial in the context of this paper, examples of similar proofs do arise in automated proving with Horn clauses, and in particular in implementation of Haskell type classes, as [18, 11] report. Appendix LABEL:sec:FP gives an example of a more complex proof in co-fohh, taken directly from [18].
4 Soundness of Coinductive Uniform Proofs for Logic Programs
We start this section by recalling the standard definitions of coinductive models for logic programs [25]. The first step in definition of such models is to define infinite tree-terms and tree-atoms that inhabit such models. We follow standard definitions in this regard [15], see Appendix 0.B. Informally, a tree-term is defined as a map from a set of lists of non-negative integers into , with tree branching respecting the term arity. If the domain of the map is infinite, the tree-term is infinite. This definition then extends to tree-atoms in an obvious way.
Given a first order signature and a logic program , the coinductive Herbrand universe of , denoted , is the set of all finite and infinite closed tree-terms on . The coinductive Herbrand base of , denoted , is the set of all finite and infinite closed tree-atoms on .
We first establish a connection between guarded atoms on and the coinductive Herbrand base of . It is a form of productivity result for guarded fixed-point terms.
If is a first order atom, then we will denote the equivalent tree-atom by . Let be a guarded atom on and let , then a snapshot of , denoted , is an atom obtained by replacing all guarded full terms in with , and it is understood that a guarded full term in is replaced by only if is not a first order term. Clearly, is a first order atom. A guarded atom has a fair infinite sequence of -reductions if every -reducible sub-term is reduced within a finite number steps. The next lemma relies on a standard definition of a metric on tree-terms from [25]. Given as two tree-terms (tree-atoms), denotes the distance between , where and the smaller is, the more similar are (cf. Appendix 0.B).
Lemma 1 (Productivity lemma)
Let be a guarded atom on a first-order signature and . If has a fair infinite sequence of one step -reductions , where is the -normal form of , then there exist an infinite tree-atom such that as . Moreover, if is a closed guarded atom, then .
Proof
Similar to the proof in Komendantskaya and Li [22, Lemma 4.1].
Lemma 1 allows us to extend the notation , from requiring be a first order atom, to allowing to be any guarded atom, and shows that if is closed.
We now proceed to consider coinductive models of logic programs. If a -formula in (co)-hohc is in the form
[TABLE]
then it is also called an -formula, which is perhaps a better known presentation of Horn clauses. It is well known that in both classical and intuitionistic logics, a set of Horn clause -formulae can be transformed into an equivalent set of -formulae, and vice versa [28, §2.6.2]. Also note that, by the discussion of the previous section, this is the only kind of formulae that we can coinductively prove using the co-fix rule.
Given an -formula , we define:
tree-form ground instance :
term-form ground instance :
where each
where each
If is a ground instance (in either tree-form or term-form), then we denote by and denote the set by .
A Herbrand interpretation, denoted , is any subset of . We denote a powerset of by . It is well known that is a complete lattice. Appendix 0.C recalls some standard lattice-theoretic definitions and results we use. The immediate consequence operator with respect to a logic program , , is defined as
[TABLE]
A Herbrand interpretation is a model of if and only if is a pre-fixed point of .
Using the fact that is increasing [25], we can rely on the Knaster-Tarski theorem (c.f. Appendix 0.C) to assert that its greatest fixed point exists:
[TABLE]
We say that is a coinductive model of .
In order to use these models for our main soundness results, we first need to formulate a coinductive principle for the proofs involving these models. The implication from right to left in Lemma 2 is an instance of the coinductive proof principle, as formulated e.g. in Sangiorgi [32, §2.4]:
Lemma 2 (Coinductive proof principle for coinductive models)
Let be a logic program, with the operator and the model . Given a set , , if and only if, there exist a Herbrand interpretation for , such that and is a post-fixed point of .
The proof is given in Appendix 0.D.
We are now ready to formulate soundness of coinductive uniform proofs. We prove the result for co-hohh, but, because proofs in co-fohc, co-fohh are co-hohc are, by definition, also proofs in co-hohh, their soundness relative to coinductive models follows as a corollary of this theorem.
Theorem 4.1 (Soundness of co-hohh proofs)
Let be a logic program with a coinductive model , be a -formula, and have a proof in co-hohh which involves only guarded atoms. Then, for an arbitrary tree-form ground instance of the goal, implies .
Proof (Sketch)
We use Lemma 2 from right to left, which means, to show that , we look for a set such that the requirements and are satisfied. The proof follows an Analysis–Construction–Verification structure, where we first study the proof of the root sequent which provides information for constructing a candidate set . In this construction, we use Lemma 1. Finally we verify that the set so constructed satisfies the requirements. The exact details of these three steps are given in Appendix 0.D.
Finally, we show that extending logic programs with coinductively proven lemmas is sound.
Theorem 4.2 (Conservative model extension)
Let a logic program have coinductive model , and a sequent have a co-hohh proof that only involves guarded atoms. Let be distinct term-form ground instances of involving only guarded atoms, and such that for each ( ), if , then . Let have a coinductive model . Then, .
Proof (Sketch)
The proof shows equality of the two sets by proving that they are each other’s subset. Theorem 4.1 and Lemma 2 are used. The exact details are given in Appendix 0.D.
By Theorem 4.1, proofs for logic programs and are sound relative to their coinductive models. But, subject to conditions of Theorem 4.2, the models of these two programs are equivalent. Hence, proofs for are coinductively sound relative to the coinductive model of .
5 Conclusions, Discussion, Future and Related Work
We have presented a sound method for proving coinductive properties of theories expressed in first-order Horn clause logic. We used the four calculi of the “uniform proof diamond” to distinguish important classes of these coinductive properties. The major division is between classes of properties involving (or not involving) infinite data structures, accommodated by higher-order/first-order division of the diamond. Then classification further splits into regular and irregular cases of coinductive reasoning, accommodated by Horn clause logic/hereditary Harrop clause logic parts of the diamond.
The most intriguing future direction is to explore how these results may be applied in automated reasoning systems based on first-order logic [8]. The methods presented here are different from most popular coinductive methods, such as [14, 19, 9], which are based on higher-order logic and/or dependent type theory with (co)inductive data types. For example, in Coq we would need to implement clauses (3), (6), (8), (9) as coinductive types, each clause would be inhabited by a constant proof term, seen by Coq as a coinductive type constructor (the code is given in Appendix 0.E). Coq’s way of ensuring soundness of these proofs is type-checking backed by the guardedness checks at the proof term level. Proof terms that inhabit proven propositions must be guarded by constructors of the coinductive type in question. In comparison, we formulated the coinductive calculi without any notion of (co)inductive data types, or any generation of proof terms. Instead of guarding proof terms, we use rules of Figure 4 to guard applications of the coinductive hypotheses. When working with definitions of infinite streams, we introduce only minimal guardedness checks on fixed point terms.
In this respect, of particular interest is the clean separation between coinductive proofs involving (or not involving) fixed point terms made by the coinductive diamond. Thus, depending on first-order theory in question, we can now choose to work with one or the other kind of coinduction: if a certain prover’s syntax does not admit fixed point terms, there are still co-fohc and co-hohh available for it. This differs from majority of automated coinductive methods [9, 24], that were proposed with (co)inductive data structures in mind. This paper shows that having coinductive data structures is not at all a pre-requisite for having sound coinductive proofs.
An interesting direction for future work is to generalise our definition of guarded fixed point terms, e.g. benefiting from recent new methods by Blanchette et al. [10]. Adding data structures explicitly to the syntax of unform proofs is a related task, and deserves attention. In a sense, a similar work has already been done in a richer system – Abella [2]. Compared to these richer languages, our current paper helped us to explain and systematise the kinds of coinductive reasoning available for first-order Horn clauses.
The coinductive uniform proofs cannot capture all coinductive properties arising in first-order Horn clause logic. Consider the following logic program defining a Fibonacci stream:
(10)
(11)
(12)
The syntax of co-hohh would allow us to express the coinductive property , where is a guarded fixed-point term (relying on a function ). We would even be able to safely apply the coinductive hypothesis in the proof. However, the problem arises with inductive parts of this proof. It inevitably stumbles upon having to prove and use a relatively trivial property . However, it can only be proven by induction, and the original formulation of uniform proofs does not admit the inductive proof principle [28]. Stating this property as part of the logic program would violate our assumption that the given logic program is first-order ( is defined by -abstraction). This suggests two future directions.
Firstly, it would be useful to complement our coinductive proof principle with an inductive one. Inductive proof principle has been introduced in a similar framework in [26, 2]. With this additional tool at hand, the question of mixing induction and coinduction will arise, and several existing methods, such as those given in [4], may prove useful.
Alternatively, we could lift our current restrictions and allow the syntax of co-hohh in logic programs. Section 3 formulates the four coinductive calculi with this generalisation in mind. However, to prove soundness of these logics, we would need to use a much more sophisticated notion of a coinductive model, which was beyond the scope of this paper. Categorical models for mixed induction and coinduction by Basold [4, 5] seem promising in this respect.
In this paper, we only worked with one definition of fixed-point operator at the term level. A solid body of literature exists on introducing both fixed point and co-fixed point operators (also sometimes known as and operators) to calculi similar to ours: [3, 1, 12, 4]. We plan to look into these methods when extending the notion of a logic program to co-hohh, and/or extending our four calculi with the inductive proof principle.
An orthogonal, but promising direction would be to give a Curry-Howard interpretation to our calculi, as was done already for co-fohc and co-fohh in [18]. There, Horn clauses are seen as types, and terms inhabiting these types are constructed alongside the proof rule applications. Note that all four calculi we have introduced here are intuitionistic and hence in principle should allow constructive interpretation. Extension of [18] to co-hohc and co-hohh would require dependent types, similar to [4, 5]. This work could help to automate coinductive proofs in interactive theorem provers (such as Coq or Agda), which are based on constructive type theory.
Finally, we plan a more systematic study of syntactic and semantics approaches to the cut rule in presence of (mixed) inductive and coinductive proofs, in order to better relate results of Section 4 to the existing literature on the subject [26].
Appendix 0.A Omitted Standard Syntactic Definitions
In this section, we complete some of the omitted standard syntactic definitions omitted in Section 2. The textbook [28] gives the full details on uniform proofs.
Free Variables
for all 2. 2.
for all 3. 3.
for all 4. 4.
for all and 5. 5.
Typing Rules
If maps constant to type , we write . Moreover we write (or ), to denote . Similar notations apply to .
Definition of a Sub-term
if or 2. 2.
3. 3.
4. 4.
5. 5.
in case we use to denote an unknown (thus not analysable) term, we define that
Definition of Substitution
2. 2.
, if is distinct from , or 3. 3.
4. 4.
5. 5.
Let denote the result of replacing every free occurrence of variable in lambda term by variable . , if both and
-Equivalence, Identity
The relation , expressed with symbol , is defined as: , provided that does not occur in . Moreover, for arbitrary term and variable , we define that , and that if , then , , , and , and that if both and , then . We use to denote the relation of syntactical identity modulo -equivalence.
Syntactic Conventions
The outermost parentheses for a term can be omitted. Application associates to the left. Application binds more tightly than abstraction, therefore stands for . The constants are used as infix operators with precedence decreasing in the same order therein, and they all bind less tightly than application but more tightly than abstraction. For instance, stands for . We may combine successive abstraction under one , for instance, instead of . Successive quantification with the same quantifier can be combined under a single quantifier, for instance, we write instead of .
Appendix 0.B Tree Terms and Atoms
We write for the set of all non-negative integers, and write for the set of all finite lists of non-negative integers. Lists are denoted by where . The empty list is denoted . If , then denotes the list which is the concatenation of and . If and , then denotes the list .
Definition 5 (Tree Language)
A set is a (finitely branching) tree language provided: i) for all and all , if then and, for all , ; and ii) for all , the set of all such that is finite. A non-empty tree language always contains , which we call its root. A tree language is finite if it is a finite subset of , and infinite otherwise. We use to denote the length of list , called the depth of the node if is a tree language.
Arity
Given a first-order signature , the type of a non-logical constant in can be depicted as where is either or , and the arity of is defined as the number of occurrences of in the type of . A variable of type has arity [math].
Definition 6 (Tree-Terms, Tree-Atoms)
If is a non-empty tree language, is a first-order signature, and is a context that assigns the type to variables, then a tree-term over is a function such that, i) for all , is either a variable in , or a non-logical constant in which is not a predicate, and ii) the arity of equals to the cardinality of the set . If, for , , we say is a leaf of the tree-term . A tree-atom over is defined in the same way as a tree-term except that the root of is mapped to a predicate in . We use to denote arbitrary tree-terms (tree-atoms). The domain of a tree-term (tree-atom) is denoted . A tree-term (tree-atom) is closed if no is mapped to a variable, otherwise is open.
Tree-terms (tree-atom) are finite or infinite if their domains are finite or infinite. Substitution of a tree-term for all occurrences of a variable in a tree-term (tree-atom) , denoted , is defined as follows: let be the result of the substitution, then i) is the union of with the set , and ii) if and ; if .
Example 8 (Tree-term)
Let contain non-logical constants , and . Let contain .
Let . A finite closed tree-term is defined by the mapping , such that , , . 2. 2.
Let , denoting the set of all finite (possibly empty) lists of 1’s. Let be the smallest tree language containing , which amounts to the union of and , where . An infinite open tree-term is defined by the mapping , such that for all , , and for all , .
Definition 7 (Tree-Term (Tree-Atom) Metric [25])
Given a term on where , the truncation of a tree-term (or tree-atom) at depth , denoted by , is constructed as follows:
(a) the domain of the term is ;
(b)
[TABLE]
For tree-terms (or tree atoms) , we define , so that is the least depth at which and differ. If we further define if and otherwise, then the set of tree-terms and atoms on equipped with metric is an ultrametric space.
Appendix 0.C Lattice-Theory and Fixed Point Theorem
Let set be a set equipped with a partial order , denoted , and let , and . If for all , , then is called a lower bound of . If for all , , then is called a upper bound of . Further, let be a lower bound and a upper bound of , respectively, then, if for all lower bounds of , , then is the greatest lower bound of , denoted , and, if for all upper bounds of , , then is the least upper bound of , denoted . A partially ordered set is a complete lattice if for all subset , there exist and .
Example 9
Given a set , its power set is denoted . Then is a complete lattice, as for each subset of , is given by , and is given by .
Definition 8 (Fixed points)
Given a complete lattice , a function is increasing if whenever . Moreover, given an , is a fixed point of if ; is a pre-fixed point of if ; is a post-fixed point of if . We call the least fixed point of , denoted , if is a fixed point of , and for all fixed points of , . The greatest fixed point of , denoted , is defined similarly.
**Theorem (Knaster-Tarski). **Given a complete lattice and an increasing function ,
[TABLE]
Appendix 0.D Full Proof of Soundness Theorems
In this Section, we give full proofs for the main Lemma and Theorems of Section 4.
0.D.1 Corollaries for Lemma 1 (Productivity Lemma)
Corollary 1 and Corollary 2 follow from Lemma 1.
Corollary 1 (Productivity of Guarded Full Terms )
If (which is not a first order term) on is a closed guarded full term, or is -equivalent to a closed guarded full term, then there exist an equivalent infinite tree-term . Further, if is closed, then .
Corollary 2 (Tree Sharing Among fix-Equivalent Guarded Atoms)
If are guarded atoms and they are pairwise -equivalent, then .
0.D.2 Lemma 2 (Coinductive proof principle)
Lemma 2 (Coinductive proof principle for coinductive models). *Let be a logic program, with the operator and the model . A set , if and only if, there exist a Herbrand interpretation for , such that and is a post-fixed point of . *
Proof
We first prove the implication from right to left. This is justified by the definition of .
Then we prove from left to right. implies that for all , . Then, by the definition of , for all , there exist an , such that and . Then let . By the construction of , we have . Also we have , for all . Since is increasing, , for all . By transitivity of , , for all . So , by the construction of .
0.D.3 Proof of Theorem 4.1 (Soundness of Coinductive Uniform Proofs)
Theorem 4.1 (Soundness of co-hohh proofs). Let be a logic program with coinductive model , be a -formula, and have a proof in co-hohh which involves only guarded atoms. Then, for an arbitrary tree-form ground instance of the goal, implies .
Proof
We use Lemma 2 from right to left, which means, to show that , we look for a set such that the requirements and are satisfied. 2. 2.
The proof follows an Analysis–Construction–Verification structure, where we first study the proof of the root sequent
[TABLE]
which provides a clue for constructing a candidate set . Finally we verify that the set so constructed satisfies the requirements.
Analysis
The proof for the root sequent starts with the following steps.
[TABLE]
where (the coinductive hypothesis) is
[TABLE]
and is a short hand for , and is a short hand for . 2. 4.
The steps in 3 extend the signature from to . Given a formula , we will distinguish its term-form ground instance based on (denoted with ) from its term-form ground instance based on (denoted with ). Moreover, if a lambda term on , contains some (or none) of the eigenvariables , we will use notation to refer to it, and particularly, we reserve for an arbitrary such atomic -formula. We define a referent of (provided is guarded), as
[TABLE]
where , , and, regarding the definition of substitution, are technically treated as free variables in . 3. 5.
The proof for the root sequent proceeds as follows:
[TABLE]
where (the hypothesis) is and . Note that the above step is also the only occasion in the proof where the rule is used (and this shall become clearer as we further analyse the sequent proof). We will use as the general form of a fact in , as the general form of a rule in , and write for . can be either a fact or a rule. 4. 6.
If is a fact, then the proof for the root sequent proceeds as follows:
[TABLE]
where . This situation is trivial and we can do the post-fixed point construction and verification immediately, as follows. Note that (which the head of an arbitrary tree-form ground instance of the goal mentioned in the theorem) is a referent of . Since , then by Corollary 2, , so is a referent of . A referent of , i.e. , is a tree-form ground instance of . Then, let , we have . Now we have verified that satisfies the requirements (cf. 1). 5. 7.
If is a rule, then the proof for the root sequent proceeds as follows:
[TABLE]
where is
[TABLE]
and the root of is labelled by
[TABLE] 6. 8.
The step in 7 removes the coinductive status of goals in its upper sequents, then is a uniform proof in the style of Miller and Nadathur [27]. It is important to know that has the following properties. 7. 9.
We pay attention to two kinds of sequents involved in :
- (a)
Sequents, whose right side is a conjunction of (at least two) atoms, in the form
For instance, the sequent labelling the root of is in this form. 2. (b)
Sequents, whose right side is a single atom, in the form
8. 10.
In , for each sequent in the form (9a), a succession of steps are used to break it down to a series of sequents
[TABLE]
which are in the form (9b). 9. 11.
In , for each sequent in the form (9b), only the decide rule can be used as the next step of reduction, and there are four cases of possible development, as follows.
- (a)
decide selects a fact from .
[TABLE]
where . 2. (b)
decide selects a rule from .
[TABLE]
where is
[TABLE]
and the root of is labelled by
[TABLE]
which is a sequent of the form (9a). Note that the selected rule is possibly different from the rule selected in 7 although the same formula is used to depict the selected rule. 3. (c)
decide selects the coinductive hypothesis .
[TABLE]
where refers to
[TABLE]
for some guarded full terms — These terms are guarded full terms because the theorem assumes that all atoms involved in the sequent proof are guarded, both before substitution and after substitution. Then a case analysis on a variable being substituted, reveals that the substituting terms must be guarded full terms. is
[TABLE]
and the root of is labelled by
[TABLE]
which is a sequent of the form (9a). Let denote the substitution
[TABLE]
Later we will see that the above mentioned plays an central role in the construction of the post-fixed point. 4. (d)
decide selects the hypothesis .
[TABLE]
where for some and .
Construction
We now use the above analysis of the proof of the root sequent to construct the post-fixed point . It remains to work with the case when the program clause selected by is a rule (cf. 5, 6, 7). The main difficulty in construction in this situation arises when the post-fixed point in question is an infinite set, which happens when a proof exhibits certain irregularity. 2. 13.
Firstly, let the formula (as mentioned in the theorem) be computed by
[TABLE]
for some arbitrary . 3. 14.
Note that the rules of our coinductive calculus allow us to form only one coinductive hypothesis in a proof for the root sequent, but the proof may use this coinductive hypothesis more than once. Suppose that the coinductive hypothesis is used in the given proof times. Let . 4. 15.
Consider the times when the coinductive hypothesis was used. In each case, a substitution was constructed, as described above in 11c. Let us denote all these substitutions by . 5. 16.
Each () is given by
[TABLE]
where is given by in , as in 11c. (Note that each time the same coinductive hypothesis is used.) 6. 17.
Given that the proof of the root sequent uses exactly the eigenvariables , we want to define a set of mapping for the eigenvariables into in order to construct the post-fixed point. So, we define to denote the set of all finite lists on , including the empty list , and define the set of substitutions, where is a function defined by recursion, as follows.
- (a)
Base case:
[TABLE] 2. (b)
Recursive case: If , then
[TABLE]
where the notation is used to denote application of the substitution to the tree-term . Note that is a valid notation due to Corollary 1 and the fact that is a guarded full term (cf. 11c).
Since is an infinite set, this construction is potentially infinite, and moreover, through recursive application of substitutions at each iteration of it can construct an infinite set of substitutions. 7. 18.
Note that the above construction involving can and will be used to construct models generally, even when the coinductive hypothesis was not applied (i.e applied times). 8. 19.
We define the set , as the collection of all atoms , where is the atom on the right side of some sequent , where is in . In addition, we add to , i.e. we add the tree corresponding to the atom occurring in the lower sequent in the step (cf. 5). Note that the in that sequent should intuitively be seen as a coinductive conclusion. 9. 20.
We use to denote the set resulted from applying substitution to all members of . We define as
[TABLE] 10. 21.
Given , by Lemma 2 (used from left to right), there exist a set , such that and is a post-fixed point of . 11. 22.
Now we construct a candidate post-fixed point , given as
[TABLE]
Verification
We verify that set satisfies the two requirements (cf. 1). 2. 24.
is proved by
[TABLE] 3. 25.
It remains to show that is a post-fixed point of . In other words, we need to show that each member of is also a member of . 4. 26.
For all , , as proven by the following argument:
[TABLE] 5. 27.
By definition of , for all , for some , and has an underlying atom such that
[TABLE]
Let be the sequent from where we get the atom . We show using a case analysis 27a – 27d, with respect to the ways 11a – 11d in which the sequent is reduced.
- (a)
If is reduced in the way 11a, then there exist a fact in , such that , then (by Corollary 2), so there exist tree-form ground instance such that . So . 2. (b)
If is reduced in the way 11b (note that this is also the case when ), then there exist a rule such that , and for each , . Note that by Corollary 2. Then there exist a tree-form ground instance for , whose head is , and whose body is the set such that if and only if there exist and . Then, for all , . So . 3. (c)
If is reduced in the way 11c, then the use of results in existence of for some , given as
[TABLE]
and . Note that
[TABLE]
because, by definition of ,
[TABLE]
So and this membership is underlain by . In light of this discovery, we start a new round of case analysis where we regard the same as a member of , then 27b applies, so . 4. (d)
If is reduced in the way 11d, it implies that for some . Further, by Corollary 2, . Then . We further inspect two sub-cases.
- i.
. Then , and , so . 2. ii.
. Then there exist such that . Then, there exist a use of that gives rise to , given as
[TABLE]
In addition, there exist (cf. 11c and 20). Note that
[TABLE]
This is because , by definition of , that
[TABLE]
Thus, , underlain by . In light of this discovery, we start a new round of case analysis where we regard the same as a member of . Note that whenever this branch, i.e. 27(d)ii, is reached, we take a new round of case analysis, thus entering into iteration if we repeatedly reach this branch. Since in each new round, we work with a smaller index, i.e. from to , iteration caused by this branch always terminates, ending in one of the branches 27a, 27b, 27c or 27(d)i in the final round. In all these possible final circumstances, previous analysis has shown that . 6. 28.
Now we have finished with showing that , and the proof is complete.
0.D.4 Proof of Theorem 4.2
**Theorem 4.2 (Conservative Model Extension). **
- Let a logic program have coinductive model , sequent have a co-hohh proof that only involves guarded atoms. Let be distinct term-form ground instances of involving only guarded atoms, and such that for each ( ), if , then . Let have a coinductive model . Then, .*
Proof
We first show . Let and denote immediate consequence operators for and , respectively. By definition of a coinductive model, we have
[TABLE]
Note that
[TABLE]
therefore .
Then we show . Given a set that is a post-fixed point of , we distinguish two cases concerning how is a post-fixed point, as follows.
For all , there exist , with tree-form ground instance , such that is the head of , and the body of is a subset of . In this case, is also a post-fixed point of . 2. 2.
There exist (, where the inequality is explained later), called outstanding members of , such that for all ()
- (a)
is the tree-atom equivalent to the head of some , and, the set of tree-atoms equivalent to the body of is a subset of , and 2. (b)
there does not exist , with tree-form ground instance such that is the head of , and the body of is a subset of .
Note that the total number of outstanding members in a given post-fixed point of must be finite, and more precisely, no more than , which is the number of ’s instances used to augment the program, to which outstanding members are associated. Because of existence of outstanding members, is not a post-fixed point of , but in below we can show that there exist a post-fixed point of , such that . As the theorem assumes that the set of tree-atoms equivalent to the body of each is a subset of , then by Theorem 4.1, . Then by Lemma 2, there exist a post-fixed point of , such that . Then let . It is easy to verify that is a post-fixed point of and .
Now we have shown that a member of is either a member of , or a subset of a member of the latter set. Therefore . The proof is complete.
Appendix 0.E Examples of this Paper in Coq: Horn clauses as Coinductive Data Types
In this section, we compare our four examples with alternative encoding in Coq. Of interest is Coq’s reliance on the notion of coinductive data types and checking guardedness of the proof terms. Both of these features are absent in the work we present. Therefore, the coinductive principle is formulated in this paper without relying on richer supporting infrastructure available in Coq.
0.E.1 Some minimal infrastructure
Variable A : Set.
CoInductive Stream : Set :=
Cons : A -> Stream -> Stream.
Notation (* … *) below stands for commented out text in Coq.
We could, but do not, use Coq’s inductive types Bool or nat in these examples, as none of our examples depends on induction on Booleans or natural numbers. Below, in order to mimic the minimalistic logic programming style, we define z, nil, O, I, s as arbitrary constants in a given set .
0.E.2 Example in cofohc
Firstly, we give a Coq proof for the clause (6) and the goal from Introduction. It uses a dummy function dummy_cons for list constructor , to emphasize that no induction on the list structure is needed. It uses Coq’s native definition of equality (in x = y) for brevity.
Note that the clause (6) is defined as coinductive type, with constructor member_cons.
Variable dummy_cons: A -> A -> A.
CoInductive member: A -> A -> Prop :=
| member_cons: forall (x : A) (y : A) (t: A),
member x (dummy_cons y t) /\ x = y -> member x (dummy_cons y t).
Variable z : A.
Variable nil: A.
Lemma circular_member: member z (dummy_cons z nil).
(* coinductive hypothesis (member z (dummy_cons z nil )) taken: *)
cofix CH.
(* one step resolution with the Horn clause: *)
apply member_cons.
(* split for conjunction, application of coinductive hypothesis: *)
split; trivial; try apply CH.
Qed.
Coq infers (and checks) that the type member z (dummy_cons z nil) is inhabited by the proof term member_cons (conj CH eq_refl), and that this term is guarded by the coinductive constructor member_cons. Thus type checking together with guardedness gives soundness to the cofix rule.
Similar construction of proof terms happens in the remaining examples of this section.
We cannot have a similar guardedness checks in coinductive uniform proofs, as we have no proof terms. Thus, the above guardedness check is replaced by rules of Figure 4.
0.E.3 Example in cohohc
For clauses (3)-(5) in Introduction:
Variable O : A.
Variable I : A.
Inductive bit : A -> Prop :=
| O_cons: bit O
| I_cons: bit I.
CoInductive bitstream: Stream -> Prop :=
| bitstream_cons: forall (x : A) (t: Stream),
bitstream t /\ bit (x) -> bitstream (Cons x t).
CoFixpoint z_str : Stream :=
Cons O z_str.
Note the below term z_str of type Stream is guarded by constructor Cons. Definition 3 insures this kind of guardedness in coinductive uniform proofs.
The proof below is then similar to the one we explained above:
Lemma bistreamO: bitstream z_str.
(* coinductive hypothesis (bitstream z_str) taken: *)
cofix CH.
(* forcing one-step stream reduction: *)
rewrite Stream_decomposition_lemma; simpl.
(* one step resolution with the Horn clause: *)
apply bitstream_cons.
(* split for conjunction, application of coinductive hypothesis: *)
split; try apply CH.
apply O_cons.
Qed.
0.E.4 Example in cofohh
For clause (9) in Introduction:
Variable f: Stream -> Stream.
CoInductive com_bit: A -> Stream -> Prop :=
| com_bit_cons: forall (x : A) (t: Stream),
com_bit x (f t) /\ bit (x) -> com_bit x t.
Lemma com_bit_lem: forall x y, bit x -> com_bit x y.
(* coinductive hypothesis (forall x y, bit x -> com_bit x y) taken: *)
cofix CH.
intros.
(* one step resolution with the Horn clause: *)
apply com_bit_cons.
(* split for conjunction, application of coinductive hypothesis: *)
split; try apply CH; assumption.
Qed.
Using coinductive lemma in other proofs:
Variable t: Stream.
Lemma com_bit_O: com_bit O t.
apply com_bit_lem; apply O_cons.
Qed.
0.E.5 Example in cohohh
For clause (8) in Introduction:
Variable s: A -> A.
CoInductive from: A -> Stream -> Prop :=
| from_cons: forall (x : A) (y: Stream),
from (s x) y -> from x (Cons x y).
CoFixpoint fromstr (x : A ) : Stream :=
Cons x (fromstr (s x)).
Lemma fromQ: forall x, from x (fromstr x).
(* coinductive hypothesis (forall x, from x (fromstr x)) taken: *)
cofix CH.
intros.
(* forcing one-step stream reduction: *)
rewrite Stream_decomposition_lemma; simpl.
(* one step resolution with the Horn clause: *)
apply from_cons.
(* application of coinductive hypothesis: *)
apply CH.
Qed.
Using coinductive lemma in other proofs:
Lemma from0: exists z, from O z.
exists (fromstr O).
apply fromQ.
Qed.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] D. Baelde. A Linear Approach to the Proof-Theory of Least and Greatest Fixed Points . Ph D thesis, Ecole Polytechnique, Paris, 2008.
- 2[2] D. Baelde et al. Abella: A system for reasoning about relational specifications. J. Formalized Reasoning , 7(2):1–89, 2014.
- 3[3] D. Baelde and G. Nadathur. Combining deduction modulo and logics of fixed-point definitions. In Proceedings LICS 2012 , pages 105–114. IEEE Computer Society, 2012.
- 4[4] H. Basold. Mixed Inductive-Coinductive Reasoning: Types, Programs and Logic . Ph D thesis, 2018.
- 5[5] H. Basold and H. Geuvers. Type theory based on dependent inductive and coinductive types. In LICS ’16 , pages 327–336, 2016.
- 6[6] H. Basold, E. Komendantskaya, and Y.Li. Coinduction in uniform: Foundations for corecursive proof search with Horn clauses. In ESOP’19 , 2019.
- 7[7] Y. Bertot and E. Komendantskaya. Inductive and coinductive components of corecursive functions in Coq. ENTSC , 203(5):25–47, 2008.
- 8[8] N. Bjørner et al. Horn clause solvers for program verification. In Fields of Logic and Computation II , volume 9300 of LNCS , pages 24–51, 2015.