Capture Calculus proofs

This project contains the Coq proofs for Capture Calculus

We developed the proofs with Coq version 8.10.0.

A makefile is attached, but to recreate it in case of problems, run the following command:

coq_makefile -f _CoqProject -o Makefile

Then, to actually build the proofs:

make

Overview

The proofs are based on an implementation of System F-Sub in locally nameless style.

All definitions can be found in the file CCsub_Definitions.v.
The files CCsub_Infrastructure.v and CCsub_Lemmas.v contain technical lemmas related to substitution and the locally nameless representation.
File CCsub_CvFacts.v contains lemmas about cv.
File CCsub_Hints.v contains hints and tactics we found useful for in the next file.
The file CCsub_Soundness.v contains lemmas leading to and including preservation and progress.
Finally, the file CCsub_Examples.v contains lemmas leading to and including preservation and progress.

Name		Name	Last commit message	Last commit date
Latest commit History 574 Commits
.envrc		.envrc
.gitignore		.gitignore
AdditionalTactics.v		AdditionalTactics.v
Atom.v		Atom.v
CC_Zoo.v		CC_Zoo.v
CCsub_Definitions.v		CCsub_Definitions.v
CCsub_Examples.v		CCsub_Examples.v
CCsub_Hints.v		CCsub_Hints.v
CCsub_Infrastructure.v		CCsub_Infrastructure.v
CCsub_Lemmas.v		CCsub_Lemmas.v
CCsub_Soundness.v		CCsub_Soundness.v
CCsub_Subcapt.v		CCsub_Subcapt.v
CCsub_Substitution.v		CCsub_Substitution.v
CCsub_Subtyping.v		CCsub_Subtyping.v
CCsub_Typing.v		CCsub_Typing.v
CCsub_Wellformedness.v		CCsub_Wellformedness.v
CaptureSets.v		CaptureSets.v
Environment.v		Environment.v
FSetDecide.v		FSetDecide.v
FSetNotin.v		FSetNotin.v
FiniteSets.v		FiniteSets.v
LibTactics.v		LibTactics.v
ListFacts.v		ListFacts.v
Makefile		Makefile
Makefile.conf		Makefile.conf
Metatheory.v		Metatheory.v
Nat.v		Nat.v
README.md		README.md
Tactics.v		Tactics.v
TaktikZ.v		TaktikZ.v
_CoqProject		_CoqProject
examples.md		examples.md
find_unused_definitions.py		find_unused_definitions.py
flake.lock		flake.lock
flake.nix		flake.nix
working.md		working.md