Coq Evidence Files
This is a brief listing of the files used to declare evidence in Coq. They are listed in order of recommended reading. The Coq index and code listings were generated automatically with coqdoc. An archive of coq files can be downloaded here.


evidence
evidence.v contains all of the evidence declarations that match up with the evidence declarations from the document. This includes 1-implication, 2-implication NPC, equality, and evidence over triples


soundness
These are the definitions of soudness for 2-assertions, lists of 2-assertions, and all of the evidence defined in evidence.v


language
All definitions for expressions, commands and states.


operationalSemantics
Operational Semantics for the core SPARK language


soundnessProof
The proof of soundness for triple evidence.


evidenceGenerator
Evidence generator, along with a proof that evidence exists for generated triples


soundnessLemmas
Contains a number of lemmas used in the soundness proof. Also contains the proof for the mismatch case of conditional used in the soundness proof.


evalCompletion
Lemmas pertaining to expressions evaluating when all of their free variables are contained in some state


twoAssn
Definition for two assertions


synEq
Syntactic equality definition and lemmas


varLists
Useful lemmas for manipulating lists of variables and functions operating on them.


substLemmas
Properties of substitution.


twoISoundnessProof
Soundness of two implication evidence.


oiSoundness
Soundness of one implication evidence.


NPCSoudnenss
Soundness of NPC Evidence.


eqSoudnenss
Soundness of EQ Evidence.