## 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 (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.
match a with
| 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 (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 26 2023 at 12:02 UTC