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_Def depend on the specific proof of
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.
bool_decide (Closed t) = truewould be once you prove
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.
= 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
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
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: Oct 04 2023 at 20:01 UTC