diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-06 16:43:52 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-06 16:43:52 +0000 |
| commit | c5f077f5680951fff590082effa0e2843706962e (patch) | |
| tree | b648a4e9eb65a5b662321d9b7ae9f3a4a42f680e /theories/Classes | |
| parent | 9ed53a06a626b82920db6e058835cf2d413ecd56 (diff) | |
Numbers: finish files NStrongRec and NDefOps
- NStrongRec provides a "strong" recursor based on the usual one:
recursive calls can be done here on any lower value.
See binary log in NDefOps for an example of use.
- NDefOps contains alternative definitions of usual operators
(add, mul, ltb, pow, even, half, log)
via usual or strong recursor, and proofs of correctness and/or
of equivalence with axiomatized operators.
These files were in the archive but not being compiled,
some proofs of correction for functions defined there were missing.
By the way, some more iff-style lemmas in Bool.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12476 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/RelationPairs.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index c0e0bd61c..ecc8ecb79 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -110,10 +110,21 @@ Instance SndRel_sub {A B} (RA:relation A)(RB:relation B): subrelation (RA*RB) (RB @@ snd). Proof. firstorder. Qed. -Instance pair_compat { A B } (RA:relation A)(RB : relation B) : +Instance pair_compat { A B } (RA:relation A)(RB:relation B) : Proper (RA==>RB==> RA*RB) pair. Proof. firstorder. Qed. +Instance fst_compat { A B } (RA:relation A)(RB:relation B) : + Proper (RA*RB ==> RA) fst. +Proof. +intros A B RA RB (x,y) (x',y') (Hx,Hy); compute in *; auto. +Qed. + +Instance snd_compat { A B } (RA:relation A)(RB:relation B) : + Proper (RA*RB ==> RB) snd. +Proof. +intros A B RA RB (x,y) (x',y') (Hx,Hy); compute in *; auto. +Qed. Instance RelCompFun_compat {A B}(f:A->B)(R : relation B) `(Proper _ (Ri==>Ri==>Ro) R) : |