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.
Class InjTyp (S : Type) (T : Type) :=
mkinj {
inj : S -> T;
pred : T -> Prop;
cstr : forall x, pred (inj x)
}.
mkinj {
inj : S -> T;
pred : T -> Prop;
cstr : forall x, pred (inj x)
}.
BinOp Op declares a source operator Op: S1 -> S2 -> S3.
Class BinOp {S1 S2 S3:Type} {T:Type} (Op : S1 -> S2 -> S3) {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} {I3 : InjTyp S3 T} :=
mkbop {
TBOp : T -> T -> T;
TBOpInj : forall (n:S1) (m:S2), inj (Op n m) = TBOp (inj n) (inj m)
}.
mkbop {
TBOp : T -> T -> T;
TBOpInj : forall (n:S1) (m:S2), inj (Op n m) = TBOp (inj n) (inj m)
}.
Unop Op declares a source operator Op : S1 -> S2.
Class UnOp {S1 S2 T:Type} (Op : S1 -> S2) {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} :=
mkuop {
TUOp : T -> T;
TUOpInj : forall (x:S1), inj (Op x) = TUOp (inj x)
}.
mkuop {
TUOp : T -> T;
TUOpInj : forall (x:S1), inj (Op x) = TUOp (inj x)
}.
CstOp Op declares a source constant Op : S.
Class CstOp {S T:Type} (Op : S) {I : InjTyp S T} :=
mkcst {
TCst : T;
TCstInj : inj Op = TCst
}.
mkcst {
TCst : T;
TCstInj : inj Op = TCst
}.
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.
Class BinRel {S:Type} {T:Type} (R : S -> S -> Prop) {I : InjTyp S T} :=
mkbrel {
TR : T -> T -> Prop;
TRInj : forall n m : S, R n m <-> TR (@inj _ _ I n) (inj m)
}.
mkbrel {
TR : T -> T -> Prop;
TRInj : forall n m : S, R n m <-> TR (@inj _ _ I n) (inj m)
}.
PropOp Op declares morphisms for <->.
This will be used to deal with e.g. and, or,...
Class PropOp (Op : Prop -> Prop -> Prop) :=
mkprop {
op_iff : forall (p1 p2 q1 q2:Prop), (p1 <-> q1) -> (p2 <-> q2) -> (Op p1 p2 <-> Op q1 q2)
}.
Class PropUOp (Op : Prop -> Prop) :=
mkuprop {
uop_iff : forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1)
}.
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
Class BinOpSpec {S T: Type} (Op : T -> T -> T) {I : InjTyp S T} :=
mkbspec {
BPred : T -> T -> T -> Prop;
BSpec : forall x y, BPred x y (Op x y)
}.
Class UnOpSpec {S T: Type} (Op : T -> T) {I : InjTyp S T} :=
mkuspec {
UPred : T -> T -> Prop;
USpec : forall x, UPred x (Op x)
}.
mkbspec {
BPred : T -> T -> T -> Prop;
BSpec : forall x y, BPred x y (Op x y)
}.
Class UnOpSpec {S T: Type} (Op : T -> T) {I : InjTyp S T} :=
mkuspec {
UPred : T -> T -> Prop;
USpec : forall x, UPred x (Op x)
}.
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.
Class Saturate {T: Type} (Op : T -> T -> T) :=
mksat {
mksat {
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)
PArg1 : T -> Prop;
PArg2 : T -> Prop;
PRes : T -> Prop;
PArg2 : T -> Prop;
PRes : T -> Prop;
SatOk states the correctness of the reasoning
SatOk : forall x y, PArg1 x -> PArg2 y -> PRes (Op x y)
}.
}.
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.
Record injterm {S T: Type} (I : S -> T) :=
mkinjterm { source : S ; target : T ; inj_ok : I source = target}.
Record injprop :=
mkinjprop {
source_prop : Prop ; target_prop : Prop ;
injprop_ok : source_prop <-> target_prop}.
Lemmas for building rewrite rules.
Definition PropOp_iff (Op : Prop -> Prop -> Prop) :=
forall (p1 p2 q1 q2:Prop), (p1 <-> q1) -> (p2 <-> q2) -> (Op p1 p2 <-> Op q1 q2).
Definition PropUOp_iff (Op : Prop -> Prop) :=
forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1).
Lemma mkapp2 (S1 S2 S3 T : Type) (Op : S1 -> S2 -> S3)
(I1 : S1 -> T) (I2 : S2 -> T) (I3 : S3 -> T)
(TBOP : T -> T -> T)
(TBOPINJ : forall n m, I3 (Op n m) = TBOP (I1 n) (I2 m))
(s1 : S1) (t1 : T) (P1: I1 s1 = t1)
(s2 : S2) (t2 : T) (P2: I2 s2 = t2): I3 (Op s1 s2) = TBOP t1 t2.
Lemma mkapp (S1 S2 T : Type) (OP : S1 -> S2)
(I1 : S1 -> T)
(I2 : S2 -> T)
(TUOP : T -> T)
(TUOPINJ : forall n, I2 (OP n) = TUOP (I1 n))
(s1: S1) (t1: T) (P1: I1 s1 = t1): I2 (OP s1) = TUOP t1.
Lemma mkrel (S T : Type) (R : S -> S -> Prop)
(I : S -> T)
(TR : T -> T -> Prop)
(TRINJ : forall n m : S, R n m <-> TR (I n) (I m))
(s1 : S) (t1 : T) (P1 : I s1 = t1)
(s2 : S) (t2 : T) (P2 : I s2 = t2):
R s1 s2 <-> TR t1 t2.
Hardcoded support and lemma for propositional logic
Lemma and_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 /\ s2) <-> (t1 /\ t2)).
Lemma or_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 \/ s2) <-> (t1 \/ t2)).
Lemma impl_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 -> s2) <-> (t1 -> t2)).
Lemma iff_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 <-> s2) <-> (t1 <-> t2)).
Lemma not_morph : forall (s1 t1:Prop), s1 <-> t1 -> (not s1) <-> (not t1).
Lemma eq_iff : forall (P Q : Prop), P = Q -> (P <-> Q).
Lemma rew_iff (P Q : Prop) (IFF : P <-> Q) : P -> Q.
Definition identity (A : Type) : A -> A := fun x => x.
Registering constants for use by the plugin
Propositional logic
Identify function