Zulip Chat Archive

Stream: general

Topic: context irrelevance of defeq

Reid Barton (Feb 28 2020 at 15:31):

Does Lean have the following metatheoretic property:
If Γa:A\Gamma \vdash a : A and Γb:A\Gamma \vdash b : A and Γ,Δab\Gamma, \Delta \vdash a \equiv b (defeq), then Γab\Gamma \vdash a \equiv b.
Also, is there an established name for this property?

Mario Carneiro (Feb 28 2020 at 21:32):

I'm pretty sure the answer is yes, but I don't think if explicitly shows up in the thesis

Mario Carneiro (Feb 28 2020 at 21:32):

If Δ\Delta is inhabited, you can prove it by substitution

Mario Carneiro (Feb 28 2020 at 22:32):

It's also equivalent to the following statement about typing: If Γ,Δe:A\Gamma,\Delta\vdash e:A and FV(e)ΓFV(e)\subseteq\Gamma, then Γe:A\Gamma\vdash e:A

Reid Barton (Feb 29 2020 at 01:04):

(do you also need FV(A)ΓFV(A) \subseteq \Gamma or does it follow?)

Mario Carneiro (Feb 29 2020 at 03:04):

Another good question in the same area. Obviously the "natural type" of ee does not have any free variables not in ee itself, but it is possible for defeq terms to have different sets of free variables because of proof irrelevance.

For example, consider the proofs A:Urefl  A:A=AA:U\vdash refl\;A: A = A and A:U,h:rec  (A=A)  h:A=AA:U,h:\bot\vdash rec_{\bot}\; (A=A)\; h:A=A. By proof irrelevance, these two are defeq in the context A:U,h:A:U,h:\bot. So you could have A:U,x:A,h:x:cast(rec  (A=A)  h)AA:U,x:A,h:\bot\vdash x: cast (rec_{\bot}\; (A=A)\; h) A (where the cast is defeq to AA).

Reid Barton (Feb 29 2020 at 14:30):

Now that you say that, isn't a more down to earth version something like A:U,x:A,B:Ux:constA(B)A : U, x : A, B : U \vdash x : \mathrm{const}_A(B), where constA(t)=A\mathrm{const_A}(t) = A for all tt

Last updated: Aug 03 2023 at 10:10 UTC