## Stream: Coq users

### Topic: How to deal with proof irrelevance

#### walker (Jan 22 2023 at 11:19):

So I was experimenting with coq and I eneded up with something that looks like that:

``````Definition Closed t : Prop := forall σ, t.[σ] = t.

Inductive ModuleItem : Type :=
| Module_Decl (name: string) (T: Term): Closed T -> ModuleItem
| Module_Def (name: string) (t: Term): Closed t -> ModuleItem.

Inductive Module : Type :=
| module (name: string) (content: seq ModuleItem).
``````

The problem is that both `Module_Decl` and `Module_Def` depend on the specific proof of `closed T`

Very soon during proofs, I encountered the following:

``````Hclosed: Closed T
Hgget: gget Σ name = Some (Module_Decl name T Hclosed)
=========================================================== Goal
forall Hyp0 : Closed T,
gget Σ name = Some (Module_Def name T Hyp0)
``````

Which kind of made me understand what people meant when they say proof irrelevance, but now I don't know how to restructure things to avoid this kind of problems.

Note: I tried also `Definition Closed t : SProp := forall σ, t.[σ] = t.` But it failed saying that Prop is not subtype of `SProp` so apparently this is now how SProp works.

#### Paolo Giarrusso (Jan 22 2023 at 12:02):

options include:

• the proof irrelevance axiom (if sound for you)
• switching to a proposition that is _provably_ proof irrelevant (equalities of decidable types are, so `bool_decide (Closed t) = true` would be once you prove `Closed` is decidable)
• move validity outside of terms and into typing derivations (if those are separate)
• maybe `SProp`, but it's experimental and I'm no expert... (BTW, your failed attempt doesn't mention `SProp` — guess you tried `Definition Closed t : SProp`)

#### walker (Jan 22 2023 at 12:07):

point 4, this is exactly what I tried, fixed the typo

regard point 1: May I ask when proof irrelevance axiom would be not sound I am assuming functional extensionality in coq, and the language I am developing also will at some point have functional extensionality as a lemma.

#### Gaëtan Gilbert (Jan 22 2023 at 12:08):

if you have funext and equality on Term is decidable then you can prove irrelevance of Closed without further axioms

#### walker (Jan 22 2023 at 12:11):

Equality on terms (by beta reductions) is not actually decidable in coq.

#### walker (Jan 22 2023 at 12:11):

Also just to make sure I am not causing my futute self problems, Term will eventually have sufficient constructs to build basic cubical type theory, so I am not sure if that will cause problems with proof irrelevance axiom.

#### Gaëtan Gilbert (Jan 22 2023 at 12:12):

the `=` you use in the definition of Closed is not up to beta is it?

#### walker (Jan 22 2023 at 12:12):

oh no it is not! It is just coq equality, this kind of equality is decidable in coq for `Term`.

#### walker (Jan 22 2023 at 12:13):

I wasn't sure which one you meant.

#### walker (Jan 22 2023 at 12:13):

I will try to prove proof irrelevance for that, but if there is a layout of the proof somewhere, please let me about it.

#### Gaëtan Gilbert (Jan 22 2023 at 12:16):

you just apply funext to `Eqdep_dec.eq_proofs_unicity`

#### Pierre-Marie Pédrot (Jan 22 2023 at 12:17):

You should maybe characterize closedness in a decidable way and prove that it is equivalent to the quantified variant.

#### Pierre-Marie Pédrot (Jan 22 2023 at 12:18):

This would require less axioms and would be easier to work with.

#### walker (Jan 22 2023 at 12:19):

right I thought about doing that but I was lazy and this definition was the one I really needed to use, but I might characterize it as a boolean function.

#### Gaëtan Gilbert (Jan 22 2023 at 12:20):

``````Require Import Eqdep_dec.

Context (Term:Type) (Substitution:Type) (substitute : Term -> Substitution -> Term)
(Termdec : forall x y : Term, x = y \/ x <> y)
(Funext : forall A B f g, (forall x, f x = g x) -> f = g :> forall x:A, B x).

Definition Closed n := forall sigma, substitute n sigma = n.

Lemma Closed_irr : forall n (p1 p2 : Closed n), p1 = p2.
Proof.
intros.
apply Funext.
intros sigma.
apply eq_proofs_unicity.
exact Termdec.
Qed.
``````

#### walker (Jan 22 2023 at 12:20):

thanks a lot @Gaëtan Gilbert for the proof !

Last updated: Oct 04 2023 at 20:01 UTC