Library Coq.micromega.ZifyClasses
An alternative to
zify in ML parametrised by user-provided classes instances.
The framework has currently several limitations that are in place for simplicity.
For instance, we only consider binary operators of type
Op: S -> S -> S.
Another limitation is that our injection theorems e.g.
TBOpInj,
are using Leibniz equality; the payoff is that there is no need for morphisms...
An injection
InjTyp S T declares an injection
from source type S to target type T.
BinOp Op declares a source operator Op: S1 -> S2 -> S3.
Unop Op declares a source operator Op : S1 -> S2.
CstOp Op declares a source constant Op : S.
In the framework,
Prop is mapped to
Prop and the injection is phrased in
terms of
= instead of
<->.
BinRel R declares the injection of a binary relation.
PropOp Op declares morphisms for <->.
This will be used to deal with e.g. and, or,...
Once the term is injected, terms can be replaced by their specification.
NB1: The Ltac code is currently limited to (Op: Z -> Z -> Z)
NB2: This is not sufficient to cope with Z.div or Z.mod
After injections, e.g. nat -> Z,
the fact that Z.of_nat x * Z.of_nat y is positive is lost.
This information can be recovered using instance of the Saturate class.
Given
Op x y,
- PArg1 is the pre-condition of x
- PArg2 is the pre-condition of y
- PRes is the pos-condition of (Op x y)
SatOk states the correctness of the reasoning
The rest of the file is for internal use by the ML tactic.
There are data-structures and lemmas used to inductively construct
the injected terms.
The data-structures
injterm and
injected_prop
are used to store source and target expressions together
with a correctness proof.
Lemmas for building rewrite rules.
Hardcoded support and lemma for propositional logic
Registering constants for use by the plugin
Propositional logic
Identify function