walker (Jan 22 2023 at 11:19): 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:
bool_decide (Closed t) = true would be once you prove Closed is decidable)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.
thanks a lot @Gaëtan Gilbert for the proof !
Last updated: Oct 13 2024 at 01:02 UTC