Verification of a partial evaluation algorithm for S-Graph in Coq. The algorithm was taken from "https://link.springer.com/chapter/10.1007/3-540-57264-3_34"
Utility lemmas and tactics. Includes lia
analogue for ssreflect --
ssrnatlia
, extracted from https://github.com/amahboubi/lia4mathcomp by Assia
Mahboubi.
Substitution Theory and basic definitions
Interpretation algorithm and its basic properties
Specification algorithm and proof of its correctness
Some example