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.

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`

)

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.

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

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

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.

the `=`

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

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

.

I wasn't sure which one you meant.

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

you just apply funext to `Eqdep_dec.eq_proofs_unicity`

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

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

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.

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

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

Last updated: Jun 13 2024 at 07:01 UTC