open import Definition.Typed.Restrictions
module Graded.Erasure.SucRed
{a} {M : Set a}
(R : Type-restrictions M)
where
open import Tools.Empty
open import Tools.Function
open import Tools.Nat
open import Tools.Nullary
open import Tools.Product
import Tools.PropositionalEquality as PE
open import Tools.Unit
open import Definition.Untyped M hiding (_∷_)
open import Definition.Typed R
open import Definition.Typed.Consequences.Consistency R
open import Definition.Typed.Properties R
import Graded.Erasure.Target as T
private
variable
n : Nat
Γ : Con Term n
t t′ u : Term n
v v′ w w′ : T.Term n
data _⊢_⇒ˢ_∷ℕ (Γ : Con Term n) : (t u : Term n) → Set a where
whred : Γ ⊢ t ⇒ u ∷ ℕ → Γ ⊢ t ⇒ˢ u ∷ℕ
sucred : Γ ⊢ t ⇒ˢ u ∷ℕ → Γ ⊢ suc t ⇒ˢ suc u ∷ℕ
data _⊢_⇒ˢ*_∷ℕ (Γ : Con Term n) : (t u : Term n) → Set a where
id : Γ ⊢ t ∷ ℕ → Γ ⊢ t ⇒ˢ* t ∷ℕ
_⇨ˢ_ : Γ ⊢ t ⇒ˢ t′ ∷ℕ → Γ ⊢ t′ ⇒ˢ* u ∷ℕ → Γ ⊢ t ⇒ˢ* u ∷ℕ
⇒ˢ*∷ℕ-trans : Γ ⊢ t ⇒ˢ* t′ ∷ℕ → Γ ⊢ t′ ⇒ˢ* u ∷ℕ → Γ ⊢ t ⇒ˢ* u ∷ℕ
⇒ˢ*∷ℕ-trans (id x) d′ = d′
⇒ˢ*∷ℕ-trans (x ⇨ˢ d) d′ = x ⇨ˢ ⇒ˢ*∷ℕ-trans d d′
whred* : Γ ⊢ t ⇒* u ∷ ℕ → Γ ⊢ t ⇒ˢ* u ∷ℕ
whred* (id x) = id x
whred* (x ⇨ d) = whred x ⇨ˢ whred* d
sucred* : Γ ⊢ t ⇒ˢ* u ∷ℕ → Γ ⊢ suc t ⇒ˢ* suc u ∷ℕ
sucred* (id x) = id (sucⱼ x)
sucred* (x ⇨ˢ d) = (sucred x) ⇨ˢ (sucred* d)
subsetTermˢ : Γ ⊢ t ⇒ˢ u ∷ℕ → Γ ⊢ t ≡ u ∷ ℕ
subsetTermˢ (whred x) = subsetTerm x
subsetTermˢ (sucred d) = suc-cong (subsetTermˢ d)
subset*Termˢ : Γ ⊢ t ⇒ˢ* u ∷ℕ → Γ ⊢ t ≡ u ∷ ℕ
subset*Termˢ (id x) = refl x
subset*Termˢ (x ⇨ˢ d) = trans (subsetTermˢ x) (subset*Termˢ d)
⇒ˢ∷ℕ≡zero→⇒ : Γ ⊢ t ⇒ˢ u ∷ℕ → Γ ⊢ u ≡ zero ∷ ℕ → Γ ⊢ t ⇒ u ∷ ℕ
⇒ˢ∷ℕ≡zero→⇒ (whred t⇒u) _ = t⇒u
⇒ˢ∷ℕ≡zero→⇒ (sucred _) suc≡zero = ⊥-elim (zero≢suc (sym suc≡zero))
⇒ˢ*∷ℕ≡zero→⇒* : Γ ⊢ t ⇒ˢ* u ∷ℕ → Γ ⊢ u ≡ zero ∷ ℕ → Γ ⊢ t ⇒* u ∷ ℕ
⇒ˢ*∷ℕ≡zero→⇒* (id ⊢t) _ = id ⊢t
⇒ˢ*∷ℕ≡zero→⇒* (t⇒v ⇨ˢ v⇒*u) u≡0 =
⇒ˢ∷ℕ≡zero→⇒ t⇒v (trans (subset*Termˢ v⇒*u) u≡0) ⇨
⇒ˢ*∷ℕ≡zero→⇒* v⇒*u u≡0
⇒ˢzero∷ℕ→⇒zero : Γ ⊢ t ⇒ˢ zero ∷ℕ → Γ ⊢ t ⇒ zero ∷ ℕ
⇒ˢzero∷ℕ→⇒zero t⇒ =
⇒ˢ∷ℕ≡zero→⇒ t⇒ (refl (zeroⱼ (wfEqTerm (subsetTermˢ t⇒))))
⇒ˢ*zero∷ℕ→⇒*zero : Γ ⊢ t ⇒ˢ* zero ∷ℕ → Γ ⊢ t ⇒* zero ∷ ℕ
⇒ˢ*zero∷ℕ→⇒*zero t⇒ =
⇒ˢ*∷ℕ≡zero→⇒* t⇒ (refl (zeroⱼ (wfEqTerm (subset*Termˢ t⇒))))
data _⇒ˢ_ : (v w : T.Term n) → Set where
whred : v T.⇒ w → v ⇒ˢ w
sucred : v ⇒ˢ w → T.suc v ⇒ˢ T.suc w
data _⇒ˢ*_ : (v w : T.Term n) → Set where
refl : v ⇒ˢ* v
trans : v ⇒ˢ v′ → v′ ⇒ˢ* w → v ⇒ˢ* w
⇒ˢ*-trans : v ⇒ˢ* v′ → v′ ⇒ˢ* w → v ⇒ˢ* w
⇒ˢ*-trans refl d′ = d′
⇒ˢ*-trans (trans d d₁) d′ = trans d (⇒ˢ*-trans d₁ d′)
whred*′ : v T.⇒* w → v ⇒ˢ* w
whred*′ T.refl = refl
whred*′ (T.trans x d) = trans (whred x) (whred*′ d)
sucred*′ : v ⇒ˢ* w → T.suc v ⇒ˢ* T.suc w
sucred*′ refl = refl
sucred*′ (trans x d) = trans (sucred x) (sucred*′ d)
Is-suc : T.Term n → Set
Is-suc = λ where
(T.suc _) → ⊤
_ → ⊥
data Suc-view : T.Term n → Set where
is-suc : Suc-view (T.suc v)
not-is-suc : ¬ Is-suc v → Suc-view v
suc-view : (v : T.Term n) → Suc-view v
suc-view = λ where
(T.suc _) → is-suc
(T.var _) → not-is-suc (λ ())
(T.lam _) → not-is-suc (λ ())
(_ T.∘ _) → not-is-suc (λ ())
(T.prod _ _) → not-is-suc (λ ())
(T.fst _) → not-is-suc (λ ())
(T.snd _) → not-is-suc (λ ())
(T.prodrec _ _) → not-is-suc (λ ())
T.zero → not-is-suc (λ ())
(T.natrec _ _ _) → not-is-suc (λ ())
T.star → not-is-suc (λ ())
T.↯ → not-is-suc (λ ())
suc⇒*suc : v T.⇒* w → Is-suc v → Is-suc w
suc⇒*suc T.refl is-suc-v = is-suc-v
suc⇒*suc {v = v} (T.trans v⇒ _) is-suc-v =
case suc-view v of λ where
is-suc → case v⇒ of λ ()
(not-is-suc not-is-suc-v) → ⊥-elim (not-is-suc-v is-suc-v)
⇒ˢ≢suc→⇒ : v ⇒ˢ w → ¬ Is-suc w → v T.⇒ w
⇒ˢ≢suc→⇒ (whred v⇒w) _ = v⇒w
⇒ˢ≢suc→⇒ (sucred _) not-suc = ⊥-elim (not-suc _)
⇒ˢ*≢suc→⇒* : v ⇒ˢ* w → ¬ Is-suc w → v T.⇒* w
⇒ˢ*≢suc→⇒* refl _ = T.refl
⇒ˢ*≢suc→⇒* (trans v⇒v′ v′⇒*w) not-suc =
T.trans (⇒ˢ≢suc→⇒ v⇒v′ (not-suc ∘→ suc⇒*suc v′⇒*w′)) v′⇒*w′
where
v′⇒*w′ = ⇒ˢ*≢suc→⇒* v′⇒*w not-suc
⇒ˢzero→⇒zero : v ⇒ˢ T.zero → v T.⇒ T.zero
⇒ˢzero→⇒zero = flip ⇒ˢ≢suc→⇒ (λ ())
⇒ˢ*zero→⇒*zero : v ⇒ˢ* T.zero → v T.⇒* T.zero
⇒ˢ*zero→⇒*zero = flip ⇒ˢ*≢suc→⇒* (λ ())
⇒ˢsuc→⇒*suc : v ⇒ˢ T.suc w → ∃ λ w → v T.⇒* T.suc w
⇒ˢsuc→⇒*suc (whred v⇒) = _ , T.trans v⇒ T.refl
⇒ˢsuc→⇒*suc (sucred v⇒) = _ , T.refl
⇒ˢ*suc→⇒*suc : v ⇒ˢ* T.suc w → ∃ λ w → v T.⇒* T.suc w
⇒ˢ*suc→⇒*suc = λ where
refl →
_ , T.refl
(trans {v′ = v′} v⇒v′ v′⇒*suc) → case suc-view v′ of λ where
is-suc → ⇒ˢsuc→⇒*suc v⇒v′
(not-is-suc not-suc) →
case ⇒ˢ*suc→⇒*suc v′⇒*suc of λ {
(_ , v′⇒*suc) →
_ , T.trans (⇒ˢ≢suc→⇒ v⇒v′ not-suc) v′⇒*suc }