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?

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.

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?

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

`rewrite`

involves transforming terms using equality proofs, whereas `cbn`

in some sense does not affect the term being generated.

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

An alternative would be to rewrite a variant of `PeanoNat.Nat.sub_max_distr_r`

with `Defined`

instead of `Qed`

.

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

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

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?

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.

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

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.

This way, if `nat_eq_dec`

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

Last updated: Jan 29 2023 at 01:02 UTC