{-# OPTIONS --allow-unsolved-metas -vtactic:10 #-}
open import 1Lab.Reflection.HLevel
open import 1Lab.Reflection.Subst
open import 1Lab.Reflection
open import 1Lab.Path
open import 1Lab.Type
module 1Lab.Reflection.Regularity where
private
double-comp
: ∀ {ℓ} {A : Type ℓ} {w z : A} (x y : A)
→ w ≡ x → x ≡ y → y ≡ z
→ w ≡ z
double-comp x y p q r i = primHComp
(λ { j (i = i0) → p (~ j) ; j (i = i1) → r j }) (q i)
data Regularity-precision : Type where
precise fast : Regularity-precision
refl-transport : Nat → Term → TC Term
go : Regularity-precision → Nat → Term → TC Term
go* : Regularity-precision → Nat → List (Arg Term) → TC (List (Arg Term))
refl-transport n tm@(def (quote transp) (ℓ h∷ Al v∷ φ v∷ x v∷ [])) =
(do
debugPrint "tactic.regularity" 10 $ "Checking regularity of " ∷ termErr tm ∷ []
let φ' = def (quote _∨_) (φ v∷ var n [] v∷ [])
let tm' = def (quote transp) (ℓ h∷ Al v∷ φ' v∷ x v∷ [])
check-type tm' unknown
pure tm') <|>
(do
debugPrint "tactic.regularity" 10 $ "NOT a (transport refl): " ∷ termErr tm ∷ []
pure tm)
refl-transport _ tm = pure tm
go pre n (var x args) = var x <$> go* pre n args
go pre n (con c args) = con c <$> go* pre n args
go fast n (def (quote transp) (ℓ h∷ Al v∷ φ v∷ x v∷ [])) = do
x ← go fast n x
let φ' = def (quote _∨_) (φ v∷ var n [] v∷ [])
pure $ def (quote transp) (ℓ h∷ Al v∷ φ' v∷ x v∷ [])
go pre n (def f args) = do
as ← go* pre n args
refl-transport n (def f as)
go pre k t@(lam v (abs nm b)) = lam v ∘ abs nm <$> under-abs t (go pre (suc k) b)
go pre n (pat-lam cs args) = typeError $ "regularity: Can not deal with pattern lambdas"
go pre n t@(pi (arg i a) (abs nm b)) = do
a ← go pre n a
b ← under-abs t (go pre (suc n) b)
pure (pi (arg i a) (abs nm b))
go pre n (agda-sort s) = pure (agda-sort s)
go pre n (lit l) = pure (lit l)
go pre n (meta x args) = meta x <$> go* pre n args
go pre n unknown = pure unknown
go* pre n [] = pure []
go* pre n (arg i a ∷ as) = do
a ← go pre n a
(arg i a ∷_) <$> go* pre n as
to-regularity-path : Regularity-precision → Term → TC Term
to-regularity-path pre tm = do
let tm = raise 1 tm
tm ← run-speculative $ extend-context "i" (argN (quoteTerm I)) do
tm ← go pre 0 tm
pure (tm , false)
pure $ vlam "i" tm
regular!-worker :
∀ {ℓ} {A : Type ℓ} {x y : A}
→ Regularity-precision
→ x ≡ y
→ Term
→ TC ⊤
regular!-worker {x = x} {y} pre p goal = do
gt ← infer-type goal
`x ← quoteTC x
`y ← quoteTC y
`p ← quoteTC p
just (_ , l , r) ← unapply-path =<< wait-for-type =<< infer-type goal
where _ → typeError [ "goal type is not path type: " , termErr goal ]
l ← normalise =<< wait-for-type l
r ← normalise =<< wait-for-type r
reg ← to-regularity-path pre l
reg' ← to-regularity-path pre r
unify-loudly goal $ def (quote double-comp) $
`x v∷ `y v∷ reg
v∷ `p
v∷ def (quote sym) (reg' v∷ [])
v∷ []
module Regularity where
open Regularity-precision public
macro
reduce! : Term → TC ⊤
reduce! goal = do
just (_ , l , r) ← unapply-path =<< infer-type goal
where _ → typeError []
reg ← to-regularity-path precise =<< (wait-for-type =<< normalise l)
unify-loudly goal reg
precise! : ∀ {ℓ} {A : Type ℓ} {x y : A} → x ≡ y → Term → TC ⊤
fast! : ∀ {ℓ} {A : Type ℓ} {x y : A} → x ≡ y → Term → TC ⊤
precise! p goal = regular!-worker precise p goal
fast! p goal = regular!-worker fast p goal
reduct : Regularity-precision → Term → Term → TC ⊤
reduct pres tm _ = do
orig ← wait-for-type =<< normalise tm
tm ← to-regularity-path pres orig
red ← normalise (apply-tm tm (argN (con (quote i1) [])))
`pres ← quoteTC pres
typeError $
"The term\n\n " ∷ termErr orig ∷ "\n\nreduces modulo " ∷ termErr `pres ∷ " regularity to\n\n "
∷ termErr red
∷ "\n"
module
_ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f g : A → B) (x : A)
(a-loop : (i : I) → Type ℓ [ (i ∨ ~ i) ↦ (λ ._ → A) ])
where private
p : (h : ∀ x → f x ≡ g x)
→ transport (λ i → A → B)
(λ x → transport refl (transport refl (f (transport refl x)))) ≡ g
p h = Regularity.reduce! ∙ funext h
q : transport refl (transp (λ i → outS (a-loop i)) i0 x) ≡ transp (λ i → outS (a-loop i)) i0 x
q = Regularity.reduce!
q' : ⊤
q' = {! Regularity.reduct Regularity.fast (transp (λ i → outS (a-loop i)) i0 x) !}
r : (h : ∀ x → f x ≡ g x) → transport refl (f x) ≡ transport refl (g x)
r h = Regularity.precise! (h x)
s : (h : ∀ x → f x ≡ g x) → transport refl (g x) ≡ transport refl (f x)
s h = sym $ Regularity.fast! (h x)