Stream: Coq users

Topic: Opaque lemmas in dependent evaluation

Lef Ioannidis (May 25 2021 at 18:43):

Hi I'm using some lemmas from the Nat standard library with Nat indexed types, specifically I use Nat.max. Then I have a Program Fixpoint that uses a proof of Nat.sub_max_distr_r to solve obligations. Unfortunately, that lemma is opaque so when I try to simplify that fixpoint, I cannot unfold past that lemma. I tried using lia instead which succeeds in solving the obligation but also does not simplify. Is there some common solution except reprove everything in Nat.max with transparent theorems?

Lef Ioannidis (May 25 2021 at 19:32):

Here's my code, as you can see in the last evaluation of cbn evaluation stops at the Nat.sub_max_distr_r even though it has the arguments needed to reduce.

  Inductive term: nat -> nat -> Set :=
  | input(m: nat): forall (n: nat), term (S n) 0
  | output(m: nat): term 0 0
  | var(m: nat): forall (n: nat), term 0 (S n)
  | one(m: nat): term 0 0.

  Inductive additions: nat -> nat -> Type :=
  | ahead: forall i v, term i v -> additions i v
  | atail: forall i v i' v',
      term i v ->
      additions i' v' ->
      additions (max i i') (max v v').

  Definition substitute_inp{i v}(a: @term i v)(n: nat): @term (i-1) v :=
    match a with
    | input m 0 => one (m * n)
    | input m (S a) => input m a
    | output m => output m
    | var m n => var m n
    | one m => one m
    end.
  Program Fixpoint substitute_additions{i v}(a: @additions i v)(inp: nat): @additions (i-1) v :=
    match a with
    | ahead h => ahead (substitute_inp h inp)
    | atail h ts => atail (substitute_inp h inp) (substitute_additions ts inp)
    end.
  Next Obligation.
    apply Nat.sub_max_distr_r.
  Defined.

  Eval cbn in substitute_inp (input 2 0) 3.
  Eval cbn in substitute_additions (ahead (input 2 0)) 3.
  Eval cbn in substitute_additions (atail (output 2) (ahead (input 2 0))) 3.

I tried both cbv and cbn to escape the opacity of that lemma but no fish. Let me know how I can get that last evaluation to proceed.

Lef Ioannidis (May 25 2021 at 19:54):

I think I figured it out, using rewrite Eqdep.Eq_rect_eq.eq_rect_eq further reduces my last expression after cbn. Why is that not part of the cbn tactic by default? Is there some drawbacks to eliminating dependent equality when possible?

Li-yao (May 25 2021 at 20:36):

That's an axiom, equivalent to Uniqueness of Identity Proofs.

Li-yao (May 25 2021 at 20:40):

rewrite involves transforming terms using equality proofs, whereas cbn in some sense does not affect the term being generated.

Pierre-Marie Pédrot (May 25 2021 at 20:52):

You can get an axiom-free proof, though, since the equality you're rewriting on is between nats

Pierre-Marie Pédrot (May 25 2021 at 20:53):

An alternative would be to rewrite a variant of PeanoNat.Nat.sub_max_distr_r with Defined instead of Qed.

Pierre-Marie Pédrot (May 25 2021 at 20:54):

The reason why your term gets stuck during reduction is that this lemma is opaque, which blocks unfolding.

Pierre-Marie Pédrot (May 25 2021 at 20:55):

There are many ways to work around this issue, making everything Defined is an easy one.

Lef Ioannidis (May 26 2021 at 02:09):

I see thanks for the explanation @Li-yao . I originally went down the path that @Pierre-Marie Pédrot suggested, but this is not scalable as the lemma of PeanoNat.Nat.sub_max_distr_r has lemma dependencies. And as far as I understand, I cannot call Transparent PeanoNat.Nat.sub_max_distr_r to make it so, because it was already declared Opaque. I wonder if I could get for example the whole PeanoNat module and declare all lemmas with Defined and call it PeanoNatTransparent so PeanoNatTransparent.sub_max_distr_r would be transparent. What is the downside to having everything be transparent?

Pierre-Marie Pédrot (May 26 2021 at 07:34):

There are several reasons for which one may want Qed-terminated proofs. One of them is efficiency, since these lemmas are effectively treated as if they were atoms, so they never get unfolded (!) in particular during unification, and they are stored in a special way internally. Another reason is that it allows a strict separation between computable and non-computable parts, e.g. when you want to use extraction for programs written with Prop-parts, especially when you add excluded middle in Prop.

Pierre-Marie Pédrot (May 26 2021 at 07:35):

Regarding your problem, a reasonably easy way out is to wrap any opaque equality on nat inside a "computation-friendly" wrapper.

Pierre-Marie Pédrot (May 26 2021 at 07:37):

Since nat has decidable equality, say nat_eq_dec : forall (m n : nat), {m = n} + {m <> n} you can replace any equality p : m = n by a pattern-matching over the nat_eq_dec that uses the returned equality in the left case, and an absurd result with p in the right case.

Pierre-Marie Pédrot (May 26 2021 at 07:37):

This way, if nat_eq_dec is written in a fully transparent way, this will always compute.

Last updated: Sep 15 2024 at 13:02 UTC