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:

  1. You need to introduce the variables
  2. 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.