Stream: Coq users

Topic: How to deal with proof irrelevance


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 22 2023 at 12:02):

options include:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip walker (Jan 22 2023 at 12:11):

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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jan 22 2023 at 12:12):

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

view this post on Zulip 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.

view this post on Zulip walker (Jan 22 2023 at 12:13):

I wasn't sure which one you meant.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jan 22 2023 at 12:16):

you just apply funext to Eqdep_dec.eq_proofs_unicity

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jan 22 2023 at 12:18):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip walker (Jan 22 2023 at 12:20):

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


Last updated: Jun 13 2024 at 07:01 UTC