, Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science. An EATCS Series, 2004.
, Friends with Benefits -Implementing Corecursion in Foundational Proof Assistants, ESOP, Lecture Notes in Computer Science, vol.10201, pp.111-140, 2017.
, A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems, IJCAR, Lecture Notes in Computer Science 10900, pp.295-311, 2018.
, Codifying Guarded Definitions with Recursive Schemes, TYPES, Lecture Notes in Computer Science 996, pp.39-59, 1994.
, An Axiomatic Basis for Computer Programming, Commun. ACM, vol.12, issue.10, pp.576-580, 1969.
, The power of parameterization in coinductive proof, Georg Neis, Derek Dreyer & Viktor Vafeiadis, pp.193-206, 2013.
, A generic framework for symbolic execution: A coinductive approach, J. Symb. Comput, vol.80, pp.125-163, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01238696
, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications. In: Logic, Rewriting, and Concurrency, vol.9200, pp.451-474, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01158941
, Program Verification by Coinduction, ESOP, Lecture Notes in Computer Science 10801, pp.589-618, 2018.
, Isabelle/HOL -A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol.2283, 2002.
, Separation logic, Commun. ACM, vol.62, issue.2, pp.86-95, 2019.
, Concurrency Verification: Introduction to Compositional and Noncompositional Methods, vol.54, 2001.
, One-Path Reachability Logic, pp.358-367, 2013.
, Proving Partial-Correctness and Invariance Properties of Transition-System Models, pp.60-67, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01816798
, Proving Partial-Correctness and Invariance Properties of Transition-System Models, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01816798
, Introduction to Bisimulation and Coinduction, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00907026
, A Constructor-Based Reachability Logic for Rewrite Theories, LOPSTR, Lecture Notes in Computer Science 10855, pp.201-217, 2017.
, All-Path Reachability Logic, Traian-Florin Serbanuta & Grigore Rosu, vol.15, issue.2, 2019.
, Semantics-based program verifiers for all languages, OOPSLA, ACM, pp.74-91, 2016.
, We now show (??) (hd ? ). Indeed, by the definition of the ? function, the latter statement amounts to the existence of some state s ? S such that l s and s ? (hd ? ); taking s = s satisfies this. Hence, lhs(?l ? r) (hd ? ) and from S | = ?l ? r we obtain by Definition 2 that ? r, which, ? (step) Consider any path ? such that (lhs(l ? r)) (hd ?), i.e., l (hd ?)
,
,
, hd ?) ? S . Hence, the set T ? of prefixes of ? is nonempty. Since all sequences in T ? are finite, there is one ? m with maximal length k = len ? m
, Since ? m ? T ? , in order to show ? m ? Paths S we only need ( ?): s m ? ? S . The are two cases: ? if k = len ? then s m is the last state on ? ? fPaths S , hence
, from s m ? S and s m ? ? (k + 1) and hypotheses one has s m ? ? (k + 1), hence, ? m ? ? (k + 1) ? T ? , in contradiction with the maximal length of of ? m in T ? . From ? (k + 1) ? S \ S and s m ? ? (k + 1) we obtain from the lemma, ? if k < len ? then ? (k + 1)
, Observe also that, since ? m ? T ? , we have that ? m is a prefix of ?, thus, for all j ? k = len ? m , ? m j = ? j, particular, hd ? m = hd ? and since we assumed l (hd ?) at the beginning, we also have l (hd ? m ). From the latter and ? m ? Paths S and S | = l ? r and Lemma 12 we obtain j ? len ? m = k ? len ? such that r
, we started with ? ? fPaths S arbitrarily chosen such that l (hd ?), and obtained j ? len ? such that r (? j), By Lemma, vol.12
, For all set X ? ? of hypotheses and ? ? X, if for all l ? r ? X
, Proof (sketch) Choose an arbitrary X ? ?. The hypothesis 'for all l ? r ? X, there is l ? ? such that l l r , l ? ? and ?l ? r ? X " is the expansion of X ? F(X) with F defined as above. By Tarski's principle, X ? ?F. We obtain that for all ? ? X
, We proceed by case analysis: ? first, assume ? = s for some s ? S . Since (?, r) ? R, there is l ? ? such that l ? r and l s. Now, l ? r implies that there is l ? ? with l l r, l ? ?, and ?l ? r. Next, l s and l l r imply l s or r s. Assume first l s. Since ? is the (singleton) path s, the state s is final, hence, ? s, Proof (sketch) We first prove the following fact ( ?): the relation R ? Paths × ? defined as follows: R ?(?, r).?l.(S l ? r ? l (hd?)) satisfies R ? . We use the coinduction principle for , i.e
, ? then, assume ? = s ? for some s ? S and ? ? Paths. We have two subcases: -if r s then (ii) holds
, We show (? , r) ? R. From (?, r) ? R we know that there is l ? ? such that S l ? r and l s. Now, S l ? r implies that there is l ? ? with l l r, l ? ?, and S ?l ? r. We prove (?l ) (hd ? ): from l s and ¬r s and l l r we obtain l s. Then, since ? is a path, then so is ? , and we have the transition s ? (hd ? ), Co)inductive proof systems for compositional proofs in reachability logic -otherwise ¬rs
, or (iii) from the coinduction principle -Lemma 1. Hence, the lemma ensures R ? , and ( ?) is proved. Coming back to our theorem: consider an arbitrary ? l ? r ? ? such that S l ? r. In order to show S | = l ? r, i.e., the conclusion of the theorem, we only need to show that for all paths ? such that l (hd ?), it holds that ? r. We do this by showing (?, r) ? R and using R ? from above. We have defined R = ?(?, r).?l.(S l ? r ? l (hd?)) and for our (?, r) there does, all possible cases, (?, r) ? R implies either statements (i), (ii)
, Consider the set X = {l ? r | l q r ? q ? ? ? ?q q r}. We show the premise of the lemma with the coinductive hypothesis X: ( ?) for all l ? r ? X, there exists l ? ? such that l l r and l ? ? and ?l ? r ? X, Let then l ? r be an arbitrary element in X. Hence, (i) l q r and (ii) q ? ? and (iii) ?q q r
, By choosing in ( ?) to instantiate the existentially quantified l to q, for any formula in X, the ( ?) statement is proved. Using the coinduction principle for (Lemma 2), for all ? ? X, it holds that S ?. Finally, the formula l ? r in our lemma's conclusion does belong to X since, by the lemma's hypotheses it satisfies all the conditions of membership in X. Hence, because of the hypothesis ?q q r of out lemma and (ii) and (iii)
, We find a state predicate q that, in the case ? is valid, satisfies the three inclusions in the hypothesis of Lemma 3 and implies ?. We define q ?s. ¬rs ? ?? ? Paths.( s = hd ? ? ? r), Proof Let ? l ? r
, l q r: let s be any state such that l s; we have to prove (q r) s. If r s the proof is done. Thus, assume ¬r s, and consider any path ? such that s = hd ?. From l s and s = hd ? and | = l ? r we obtain by Definition 2
, let s be any state such that q s; we prove that ? s is impossible. By the above definition of q, ¬rs. Consider an arbitrary path ? such that s = hd ?; again, by definition of q, ? r. Now, the only way ? r can hold when ¬rs holds is (cf. Definition 1) when ? = s ? for some path ? . Hence, s is not final
, ?q) s ; we have to prove (q r) s . By the definition of the symbolic transition function ?, there exists s such that s ? s and q s. By the definition of q, ¬r s and for each ? ? Paths such that s = hd ?, it holds that ? r. There are two subcases: ? if r s then
, Then, the sequence ? s s ? is a path and is such that s = hd ?, and, per the above, ? r. We also have ¬r s, and then the only way ? r may hold is via ? r (cf. Definition1). Summarising, in the case ¬r s , we get that any path ? such that s = hd ? satisfies ? r. Hence, q s by the definition of q, and therefore also, ? if ¬r s : consider any path ? such that s = hd ?
,
,
, We choose P = {l ? r ? ? | ?? ? fPaths, l (hd?) ? O(?, r)}, where O(?, r) is either ? (i) (?s.? = s ? r s), or
, ? (ii) (?s.?? .? = s ? ? r s), or
, ? (iii) (?s.?? .?n.?? .? = s ? ? ? = (suf ? n) ? ((? , r) ? Q ? ? ? r))
, This means that the coinduction principle for ? (Lemma 6) with the parameter R therein set to Q can be applied, hence, Q ? ?. As a consequence, any ? ? ? that satisfies the hypotheses of the theorem, in particular, such that S, H ?, and any ? ? fPaths such that (lhs ?)
, For such formulas, say, l ? r, it holds by definition of validity and Lemmas 12 and 7 that for all ? ? fPaths such that l (hd ?), either (?s.? = s ? r s) or (?s.?? .? = s ? ? r s) or (?s.?? .?n.?? .? = s ? ? ? = (suf ? n) ? ? ? r), ? Constraints 1 and 2 refer to valid formulas
, ? r ? P, and consider any ? ? f Paths such that l (hd ?). Then, we also have l (hd ?), and from l ? r ? P we obtain (i) or (ii) or (iii)
, If l 1 (hd ?), then l 1 ? r ? P implies (i) or (ii) or (iii), hence, (l 1 l 2 ) ? r ? P, ? For constraint 4, consider any ? ? fPaths such that
, Co)inductive proof systems for compositional proofs in reachability logic
, = s?r s) or (b) (?s.?? .? = s ? ?r s) or (c) (?s.?? .?n.?? .? = s ? ?? = (suf ? n)?((? , r) ? Q?? ? r)). Cases (a) and (b) imply either conditions (i) or (ii) for l ? r ? P, hence, we focus on case (c), in which there exist s, ? , n, ? such that ? = s ? ? ? = (suf ? n) ? ((? , r) ? Q ? ? ? r)). We obtain that there do exist s 0 = (hd ?), ? 0 = suf ? 1, ? For constraint 5: consider any ? ? fPaths such that l (hd ?). From | = l ? m we obtain thanks to Lemma 13 (transitivity item) some k ? (len ?) such that m (? k). Let ? = (suf ? k), then m (? k) means m (hd ? ), and from m ? r ? P we obtain that either (a) (?s.?
, Assume ? = s for some s ? S . Thus, l s and s is final, contradicting the hypothesis l ? ?. Hence, ? = s ? for some s ? S and ? ? fPaths. From ?l ? r ? ?µ S,H we obtain S, H ?l ? r. Moreover, from the definition of the symbolic transition function ? and s ? (hd ? ) and l s we obtain (?l) (hd ? )
, l ? r) and for all (b , ? )
, Thus, the last occurence last(b, l ? ? r ? ) of (b, l ? ? r ? ) in ? is a strictly positive natural number. In particular, there is H and a node N labelled S, H (b, l ? ? r ? ) that is on a pad of length last(b, l ? ? r ? ) from the root of ?. We shall be using the following observation several times hereafter: ( ?) for any direct successor labelled S, H (b , l ? r ) of the above node N, last(b , l ? r ) > last(b, l ? ? r ? ). Indeed, there are instances of (b , l ? r ) occuring further from the root of ? than the furthest instance of (b, l ? ? r ? ), Proof (sketch) Let ? be a proof of S, H (f, l ? r) and consider any
, Using Lemma 8: * either (f, ?) ? H, where H is the set of initial hypotheses. Hence, S | = ?, and using Lemma 12 we obtain k ? len ? such that (rhs ?) (? k), which proves the lemma in this case. * or (f, ?) H, which, again by Lemma8, implies (f, ?) ? Con. It follows that (?, f, ?) ? D, and, since b = t, (?, f, ?) ? (?, b, ?), -if the leaf results from applying [Hyp], then b = t and (f, ?)
, Depending on the rule: -if the rule is [Str], then N has one succesor labelled S, H (b, l ? r ? ) with l ? l . It follows that (b, l ? r ? ) ? Con and from (l ? ) (hd ?) and l ? l we get l
, Hence, (?, b, l ? r ? ) ? (?, b, l ? ? r ? ) and then using the well-founded induction hypothesis we obtain k ? len ? such that (rhs ?) (? k), proving the lemma in this case. -if the rule is [Spl] then l ? l 1 l 2 and the node N has two successors, labelled S, H (b, l 1 ? r ? ) and S, H (b, l 1 ? r ? ), respectively. Hence, (b, l 1 ? r ? ) ? Con and (b, l 2 ? r ? ) ? Con. From (l ? ) (hd ?) we obtain l 1, Moreover, using ( ?), last(b, l ? r ? ) > last(b, l ? ? r ? )
, proving the lemma in this subcase. The subcase l 2 (hd ?) is identical. -if the rule is [Tra] then the node N has two successors, labelled by S, H (b, l ? ? m) and by S, H (b, m ? r ? ), hence, (b, l 1 ? m) ? Con and (b, m ? r ? ) ? Con. It follows that (?, b, l ? ? m) ? D. Using ( ?), last(b, l ? ? m) > last(b, l ? ? r ? ). Hence, (?, b, l ? ? m) ? (?, b, l ? ? r ? ). B the well-founded induction hypothesis we get k 1 ? len ? such that m (? k 1 ). * if k 1 = 0 then m (hd ?). It follows that (?, b, m ? r ? ) ? D, and, using ( ?), last(b, m ? r ? ) > last(b, l ? ? r ? ). Hence, (?, b, m ? r ? ) ? (?, b, l ? ? r ? ), Then, (?, b, l 1 ? r ? ) ? D. Using ( ?), last(b, l 1 ? r ? ) > last(b, l ? ? r ? ). Hence, (?, b, l 1 ? r ? ) ? (?, b, l ? ? r ? ) and using the well-founded induction hypothesis we obtain k ? len ? such that (rhs ?) (? k)
, Setting k = k + 1 we get k ? len ? and ? k = ? k , thus, r ? (? k), which proves the lemma in this case. -if the rule is [Cut], then the node N has two successors labelled S, H (f, l ? ? r ? ) and S, H ? {(f, l ? ? r ? )} (b, l ? ? r ? ), respectively. However, by ( ?), N has no successor in ? with the conclusion (b, l ? ? r ? ), a contradiction. The rule is not applicable for the chosen node with its maximality property, ?l ? ? r ? ), thus, (t, ?l ? ? r ? )
, all possible cases, for the freely chosen (?, b, ?) ? D we found k ? len ? such that
, Theorem 7 (Soundness of .) If for all (b , ? )