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.