Stream: Coq users

Topic: Using opaque and related

Patrick Nicodemus (Nov 20 2021 at 03:40):

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?

Patrick Nicodemus (Nov 20 2021 at 03:43):

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.)

Paolo Giarrusso (Nov 20 2021 at 07:42):

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: Oct 03 2023 at 19:01 UTC