open import Definition.Typed.Restrictions
open import Graded.Modality
module Graded.Erasure.LogicalRelation.Assumptions
{a} {M : Set a}
{π : Modality M}
(R : Type-restrictions π)
where
open Type-restrictions R
open import Definition.Typed R
open import Definition.Typed.EqualityRelation R
open import Definition.Typed.Consequences.Canonicity R
open import Definition.Typed.Inversion R
open import Definition.Typed.Properties R
open import Definition.Typed.Well-formed R
open import Definition.Untyped M
open import Definition.Untyped.Neutral M type-variant
open import Definition.Untyped.Properties M
open import Graded.Erasure.Target using (Strictness)
open import Tools.Fin
open import Tools.Function
open import Tools.Level
open import Tools.Nat
open import Tools.Product
open import Tools.Sum
private variable
n : Nat
Ξ : Con Term _
A B C t tβ tβ u v vβ vβ wβ wβ : Term _
p q qβ² r : M
record Is-reduction-relation
(Ξ : Con Term n) (_β_β·_ : Term n β Term n β Term n β Set a) :
Set (lsuc a) where
field
conv-β : t β u β· A β Ξ β’ A β‘ B β t β u β· B
β*ββ : Ξ β’ t β* u β· A β t β u β· A
βββ’β‘ : t β u β· A β Ξ β’ t β‘ u β· A
trans-β : t β u β· A β u β v β· A β t β v β· A
whnf-β : t β u β· A β Whnf u β t β v β· A β v β u β· A
app-β :
tβ β tβ β· Ξ p , q β· A βΉ B β
Ξ β’ u β· A β
tβ ββ¨ p β© u β tβ ββ¨ p β© u β· B [ u ]β
fst-β :
tβ β tβ β· Ξ£Λ’ p , q β· A βΉ B β
fst p tβ β fst p tβ β· A
snd-β :
tβ β tβ β· Ξ£Λ’ p , q β· A βΉ B β
snd p tβ β snd p tβ β· B [ fst p tβ ]β
prodrec-β :
Ξ β Ξ£Κ· p , qβ² β· A βΉ B β’ C β
tβ β tβ β· Ξ£Κ· p , qβ² β· A βΉ B β
Ξ β A β B β’ u β· C [ prodΚ· p (var x1) (var x0) ]βΒ² β
prodrec r p q C tβ u β prodrec r p q C tβ u β· C [ tβ ]β
natrec-β :
Ξ β’ t β· A [ zero ]β β
Ξ β β β A β’ u β· A [ suc (var x1) ]βΒ² β
vβ β vβ β· β β
natrec p q r A t u vβ β natrec p q r A t u vβ β· A [ vβ ]β
J-β :
Ξ β A β Id (wk1 A) (wk1 t) (var x0) β’ B β
Ξ β’ u β· B [ t , rfl ]ββ β
wβ β wβ β· Id A t v β
J p q A t B u v wβ β J p q A t B u v wβ β· B [ v , wβ ]ββ
K-β :
Ξ β Id A t t β’ B β
Ξ β’ u β· B [ rfl ]β β
vβ β vβ β· Id A t t β
K-allowed β
K p A t B u vβ β K p A t B u vβ β· B [ vβ ]β
opaque
wf-β : t β u β· A β Ξ β’ t β· A Γ Ξ β’ u β· A
wf-β = projβ ββ wf-β’β‘β· ββ βββ’β‘
opaque instance
β*-is-reduction-relation : Is-reduction-relation Ξ (Ξ β’_β*_β·_)
β*-is-reduction-relation = record
{ conv-β = conv*
; β*ββ = idαΆ
; βββ’β‘ = subset*Term
; trans-β = _β¨β·*_
; whnf-β = Ξ» tβ*u u-whnf β whrDetβTerm (tβ*u , u-whnf)
; app-β = app-subst*
; fst-β = fst-subst*
; snd-β = snd-subst*
; prodrec-β = prodrec-subst*
; natrec-β = natrec-subst*
; J-β = J-subst*
; K-β = K-subst*
}
opaque instance
β‘-is-reduction-relation : Is-reduction-relation Ξ (Ξ β’_β‘_β·_)
β‘-is-reduction-relation = record
{ conv-β = conv
; β*ββ = subset*Term
; βββ’β‘ = idαΆ
; trans-β = trans
; whnf-β = Ξ» tβ‘u _ tβ‘v β trans (symβ² tβ‘v) tβ‘u
; app-β = Ξ» tββ‘tβ β’u β app-cong tββ‘tβ (refl β’u)
; fst-β = fst-congβ²
; snd-β = snd-congβ²
; prodrec-β = Ξ» β’C tββ‘tβ β’u β
prodrec-congβ² (refl β’C) tββ‘tβ (refl β’u)
; natrec-β = Ξ» β’t β’u vββ‘vβ β
natrec-cong (refl (β’βββ’ (wfTerm β’u))) (refl β’t)
(refl β’u) vββ‘vβ
; J-β = Ξ» β’B β’u wββ‘wβ β
let β’A , β’t , β’v =
inversion-Id (wf-β’β‘β· wββ‘wβ .projβ)
in
J-congβ² (refl β’A) (refl β’t) (refl β’B) (refl β’u)
(refl β’v) wββ‘wβ
; K-β = Ξ» β’B β’u vββ‘vβ ok β
let β’A , β’t , _ =
inversion-Id (wf-β’β‘β· vββ‘vβ .projβ)
in
K-cong (refl β’A) (refl β’t) (refl β’B) (refl β’u) vββ‘vβ
ok
}
opaque
Id-is-reduction-relation :
Empty-con Ξ β Equality-reflection β
Is-reduction-relation Ξ (Ξ» t u A β β Ξ» v β Ξ β’ v β· Id A t u)
Id-is-reduction-relation {Ξ} ok = record
{ conv-β = Ξ» (_ , β’v) Aβ‘B β
let _ , β’t , β’u = inversion-Id (wf-β’β· β’v) in
_ , conv β’v (Id-cong Aβ‘B (refl β’t) (refl β’u))
; β*ββ = β’β‘ββ ββ subset*Term
; βββ’β‘ = βββ’β‘
; trans-β = Ξ» (_ , β’vβ) (_ , β’vβ) β _ , β’transitivity β’vβ β’vβ
; whnf-β = Ξ» (_ , β’vβ) _ (_ , β’vβ) β
_ , β’transitivity (β’symmetry β’vβ) β’vβ
; app-β = Ξ» tββtβ β’u β β’β‘ββ (R.app-β (βββ’β‘ tββtβ) β’u)
; fst-β = β’β‘ββ ββ R.fst-β ββ βββ’β‘
; snd-β = β’β‘ββ ββ R.snd-β ββ βββ’β‘
; prodrec-β = Ξ» β’C tββtβ β’u β β’β‘ββ (R.prodrec-β β’C (βββ’β‘ tββtβ) β’u)
; natrec-β = Ξ» β’A β’u vββvβ β β’β‘ββ (R.natrec-β β’A β’u (βββ’β‘ vββvβ))
; J-β = Ξ» β’B β’u wββwβ β β’β‘ββ (R.J-β β’B β’u (βββ’β‘ wββwβ))
; K-β = Ξ» β’B β’u vββvβ ok β β’β‘ββ (R.K-β β’B β’u (βββ’β‘ vββvβ) ok)
}
where
module R = Is-reduction-relation (β‘-is-reduction-relation {Ξ = Ξ})
βββ’β‘ : (β Ξ» v β Ξ β’ v β· Id A t u) β Ξ β’ t β‘ u β· A
βββ’β‘ (_ , β’v) = case ok of Ξ» where
(injβ Ξ΅) β
Ξ΅β’β·IdβΞ΅β’β‘β· β’v
(injβ ok) β
equality-reflectionβ² ok β’v
β’β‘ββ : Ξ β’ t β‘ u β· A β β Ξ» v β Ξ β’ v β· Id A t u
β’β‘ββ tβ‘u = rfl , rflβ±Όβ² tβ‘u
record Assumptions : Set (lsuc a) where
infix 4 _β_β·_
field
β¦ eqRelSet β¦ : EqRelSet
open EqRelSet eqRelSet public
field
{k} : Nat
{Ξ} : Con Term k
β’Ξ : β’ Ξ
β¦ inc β¦ : Neutrals-included or-empty Ξ
str : Strictness
_β_β·_ : Term k β Term k β Term k β Set a
is-reduction-relation : Is-reduction-relation Ξ _β_β·_
open Is-reduction-relation is-reduction-relation public
instance
no-equality-reflection-or-empty :
No-equality-reflection or-empty Ξ
no-equality-reflection-or-empty =
or-empty-map
(No-equality-reflectionβ .projβ ββ
flip Equality-reflection-allowedβΒ¬Neutrals-included)
inc