What I Learned This Week: Subset types, real numbers, and more Coq
WILTW #4
This has been a productive week with my Coqplexity project really starting to get off of the ground. Coqplexity is at the point now where it can automatically prove pretty much any polynomial Big O relation (as long as it’s true).
Some more work needs to be done in Coqplexity in order to make it more useful, but the foundation is there, and it’s been a good bit of experience in writing tactics and dealing with real numbers.
So, more stuff about subset types, tactics, and more!
More subset types, more pain
I had a brief conversation with Paolo G. Giarrusso while complaining about not being able to replace / rewrite a subterm in Coq. Initially I thought it was a notation thing, as I essentially had a goal like this:
a <= b <= c
Which uses a notation which unfolds to this:
a <= b /\ b <= c
I wanted to change, say, b <= c
with b <= c + 0
, and I was
having a lot of problems with this.
Turns out this had nothing to do with the notation. I actually had a subset type that I was using.
sc : {c : R | (0 < c)%R}
And my goal was this:
0 <= f n <= proj1_sig sc * g n
But I could not change proj1_sig sc * g n
with proj1_sig sc * g
n + 0
using:
replace (proj1_sig sc * g n) with (proj1_sig sc * g n + 0) by lra.
Which should have worked, dammit! And it turns out it does work if you have something like:
a, b, c : R
============================
a <= b <= c
However, because sc
is some fancy-pants dependent type I think the
rewrite
/ replace
tactics can’t actually tell that proj1_sig sc
= proj1_sig sc
(in theory they could, but it might be a bug /
limitation).
However, if you destruct the subset type to get c : R
, and Hc : 0
< c
, and simplify so you just have:
f, g : nat -> R
n : nat
c : R
Hc : 0 < c
============================
0 <= f n <= c * g n
Then replacements work as expected. Go figure! It does make some sense because equality between dependent types can be very complicated, and I guess that’s what’s going on here.
Coq coercion
Coq seems to have a lot of wonderful (and probably annoying when you delve deep enough) features for extending the environment. One example of this is the remarkably powerful notation feature, which I have used in Coqplexity to provide \(f \in O(g)\) style notation. Awesome stuff! Another thing in a similar vein that I have discovered is the coercion feature.
Basically you can define an automatic coercion between types, which is super useful if you want to use numerical literals and whatnot to convert between things. Also just useful to be able to specify what implicit coercions can be made as a user of the programming language, because the built in implicit coercions are never going to be perfectly what you want!
Tactic notations
Coq’s aforementioned notation feature also extends into tactics. I
have been writing a number of tactics for Coqplexity. One of the
things that I wanted to be able to do with my tactics was implement
the behavior that you see with tactics like simpl
, where you can
say simpl in H
to apply simplification in the hypothesis H
, or
simpl in *
which applies the tactic to every hypothesis and the
current goal.
It took me a little while to find out how to do this because searching for something like “Coq in Ltac” isn’t great!
Turns out this is done with tactic notations. I don’t know that I have done this perfectly, but this kind of thing is working well for me, though a bit repetitive:
Ltac unfold_ord :=
unfold ge_ord; unfold gt_ord; unfold le_ord; unfold lt_ord; simpl; ineq_fix.
Ltac unfold_ord_in H :=
unfold ge_ord in H; unfold gt_ord in H; unfold le_ord in H; unfold lt_ord in H; simpl in H; ineq_fix.
Ltac unfold_ord_all :=
unfold ge_ord in *; unfold gt_ord in *; unfold le_ord in *; unfold lt_ord in *; simpl in *; ineq_fix.
Tactic Notation "unfold_ord" "in" hyp(l) := unfold_ord_in l.
Tactic Notation "unfold_ord" "in" "*" := unfold_ord_all.
Real number literals
You would like to be able to write 3.14
as a “real number” in
Coq… I don’t think this is supported, though, since .
is used in
the tactic language. You can probably make notation that will work,
but it doesn’t seem to exist yet, at least not in Coquelicot.
Current recommendation: 314/100
Whatever, that’s fine for now!
Ring tactic
Somebody briefly on the #coq
IRC channel on Freenode was trying to
solve problems about rings. They wanted to know why the ring
tactic (essentially omega
for rings) could not solve this problem:
Require Import Coq.setoid_ring.Ring_theory.
Require Import Ring.
Require Import Omega.
Lemma SRNat : semi_ring_theory 0 1 plus mult eq.
Proof.
constructor;
intros;
(omega ||
apply mult_comm ||
apply mult_assoc ||
apply mult_plus_distr_r).
Qed.
Add Ring RNat : SRNat.
Goal forall (a b : nat), (a + b) * (a + b) = a * a + 2 * a * b + b * b.
Proof.
ring.
This is the kind of thing that I have some familiarity with after working on Coqplexity! I managed to figure out that:
- You need to introduce the variables
2 * a * b
is problematic
Why is 2 * a * b
problematic? Well, you see… Not all rings have
a “2”, so to speak! The ring
tactic is going to be operating with
only the axioms provided by rings / semirings. ring
knows about
things like 0
, 1
, plus
, and mult
, but it doesn’t know that
2 * a * b = a * b + a * b
. There’s no ring / semiring axiom that
this falls out from.
However, replace (2 * a * b) with (1 + 1) * a * b by omega
will
get you fixed up :).
Productivity
I have attempted to do more scheduling in org-mode, and have finally figured out some things about how org-mode is supposed to work? org-mode has the concept of “scheduling” and “deadlines”, but “scheduling” is not for scheduling when to work on something, or scheduling things like on a calendar. This has caused me some confusion. Apparently you are supposed to use plain timestamps for this (though this is not without problems either). More info here.
This is where Orgzly has forsaken me. Orgzly currently does not support plain timestamps. Which is unfortunately quite a glaring difference between how org-mode wants to work, and how orgzly wants to work.