Use `<:` (VMcast) for instances of `exact I` in lang/tactics.v

added 1 commit

1843d0c1 - Remove leftover comments.

That's surprising... I think vm_compute would introduce these casts itself. This is probably a Coq bug we should report.

Well, it's a trade-off. Using these casts does increase the size of the proof term because the goal becomes part of the term. In the case of λrust the increase does not seem to be relevant. But maybe one could imagine other developments where proof size is much more of an issue than reduction during Qed?

changed the description

That's pretty cool!

@robbertkrebbers any reason not to merge this?

@ppedrot we looked at LambdaRust performance before; this may interest you.

@ppedrot Am I right that vmcasts should be introduced automatically by vm_compute? In this case, why does this make any difference?

This looks great. We should also apply the same patch to heap_lang in Iris.

@janno why don't you immediately use vm_cast_no_check or whatever it's called?

@robbertkrebbers am I right in assuming that vm_cast_no_check will not check if the cast actually works? if so, the proof would only fail at Qed. That seems bad in terms of user experience.

For heap_lang these changes make no difference at all as far as I could tell. I have a branch (same name as this one) in iris-coq if you are interested.

@robbertkrebbers am I right in assuming that vm_cast_no_check will not check if the cast actually works? if so, the proof would only fail at Qed. That seems bad in terms of user experience.

Right, that makes sense.

For heap_lang these changes make no difference at all as far as I could tell. I have a branch (same name as this one) in iris-coq if you are interested.

Please make an MR ;)

I think it would be good to perform the patch there too, many people use heap_lang as a basis of defining their own language. Also, there is quite some stuff in iris_examples using heap_lang that could potentially benefit from a speedup.

@jung Feel free to merge!

(Feel free to squash commits in this PR. I don't think it needs to be 2 separate commits :D)

mentioned in commit d35b1cad

merged

I am really, really puzzled. I think we do not understand what is happenning here. I am sure that vm_compute does insert vm_casts in the term. First, the Qed would be much slower otherwise, and second, this is shown by the following example:

Lemma L : negb (negb true) = true.
Proof.
vm_compute. reflexivity.
Qed.

Print L.

This prints:

L = eq_refl <: negb (negb true) = true
     : negb (negb true) = true

So could someone explain me what is going on here?

I tried to come up with a minimal example to show the different, but failed:

Fixpoint slow (n : nat) :=
  match n with
  | 0 => 0
  | S n => slow n + slow n
  end.

Ltac exact_vm_cast t := match goal with |- ?P => exact (t <: P) end.

Goal slow 26 = 0.
Time exact_vm_cast (eq_refl 0).
Time Qed.

Goal slow 26 = 0.
Time vm_compute; reflexivity.
Time Qed.

Same here:

Fixpoint exp (n: nat) : nat :=
  match n with
    | 0 => 0
    | S n => exp n + exp n
  end.

Time Eval compute in exp 23. (* 6.5s *)
Time Eval vm_compute in exp 23.

Definition check_exp (n : nat) : Prop :=
  match exp n with
  | O => True
  | S _ => False
  end.

Goal check_exp 23.
  vm_compute. exact I.
Time Qed. (* 0.388s *)

Goal check_exp 23.
  exact (I <: check_exp 23).
Time Qed. (* 0.388s *)

:lol: we came up with literally the same slow function^^

Turns out @jjourdan was right; there was no performance improvement. We looked at the wrong numbers for the old time.

Use `<:` (VMcast) for instances of `exact I` in lang/tactics.v

Merge request reports

Activity