We use the variables a,b,c,f,g,h for closed terms.
We write (a → b) for the transitive closure of ↦.
We write (a ↔ b) for the equivalence closure of ↦.
(What about η laws? Do we want to validate those?)
We define the following type-indexed sets:
[A]≤ ⊆ Term × Term [A]= ⊆ Term × Term [A] ⊆ Term
As an abuse of notation, we write
A(a ≤ b) for (a,b) ∈ [A]≤ A(a = b) for (a,b) ∈ [A]= A(a) for a ∈ [A]
We first define [A]= and [A] in terms of [A]≤:
A(a = b) iff A(a ≤ b) ∧ A(b ≤ a) A(a) iff ∃ b. A(a ≤ b)
We define [A]≤ by induction on A:
1(a ≤ b) = a → () ∧ b → () 2(a ≤ b) = a → v₁ ∧ b → v₂ ∧ v₁ ≤ v₂ (for v₁,v₂ ∈ {false,true})
A × B (a ≤ b) = a → (a₁, a₂) ∧ b → (b₁, b₂) ∧ A(a₁ ≤ b₁) ∧ B(a₂ ≤ b₂) A₁ + A₂ (a ≤ b) = a → inᵢ a’ ∧ b → inᵢ b’ ∧ Aᵢ(a’ ≤ b’)
A →⁺ B (f ≤ g) = f → λx.b₁ ∧ g → λx.b₂ ∧ ∀(a₁,a₂ st. A(a₁ ≤ a₂)) B([a₁/x]b₁ ≤ [a₂/x]b₁) ∧ B([a₁/x]b₂ ≤ [a₂/x]b₂) ∧ B([a₁/x]b₁ ≤ [a₁/x]b₂) ∧ B([a₂/x]b₁ ≤ [a₂/x]b₂) NB. this is just a commuting square!
more concisely, B(f a₁ ≤ f a₂); B(g a₁ ≤ g a₂); B(f aᵢ ≤ g aᵢ)
A → B (f ≤ g) = f → λx.b₁ ∧ g → λx.b₂ ∧ ∀(a₁,a₂ st. A(a₁ = a₂)) (repeat the commuting square above)
{A} (a ≤ b) = a → {aᵢ …} ∧ b → {bᵢ …} ∧ ∀(aᵢ) ∃(bⱼ) A(aᵢ = bⱼ)
To show: If A(a ≤ b) then A(a ≤ a). By induction on A.
Case 1(a ≤ b): Trivial. Case 2(a ≤ b): By reflexivity of ≤ on booleans.
Case A × B(a ≤ b): We have a → (a₁, a₂), b → (b₁, b₂), A(a₁ ≤ b₁) and B(a₂ ≤ b₂) by IH we have A(a₁ ≤ a₁) and B(a₂ ≤ a₂) thus A × B (a ≤ a)
Case A₁ + A₂(a ≤ b): We have a → inᵢ a’ and b → inᵢ b’ and Aᵢ(a’ ≤ b’). By IH applied to Aᵢ(a’ ≤ b’), we have Aᵢ(a’ ≤ a’).
Case A →⁺ B (f ≤ g): We have f → λx.b₁, so that’s ok. Consider any a₁, a₂ st. A(a₁ ≤ a₂). We need to show: B(f a₁ ≤ f a₂) and B(f a₁ ≤ f a₁) and B(f a₂ ≤ f a₂) B(f a₁ ≤ f a₂) is direct from A →⁺ B (f ≤ g) B(f a₁ ≤ f a₁) is by applying our IH to B(f a₁ ≤ g a₁) from A →⁺ B (f ≤ g) B(f a₂ ≤ f a₂) is by applying our IH to B(f a₂ ≤ g a₂) from A →⁺ B (f ≤ g)
Case A → B (f ≤ g): We have f → λx.b₁, so that’s ok. Consider any a₁, a₂ st. A(a₁ = a₂). We need to show: B(f a₁ ≤ f a₂) and B(f a₁ ≤ f a₁) B(f a₁ ≤ f a₂) is direct from A → B (f ≤ g) B(f a₁ ≤ f a₁) is by applying our IH to B(f a₁ ≤ f a₂)
Case {A} (a ≤ b): We have a → {aᵢ …} and b → {bᵢ …} and ∀(aᵢ) ∃(bⱼ) A(aᵢ = bⱼ) To show: ∀(aᵢ) ∃(aⱼ) A(aᵢ = aⱼ) Let j = i! Since A(aᵢ = bⱼ), we have A(aᵢ ≤ bⱼ), so by our IH we have A(aᵢ ≤ aᵢ). Thus A(aᵢ = aᵢ). Done!
To show: If A(a ≤ b) and A(b ≤ c) then A(a ≤ c). By induction on A.
Case 1(a ≤ b ≤ c): Trivial. Case 2(a ≤ b ≤ c): Trivial by transitivity of ≤ on booleans.
Case A × B(a ≤ b ≤ c): We have a → (a₁, a₂); b → (b₁, b₂); c → (c₁, c₂). A(a₁ ≤ b₁ ≤ c₁) so by IH A(a₁ ≤ c₁) B(a₂ ≤ b₂ ≤ c₂) so by IH A(a₂ ≤ c₂) Done.
Case A + B(a ≤ b ≤ c): omitted
Case A →⁺ B(f ≤ g ≤ h): Consider any a₁, a₂ st. A(a₁ ≤ a₂) To show: B(f a₁ ≤ f a₂); B(h a₁ ≤ h a₂); B(f aᵢ ≤ h aᵢ) By assumption, B(f a₁ ≤ f a₂) and B(h a₁ ≤ h a₂). By assumption, B(f aᵢ ≤ g aᵢ ≤ h aᵢ); so by IH B(f aᵢ ≤ h aᵢ). Done.
Case A → B(f ≤ g ≤ h): Consider any a₁, a₂ st A(a₁ = a₂) To show: B(f a₁ ≤ f a₂); B(h a₁ ≤ h a₂); B(f aᵢ ≤ h aᵢ) By assumption, B(f a₁ ≤ f a₂) and B(h a₁ ≤ h a₂). By assumption, B(f aᵢ ≤ g aᵢ ≤ h aᵢ); so by IH B(f aᵢ ≤ h aᵢ). Done.
Case {A}(a ≤ b ≤ c): We have a → {aᵢ …} and b → {bᵢ …} and c → {cᵢ …} To show: ∀(aᵢ) ∃(cₖ) A(aᵢ = cₖ) Consider any aᵢ. Then ∃(bⱼ) A(aᵢ = bⱼ). Then ∃(cₖ) A(bⱼ = cₖ). By transitivity of [A]= (which follows from IH), we have A(aᵢ = cₖ).
To show [A]= is a PER, we need that it is symmetric and transitive. The symmetry of [A]= follows immediately from its definition. The transitivity of [A]= follows immediately from transitivity of [A]≤.
(What about η laws? ↔ doesn’t cover them! Do we want to validate those?)
Suffices to show that if A(a) and a → b then A(a = b). We prove this by induction on A:
Case 1: Since a → b and a → ()… I think I need confluence here. Hm. If a ↦ b is a reduction partial function, we’re good.
Case 2: Confluence again.
Case A × B:
By induction on A, noting that in each case the definition of A(a ≤ b) requires `a’ can reduce to WHNF.
Thm: If Γ ⊢ e : A and Γ(γ₁ ≤ γ₂) then A([γ₁]e ≤ [γ₂]e). By induction on Γ ⊢ e : A.
Γ,x:A ⊢ e : B
Γ ⊢ λx.e : A →⁺ B
TS: For any A(a₁ ≤ a₂): [γ₁,a₁/x]e ≤ [γ₁,a₂/x]e ≤ ≤ [γ₂,a₁/x]e ≤ [γ₂,a₂/x]e
Consider any A(a₁ ≤ a₂). By partial reflexivity Γ(γᵢ ≤ γᵢ). So Γ,x:A(γᵢ,a₁/x ≤ γᵢ,a₂/x). So by IH [γᵢ,a₁/x]e ≤ [γᵢ,a₂/x]e.
By partial reflexivity A(aᵢ ≤ aᵢ). So Γ,x:A(γ₁,aᵢ/x ≤ γ₂,aᵢ/x). So by IH [γ₁,aᵢ/x]e ≤ [γ₂,aᵢ/x]e. Done.
Γ,x::A ⊢ e : B
Γ ⊢ λx.e : A → B
TODO, expected to be similar to A →⁺ B.
Γ ⊢ e₁ : A →⁺ B Γ ⊢ e₂ : A
Γ ⊢ e₁ e₂ : B
WTS: If Γ(γ₁ ≤ γ₂) then B([γ₁](e₁ e₂) ≤ [γ₂](e₁ e₂)).
Let f = [γ₁]e₁ and g = [γ₂]e₁. Let a = [γ₁]e₂ and b = [γ₂]e₂. By IH, A →⁺ B(f ≤ g). By IH, A(a ≤ b). Thus we have f a ≤ g a ≤ ≤ f b ≤ g b
Note that f a = [γ₁]e₁ [γ₁]e₂ = [γ₁](e₁ e₂). Note that g b = [γ₂]e₁ [γ₂]e₂ = [γ₂](e₁ e₂).
By transitivity, B(f a ≤ g b). Done.
By induction on L (this is kind of funky):
Case 2. ε → false. Thus 2(ε ≤ ε). Case {A}. ε → {}. Thus {A}(ε ≤ ε). Case L × M. ε → (ε, ε). By IH L(ε ≤ ε) and M(ε ≤ ε). Done. Case A →⁺ L. ε → λx.ε. The commuting square becomes trivial. By IH L(ε ≤ ε). Done. Case A → L. ε → λx.ε. The commuting square becomes trivial. By IH L(ε ≤ ε). Done.
Γ ⊢ eᵢ : L
Γ ⊢ e₁ ∨ e₂ : L
Case 2. By IH γⱼ[eᵢ] → vᵢⱼ for vᵢⱼ ∈ {true,false}. Hm, this is complicated.