open import Graded.Modality
open import Graded.Usage.Restrictions
open import Definition.Typed.EqualityRelation
open import Definition.Typed.Restrictions
open import Tools.Nullary
open import Tools.PropositionalEquality as PE
module Graded.Erasure.LogicalRelation.Fundamental.Counterexample
{a} {M : Set a}
(𝕄 : Modality M)
(open Modality 𝕄)
(TR : Type-restrictions M)
(UR : Usage-restrictions M)
(𝟘-well-behaved : Has-well-behaved-zero M semiring-with-meet)
{{eqrel : EqRelSet TR}}
where
open EqRelSet {{...}}
open Type-restrictions TR
open Usage-restrictions UR
open import Graded.Context 𝕄
open import Graded.Context.Properties 𝕄
open import Graded.Modality.Properties.Has-well-behaved-zero
semiring-with-meet 𝟘-well-behaved
open import Graded.Modality.Properties.PartialOrder
semiring-with-meet
open import Graded.Usage 𝕄 UR
open import Graded.Mode 𝕄
open import Definition.Untyped M hiding (_∷_)
open import Definition.Typed TR
open import Definition.Typed.Consequences.Canonicity TR
open import Definition.Typed.Consequences.Substitution TR
open import Definition.Typed.Properties TR
open import Definition.LogicalRelation TR
open import Definition.LogicalRelation.Substitution TR
open import Definition.LogicalRelation.Substitution.Properties TR
import Definition.LogicalRelation.Substitution.Irrelevance TR as IS
import Graded.Erasure.Target as T
import Graded.Erasure.LogicalRelation 𝕄 TR is-𝟘? as LR
import Graded.Erasure.LogicalRelation.Irrelevance 𝕄 TR is-𝟘? as LRI
import Graded.Erasure.LogicalRelation.Subsumption 𝕄 TR is-𝟘? as LRS
open import Tools.Fin
open import Tools.Function
open import Tools.Product
private variable
p : M
negation-of-fundamental-lemma-with-erased-matches :
Prodrec-allowed 𝟘 p 𝟘 →
Σᵣ-allowed p 𝟘 →
¬ (∀ {k} {Δ : Con Term k} (⊢Δ : ⊢ Δ) →
let open LR ⊢Δ in
(∀ {t} → Δ ⊢ t ∷ Empty → ⊥) →
∀ {n} {Γ : Con Term n} {t A : Term n} {γ : Conₘ n} {m} →
Γ ⊢ t ∷ A → γ ▸[ m ] t →
∃₂ λ ([Γ] : ⊩ᵛ Γ) ([A] : Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ]) →
γ ▸ Γ ⊩ʳ⟨ ¹ ⟩ t ∷[ m ] A / [Γ] / [A])
negation-of-fundamental-lemma-with-erased-matches
{p = p} P-ok Σᵣ-ok hyp =
case cEx of λ {
(_ , _ , _ , _ , _ , ⊢t , ▸t , not-ok) →
not-ok (hyp ⊢Δ consistent ⊢t ▸t) }
where
Δ : Con Term 1
Δ = ε ∙ (Σᵣ p , 𝟘 ▷ ℕ ▹ ℕ)
⊢Δ : ⊢ Δ
⊢Δ = ε ∙ ΠΣⱼ (ℕⱼ ε) (ℕⱼ (ε ∙ ℕⱼ ε)) Σᵣ-ok
consistent : ∀ {t} → Δ ⊢ t ∷ Empty → ⊥
consistent {t = t} ⊢t = ¬Empty ∷Empty
where
∷Empty : ε ⊢ t [ prodᵣ p zero zero ]₀ ∷ Empty
∷Empty =
substTerm ⊢t
(prodⱼ (ℕⱼ ε) (ℕⱼ (ε ∙ ℕⱼ ε)) (zeroⱼ ε) (zeroⱼ ε) Σᵣ-ok)
open LR ⊢Δ
open LRI ⊢Δ
open LRS ⊢Δ
cEx″ : ∀ {v} → prodrec 𝟘 p 𝟘 ℕ (var x0) zero ® v ∷ℕ → ⊥
cEx″ (zeroᵣ x x₁) with whnfRed*Term x (ne (prodrecₙ (var x0)))
... | ()
cEx″ (sucᵣ x x₁ t®v) with whnfRed*Term x (ne (prodrecₙ (var x0)))
... | ()
cEx′ :
([Δ] : ⊩ᵛ Δ)
([A] : Δ ⊩ᵛ⟨ ¹ ⟩ ℕ / [Δ]) →
ε ∙ 𝟘 ▸ Δ ⊩ʳ⟨ ¹ ⟩ prodrec 𝟘 p 𝟘 ℕ (var x0) zero
∷[ 𝟙ᵐ ] ℕ / [Δ] / [A] →
⊥
cEx′ [Δ] [A] ⊩ʳpr =
let [σ]′ = idSubstS [Δ]
⊢Δ′ = soundContext [Δ]
[σ] = IS.irrelevanceSubst [Δ] [Δ] ⊢Δ′ ⊢Δ [σ]′
σ®σ′ = erasedSubst {l = ¹} {σ′ = T.idSubst} [Δ] [σ]
pr®pr = ⊩ʳpr [σ] σ®σ′
[σA] = proj₁ (unwrap [A] ⊢Δ [σ])
[ℕ] = ℕᵣ {l = ¹} (idRed:*: (ℕⱼ ⊢Δ))
pr®pr′ = irrelevanceTerm [σA] [ℕ] (pr®pr ◀≢𝟘 𝟙≢𝟘)
in cEx″ pr®pr′
cEx : ∃ λ n
→ ∃₄ λ (t A : Term n) (Γ : Con Term n) (γ : Conₘ n)
→ Γ ⊢ t ∷ A
× γ ▸[ 𝟙ᵐ ] t
× ((∃₂ λ ([Γ] : ⊩ᵛ Γ) ([A] : Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ]) →
γ ▸ Γ ⊩ʳ⟨ ¹ ⟩ t ∷[ 𝟙ᵐ ] A / [Γ] / [A]) →
⊥)
cEx = _
, prodrec 𝟘 p 𝟘 ℕ (var x0) zero , ℕ , ε ∙ (Σᵣ p , 𝟘 ▷ ℕ ▹ ℕ)
, ε ∙ 𝟘
, prodrecⱼ Δ⊢ℕ Δℕ⊢ℕ ΔΣ⊢ℕ (var ⊢Δ here) (zeroⱼ ⊢Δℕℕ) Σᵣ-ok
, sub ▸pr
(≤ᶜ-reflexive
(≈ᶜ-refl ∙ PE.sym (PE.trans (+-identityʳ _) (·-zeroˡ _))))
, λ {([Γ] , [A] , ⊩ʳpr) → cEx′ [Γ] [A] ⊩ʳpr}
where
Δ⊢ℕ = ℕⱼ ⊢Δ
⊢Δℕ = ⊢Δ ∙ Δ⊢ℕ
Δℕ⊢ℕ = ℕⱼ ⊢Δℕ
Δ⊢Σ = ΠΣⱼ Δ⊢ℕ Δℕ⊢ℕ Σᵣ-ok
⊢ΔΣ = ⊢Δ ∙ Δ⊢Σ
ΔΣ⊢ℕ = ℕⱼ ⊢ΔΣ
⊢Δℕℕ = ⊢Δ ∙ Δ⊢ℕ ∙ Δℕ⊢ℕ
▸zero =
sub zeroₘ
(≤ᶜ-reflexive
(≈ᶜ-refl ∙
PE.trans (·-congˡ (·-zeroˡ p)) (·-zeroʳ 𝟙) ∙ ·-zeroʳ _))
▸ℕ = sub ℕₘ (≤ᶜ-refl ∙ ≤-reflexive (·-zeroʳ _))
▸pr = prodrecₘ {η = 𝟘ᶜ} var ▸zero ▸ℕ P-ok