Suppose that I have a type A, and a dependent type P : A -> Type that I want to think of as a predicate; I'm interested in the "subset" \sum x : A, P(x) of A for which P holds.

In my case P(x) is a "mere proposition" in the HoTT sense, so theoretically, no functions \sum x : A, P(x) -> Z should depend on the proof of P(x).

My question is, in coq, how generally should I adapt later proofs to take advantage of this? In some sense I want to tell coq to "opaque" the inhabitant of P(x) and replace it with some formal element with no internal content, both to improve readability and computation time. What is the right language for this?

Example -

```
KK := f
(n - 1,,
natgthgehtrans (S n) n (n - 1) (natgthsnn n)
((fix F (n : nat) :
monfunstn (S n) m → (monfunstn n m → nat) → n ≥ n - 1 :=
match
n as n0
return
(monfunstn (S n0) m
→ (monfunstn n0 m → nat) → n0 ≥ n0 - 1)
with
| 0 =>
λ (_ : monfunstn 1 m) (_ : monfunstn 0 m → nat),
idpath true
| S n0 =>
λ (f : monfunstn (S (S n0)) m)
(IHn : monfunstn (S n0) m → nat), ....
```

Here I have a term KK:= f(x-1, *), where * is a very complex term belonging to a type P(x-1) which is a proposition. It goes on and on, I want coq to hide this information because it's irrelevant. (And ideally it should not do any kind of unfolding or computation within that term, either.)

You can "Qed" part of a term, with either the `abstract`

tactic or `Program Definition KK x := f (x - 1, _). Next Obligation. ... Qed.`

Last updated: Jun 24 2024 at 12:02 UTC