, Lemma tarski reach: forall (R: seq -> SymState -> Prop)

, Coq parser for generating instances of the Knaster-Tarski theorem and the Coq tactic language Ltac for the remaining transformations. Those include the following ones, which turn a general coinductive goal ?X.(H 1 ? · · · ? H n ? ?F) into one satisfying the conditions (a), (b) and (c) above

, V(H) the goal ?X.(H ? ?F) is transformed into ?(X ? {x }).(H ? (x = x) ? ?F[x /x]), where x X and ?F[x /x] denotes the replacement of every occurrence of x by x in ?F, ? eliminating variables in V(?F) \ V(H): for each x ? V(?F) \

, ? eliminating non-variable terms in the conclusion: while the resulting goal can be written as ?X.(H ? C[t/x]) for some non-variable term t, it is transformed into ?(X ? {x }).(H ?

, H ? C) contains two instances of the same variable x: let C denote the formula C in which one copy of x is replaced by some x X. The goal becomes ?(X ? {x }), ? linearising the conclusion: while the resulting goal ?X

C. ). , After the three transformations we are left with goals satisfying (a), (b) and (c)

, We thus follow the approach outlined in Section 7.1.4 in order to state and proves the Coq version of Lemma 4, i.e., the Knaster-Tarski theorem for proof, The first step is to define the functional: Inductive proof(X: Rlf -> Prop) : Rlf -> Prop := | Stp: forall (l l' r: SymState), imp l (dsj l' r) -> imp

A. Stefanescu, ?. Ciobâc?, R. Mereuta, B. M. Moore, T. Serbanuta et al., All-path reachability logic, Log. Methods Comput. Sci, vol.15, issue.2, 2019.

C. A. Hoare, An axiomatic basis for computer programming, Commun. ACM, vol.12, issue.10, pp.576-580, 1969.

P. W. O'hearn, Separation logic, Commun. ACM, vol.62, issue.2, pp.86-95, 2019.

G. Rosu, A. Stefanescu, ?. Ciobâc?, and B. M. Moore, One-path reachability logic, 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pp.358-367, 2013.

A. Stefanescu, D. Park, S. Yuwen, Y. Li, and G. Rosu, Semantics-based program verifiers for all languages, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, pp.74-91, 2016.

D. Lucanu, V. Rusu, A. Arusoaie, and D. Nowak, Verifying reachability-logic properties on rewriting-logic specifications, Logic, Rewriting, and Concurrency -Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, vol.9200, pp.451-474, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01158941

S. Skeirik, A. Stefanescu, and J. Meseguer, Logic-Based Program Synthesis and Transformation -27th International Symposium, Lecture Notes in Computer Science, vol.10855, pp.201-217, 2017.

V. Rusu, G. Grimaud, and M. Hauspie, Proving partial-correctness and invariance properties of transition-system models, 2018 International Symposium on Theoretical Aspects of Software Engineering, TASE 2018, pp.60-67, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01962912

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science. An EATCS Series, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

V. Rusu and D. Nowak, Co)inductive proof systems for compositional proofs in reachability logic, Proceedings Third Symposium on Working Formal Methods, FROM 2019, pp.3-5
URL : https://hal.archives-ouvertes.fr/hal-02176456

, , vol.303, pp.32-47, 2019.

T. Nipkow, L. C. Paulson, M. Wenzel, /. Isabelle, and . Hol--a, Proof Assistant for Higher-Order Logic, vol.2283, 2002.

?. Ciobâc? and D. Lucanu, Automated Reasoning -9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC, vol.10900, pp.295-311, 2018.

D. Lucanu, V. Rusu, and A. Arusoaie, 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

B. M. Moore, L. Peña, and G. Rosu, Program verification by coinduction, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.10801, pp.589-618, 2018.

E. Giménez, Types for Proofs and Programs, International Workshop TYPES'94, vol.996, pp.39-59, 1994.

V. Rusu, G. Grimaud, and M. Hauspie, Proving partial-correctness and invariance properties of transition-system models, Sci. Comput. Program, vol.186, 2020.
URL : https://hal.archives-ouvertes.fr/hal-01962912

Y. Bertot and E. Komendantskaya, Inductive and coinductive components of corecursive functions in Coq, Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, vol.203, pp.25-47, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00277075

Y. Bertot and E. Komendantskaya, Using structural recursion for corecursion, Types for Proofs and Programs, International Conference, vol.5497, pp.220-236, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00322331

C. Hur, G. Neis, D. Dreyer, and V. Vafeiadis, The power of parameterization in coinductive proof, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pp.193-206, 2013.

D. Pous, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pp.307-316, 2016.

N. A. Danielsson, Beating the productivity checker using embedded languages, Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, vol.5, pp.34-54, 2010.

A. Abel and B. Pientka, Well-founded recursion with copatterns and sized types, J. Funct. Program, vol.26, p.2, 2016.

A. Lochbihler, Coinductive, Archive of Formal Proofs, 2010.

D. Sangiorgi, Introduction to Bisimulation and Coinduction, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00907026

W. P. De-roever, F. S. De-boer, U. Hannemann, J. Hooman, Y. Lakhnech et al., Concurrency Verification: Introduction to Compositional and Noncompositional Methods, vol.54, 2001.

G. D. Giacomo and M. Y. Vardi, Linear temporal logic and linear dynamic logic on finite traces, IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, pp.854-860, 2013.