diff --git a/CHANGELOG.md b/CHANGELOG.md index fa15c770de..f7d4a6f3b9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -49,6 +49,10 @@ Other major additions Reflection.TypeChecking.Monad.Instances ``` +* Function application in reflected terms (`Reflection.Apply`) + +* Congruence helper macros in `Tactic.Cong` + Other major changes ------------------- @@ -89,4 +93,9 @@ Other minor additions ```agda nothing-inv : Pointwise R nothing x → x ≡ nothing just-inv : Pointwise R (just x) y → ∃ λ z → y ≡ just z × R x z + +* New functions in `Reflection.Pattern`: + ```agda + pattern-size : Pattern → ℕ + pattern-args-size : List (Arg Pattern) → ℕ ``` diff --git a/README/Tactic/Cong.agda b/README/Tactic/Cong.agda new file mode 100644 index 0000000000..123bfde70c --- /dev/null +++ b/README/Tactic/Cong.agda @@ -0,0 +1,96 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Examples of how to use Tactic.Cong +------------------------------------------------------------------------ + +{-# OPTIONS --without-K #-} + +module README.Tactic.Cong where + +open import Relation.Binary.PropositionalEquality + +-- Tactic.Cong provides a helper macro for using congruence when reasoning about +-- relations. It allows the "hole" that you are operating in to be inferred from +-- the relation instance you are operating on, through use of ⌞_⌟. + +-- Tactic.Cong is inspired by the agda-holes project. + +--import this to use ⌞_⌟ , lhs and rhs +open import Tactic.Cong.Common + +open import Data.Integer +open import Data.Integer.Properties +open import Function.Base + +-- Tactic.Cong is a very general parameterised module. Common use cases have +-- been bundled as sub-modules with fewer parameters. +-- Tactic.Cong.PropEq and its submodules use congruence of propositional +-- equality, which is the most common use case. +import Tactic.Cong.PropEq.ForAllTypes +import Tactic.Cong.PropEq.ForOneType + +module _ where + open ≡-Reasoning + open Tactic.Cong.PropEq.ForAllTypes 0 _≡_ trans + -- This use of Tactic.Cong.PropEq.ForAllTypes is equivalent to: + -- + -- open Tactic.Cong 0 _≡_ cong ℓSet projₗ projₛ _≡_ trans renaming (_≈⌊_⌋_ to _≡⌊_⌋_) + -- + -- The arguments supplied to the module are: + -- * The recursion limit in the macro when evaluating the functions provided + -- to the macro. This can normally be very low (e.g. 0), and does not depend + -- on the complexity of terms used in your proofs. Increment it if you see + -- an error of the form "Tactic.Cong: evaluation limit reached". + -- * The type of the relation that "begin ... ∎" produces, which is not + -- necessarily propositional equality (see the ≤-Reasoning proof below, for + -- example). + -- * A proof of transitivity of _≡_ with respect to the relation. + + -- example proofs using _≡⌊_⌋_ : + + foo : (a b c d : ℤ) → (a + b) * (c + d) ≡ a * c + a * d + b * c + b * d + foo a b c d = begin + (a + b) * (c + d) ≡⟨ *-distribˡ-+ (a + b) _ _ ⟩ + ⌞ (a + b) * c ⌟ + (a + b) * d ≡⌊ *-distribʳ-+ c a b ⌋ + a * c + b * c + ⌞ (a + b) * d ⌟ ≡⌊ *-distribʳ-+ d a b ⌋ + a * c + b * c + (a * d + b * d) ≡⟨ +-assoc (a * c) _ _ ⟩ + a * c + ⌞ b * c + (a * d + b * d)⌟ ≡⌊ +-comm (b * c) _ ⌋ + a * c + ((a * d + b * d) + b * c) ≡⟨ sym $ +-assoc (a * c) _ _ ⟩ + ⌞ a * c + (a * d + b * d) ⌟ + b * c ≡⌊ sym $ +-assoc (a * c) _ _ ⌋ + a * c + a * d + b * d + b * c ≡⟨ +-assoc (a * c + a * d) _ _ ⟩ + a * c + a * d + ⌞ b * d + b * c ⌟ ≡⌊ +-comm (b * d) _ ⌋ + a * c + a * d + (b * c + b * d) ≡⟨ sym $ +-assoc (a * c + a * d) _ _ ⟩ + a * c + a * d + b * c + b * d ∎ + + bar : (a b c : ℤ) → a + b + c ≡ b + a + c + bar a b c = begin + ⌞ a + _ ⌟ + _ ≡⌊ +-comm a _ ⌋ + _ ∎ + + baz : (a b c : ℤ) → ⌞ a + b ⌟ + c ≡ b + a + c + baz a b c = ⌊⌋ lhs (+-comm a b) + -- The use of lhs above tells the macro to look for ⌞_⌟ in the left hand side + -- of the relation instance. + +module _ where + open ≤-Reasoning + open Tactic.Cong.PropEq.ForOneType 0 _IsRelatedTo_ (λ {i = i} p q → step-≡ i q p) + -- This use of Tactic.Cong.PropEq.ForOneType is equivalent to: + -- + -- open Tactic.Cong 0 _≡_ cong ⊤ω (constω 0ℓ) (constω ℤ) _IsRelatedTo_ (λ {A} {i = i} p q → step-≡ i q p) renaming (_≈⌊_⌋_ to _≡⌊_⌋_) + -- + -- This is similar to the use of Tactic.Cong.PropEq.ForAllTypes, but it works + -- for relations that operate over only one specific type instead of any. + + -- example proof using _≡⌊_⌋_ : + qu : (a b c d : ℤ) → a + b + c ≤ d → b + a + c ≤ d + qu a b c d a+b+c≤d = begin + ⌞ b + a ⌟ + _ ≡⌊ +-comm b _ ⌋ + a + b + c ≤⟨ a+b+c≤d ⟩ + d ∎ + +-- Note: To use this Tactic.Cong with _≡_ and cong from Cubical Agda instead, use +-- something like the following: +-- +-- open import Tactic.Cong 2 _≡_ ℓSet projₗ projₛ _∙_ renaming (_≈⌊_⌋_ to _≡⌊_⌋_) diff --git a/src/Reflection/Apply.agda b/src/Reflection/Apply.agda new file mode 100644 index 0000000000..bb8e61eeb3 --- /dev/null +++ b/src/Reflection/Apply.agda @@ -0,0 +1,208 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Function application of reflected terms +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Data.Nat hiding (_⊔_) + +module Reflection.Apply (limit : ℕ) where + +open import Category.Monad +open import Data.Bool.Base +open import Data.List +open import Data.Maybe.Base hiding (_>>=_) +open import Data.Product +open import Data.Sum.Base +open import Function.Base +open import Level hiding (suc) +open import Reflection hiding (map-Args ; returnTC ; _≟_ ; _>>=_) renaming (return to returnTC) +open import Reflection.Argument +open import Reflection.Argument.Visibility using () renaming (_≟_ to _≟ᵥ_) +open import Reflection.Pattern hiding (_≟_) +open import Reflection.Term +open import Relation.Binary.PropositionalEquality using (_≡_) +open import Relation.Nullary using (does) +open import Relation.Unary using (Decidable ; _⊢_) + +Result : Set → Set +Result A = List ErrorPart ⊎ A + +pattern ok v = inj₂ v +pattern err e = inj₁ e + +module _ where + import Data.Sum.Categorical.Left (List ErrorPart) 0ℓ as S + open RawMonad S.monad + + failed-app : Term → Arg Term → Result Term + failed-app t (arg _ a) = err (strErr "attempted to apply" ∷ termErr a ∷ strErr "to" ∷ termErr t ∷ []) + + data Fuel : Set 0ℓ where + fuel : ℕ → Fuel + + {- These functions take a term that needs to be embedded within another term + and corrects all de-Bruijn indices to existing variables to still refer to + the same variables after being embedded. + + The first argument is the embedding depth to shift by. + + The second is used during recursion to track the depth within the whole + term that is being transformed. Non-recursive calls to shift-index should + pass 0 for this argument. + -} + shift-index : ℕ → ℕ → Term → Term + shift-index-args : ℕ → ℕ → Args Term → Args Term + shift-index-clauses : ℕ → ℕ → List Clause → List Clause + + shift-index i j (var k args) with does (j ≤? k) + ... | true = var (i + k) $ shift-index-args i j args + ... | false = var k $ shift-index-args i j args + shift-index i j (con c args) = con c $ shift-index-args i j args + shift-index i j (def f args) = def f $ shift-index-args i j args + shift-index i j (meta x args) = meta x $ shift-index-args i j args + shift-index i j (lam v (abs s t)) = lam v $ abs s $ shift-index i (suc j) t + shift-index i j (pat-lam cs args) = let + cs = shift-index-clauses i j cs + args = shift-index-args i j args + in pat-lam cs args + shift-index i j (Π[ s ∶ arg v A ] t) = let + A = shift-index i j A + t = shift-index i (suc j) t + in Π[ s ∶ arg v A ] t + shift-index i j (sort s) = sort s + shift-index i j (lit l) = lit l + shift-index i j unknown = unknown + + shift-index-args i j [] = [] + shift-index-args i j (arg info a ∷ as) = let + a = shift-index i j a + as = shift-index-args i j as + in arg info a ∷ as + + shift-index-clauses i j [] = [] + shift-index-clauses i j (clause ps t ∷ cs) = let + t = shift-index i (j + pattern-args-size ps) t + cs = shift-index-clauses i j cs + in clause ps t ∷ cs + shift-index-clauses i j (absurd-clause ps ∷ cs) = + absurd-clause ps ∷ shift-index-clauses i j cs + + app : ⦃ Fuel ⦄ → Arg Term → Term → Result Term + app-many : ⦃ Fuel ⦄ → Args Term → Term → Result Term + subst : ⦃ Fuel ⦄ → ℕ → Term → Term → Result Term + subst-args : ⦃ Fuel ⦄ → ℕ → Term → Args Term → Result (Args Term) + subst-clauses : ⦃ Fuel ⦄ → ℕ → Term → List (Clause) → Result (List Clause) + + app a (var x args) = return $ var x (args ∷ʳ a) + app a (con c args) = return $ con c (args ∷ʳ a) + app a (def f args) = return $ def f (args ∷ʳ a) + app a (meta x args) = return $ meta x (args ∷ʳ a) + app a (pat-lam cs args) = return $ pat-lam cs (args ∷ʳ a) + app a @ (arg (arg-info v₁ _) x) + b @ (lam v₂ (abs _ t)) + with does (v₁ ≟ᵥ v₂) + ... | true = subst 0 x t + ... | false = failed-app b a + app a @ (arg (arg-info v₁ _) x) + b @ (Π[ _ ∶ arg (arg-info v₂ _) _ ] t) + with does (v₁ ≟ᵥ v₂) + ... | true = subst 0 x t + ... | false = failed-app b a + -- catch all + app a t = failed-app t a + + app-many [] t = return t + app-many (a ∷ as) t = do + ta ← app a t + app-many as ta + + subst i x (var j args) with compare i j + ... | less m k = do + args ← subst-args i x args + -- decrement j by one since λ was eliminated + return $ var (m + k) args -- j ≡ suc (m + k) + ... | greater _ _ = do + args ← subst-args i x args + -- j refers to variable named inside eliminated λ + return $ var j args + subst ⦃ fuel (suc n) ⦄ + i x (var j args) | equal _ = do + args ← subst-args ⦃ fuel (suc n) ⦄ i x args + app-many ⦃ fuel n ⦄ args (shift-index i 0 x) + subst ⦃ fuel zero ⦄ + i x (var j []) | equal _ = return (shift-index i 0 x) + subst ⦃ fuel zero ⦄ + _ _ (var j (_ ∷ _)) | equal _ = err (strErr "evaluation limit reached" ∷ []) + subst i x (con c args) = do + args ← subst-args i x args + return $ con c args + subst i x (def f args) = do + args ← subst-args i x args + return $ def f args + subst i x (lam v (abs s t)) = do + t ← subst (suc i) x t + return $ lam v (abs s t) + subst i x (meta m args) = do + args ← subst-args i x args + return $ meta m args + subst i x (sort s) = return $ sort s + subst i x (lit l) = return $ lit l + subst i x unknown = return unknown + subst i x (pat-lam cs args) = do + cs ← subst-clauses i x cs + args ← subst-args i x args + return $ pat-lam cs args + subst i x (Π[ s ∶ arg v A ] t) = do + A ← subst i x A + t ← subst (suc i) x t + return $ Π[ s ∶ arg v A ] t + + subst-args i x [] = return [] + subst-args i x (arg v a ∷ as) = do + a ← subst i x a + as ← subst-args i x as + return $ arg v a ∷ as + + subst-clauses i x [] = return [] + subst-clauses i x (clause ps t ∷ cs) = do + t ← subst (i + pattern-args-size ps) x t + cs ← subst-clauses i x cs + return $ clause ps t ∷ cs + subst-clauses i x (absurd-clause ps ∷ cs) = do + cs ← subst-clauses i x cs + return $ absurd-clause ps ∷ cs + +{- Apply an argument to a term. Fails if the recusion limit is reached or an + attempt is made to apply an argument to non-function-like term. +-} +apply : Term → Arg Term → Result Term +apply f x = app ⦃ fuel limit ⦄ x f + +{- Retrieve any trailing arguments in a term -} +term-args : Term → Maybe (Args Term) +term-args (var _ args) = just args +term-args (con _ args) = just args +term-args (def _ args) = just args +term-args (pat-lam _ args) = just args +term-args (meta _ args) = just args +-- catch all +term-args other = nothing + +{- Like term-args, but contains only the visible arguments -} +term-vis-args : Term → Maybe (List Term) +term-vis-args t = do + args ← term-args t + just $ Data.List.map (λ {(arg _ t) → t}) $ filter is-vis args + where + open Data.Maybe.Base using (_>>=_) + args = term-args t + is-vis : Decidable ((λ {(arg (arg-info v _) _) → v}) ⊢ (_≡ visible)) + is-vis (arg (arg-info v r) x) = v ≟ᵥ visible + +{- Conveniently convert a Result into a TC -} +Result→TC : {A : Set} → Result A → TC A +Result→TC (err e) = typeError e +Result→TC (ok v) = returnTC v diff --git a/src/Reflection/Pattern.agda b/src/Reflection/Pattern.agda index 1ddc317788..4fe6c1cf88 100644 --- a/src/Reflection/Pattern.agda +++ b/src/Reflection/Pattern.agda @@ -11,6 +11,7 @@ module Reflection.Pattern where open import Data.List.Base hiding (_++_) open import Data.List.Properties open import Data.Product +open import Data.Nat.Base open import Data.String as String using (String; braces; parens; _++_; _<+>_) import Reflection.Literal as Literal import Reflection.Name as Name @@ -98,3 +99,16 @@ absurd ≟ absurd = yes refl [] ≟s (_ ∷ _) = no λ() (_ ∷ _) ≟s [] = no λ() + +pattern-size : Pattern → ℕ +pattern-args-size : List (Arg Pattern) → ℕ + +pattern-size (Pattern.con _ ps) = pattern-args-size ps +pattern-size Pattern.dot = 0 +pattern-size (Pattern.var _) = 1 +pattern-size (Pattern.lit _) = 0 +pattern-size (Pattern.proj _) = 0 +pattern-size Pattern.absurd = 0 + +pattern-args-size [] = 0 +pattern-args-size (arg _ p ∷ ps) = pattern-size p + pattern-args-size ps diff --git a/src/Reflection/TypeChecking/Monad.agda b/src/Reflection/TypeChecking/Monad.agda index dd2babfd17..7c0038c4a9 100644 --- a/src/Reflection/TypeChecking/Monad.agda +++ b/src/Reflection/TypeChecking/Monad.agda @@ -24,7 +24,7 @@ open Builtin public using ( TC; bindTC; unify; typeError; inferType; checkType ; normalise; reduce - ; catchTC; quoteTC; unquoteTC + ; catchTC; quoteTC; unquoteTC ; quoteωTC ; getContext; extendContext; inContext; freshName ; declareDef; declarePostulate; defineFun; getType; getDefinition ; blockOnMeta; commitTC; isMacro; withNormalisation diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda new file mode 100644 index 0000000000..d585a2fe1f --- /dev/null +++ b/src/Tactic/Cong.agda @@ -0,0 +1,168 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Macros for making working with cong more convenient +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +import Category.Monad.State +open import Data.Nat renaming (_≟_ to _≟ℕ_) hiding (_⊔_) +open import Data.Product +open import Level renaming (suc to lsuc) +open import Level.Literals +open import Relation.Binary.Definitions +open import Tactic.Cong.Common + +module Tactic.Cong + (recursion-limit : ℕ) + (_≈_ : ∀ {a} {A : Set a} → A → A → Set a) + (cong : {a b : Level} + {A : Set a} + {B : Set b} + (f : A → B) + {x y : A} + (p : x ≈ y) + → (f x) ≈ (f y)) + (Param : Setω) + (Fℓ : Param → Level) + (F : (A : Param) → Set (Fℓ A)) + (_<_ : ∀ {A : Param} → F A → F A → Set (Fℓ A)) + (≈-<-trans : ∀ {A : Param} → Trans {A = F A} {B = F A} {C = F A} _≈_ _<_ _<_) + where + +open import Data.Bool hiding (_<_) +open import Data.List +open import Data.Maybe hiding (_>>=_) +open import Data.Product +open import Data.Unit +open import Function.Base +open import Reflection hiding (map-Args ; _≟_) +open import Reflection.Abstraction +open import Reflection.Apply recursion-limit +open import Reflection.Argument renaming (map to arg-map) +open import Reflection.Name using () renaming (_≟_ to _≟ⁿ_) +open import Reflection.Pattern hiding (_≟_) +open import Reflection.Term hiding (_≟_) +open import Reflection.Show +open import Relation.Nullary +open import Tactic.Cong.Impl + +private + Sort→Level : Sort → TC Level + Sort→Level unknown = typeError (strErr "Tactic.Cong: Could not determine sort of return type" ∷ []) + Sort→Level (set a) = unquoteTC a + Sort→Level (lit n) = return (# n) + + -- for idiom brackets + pure : Term → TC Term + pure t = return t + + -- for idiom brackets + _<*>_ : TC Term → Arg Term → TC Term + f <*> x = do + f ← f + case f ⟨ apply ⟩ x of λ { + (err e) → typeError $ strErr "Tactic.Cong:" ∷ e ; + (ok t) → return t + } + + -- These functions are for calling blockOnMeta on any metavariables found + -- inside a term + -- This is useful to ensure that the term that will be searched + -- for ⌊_⌋ is fully solved beforehand. + block-on-metas : Term → TC ⊤ + block-on-metas-args : Args Term → TC ⊤ + block-on-metas-clauses : List Clause → TC ⊤ + + block-on-metas (var _ args) = block-on-metas-args args + block-on-metas (con _ args) = block-on-metas-args args + block-on-metas (def _ args) = block-on-metas-args args + block-on-metas (lam _ (abs _ t)) = block-on-metas t + block-on-metas (pat-lam cs args) = block-on-metas-clauses cs >> block-on-metas-args args + block-on-metas (Π[ _ ∶ arg _ A ] t) = block-on-metas A >> block-on-metas t + block-on-metas (sort _) = return tt + block-on-metas (lit _) = return tt + block-on-metas (meta m args) = blockOnMeta m + block-on-metas unknown = return tt + + block-on-metas-args [] = return tt + block-on-metas-args (arg _ t ∷ args) = block-on-metas t >> block-on-metas-args args + + block-on-metas-clauses [] = return tt + block-on-metas-clauses (clause _ t ∷ cs) = block-on-metas t >> block-on-metas-clauses cs + block-on-metas-clauses (absurd-clause _ ∷ cs) = block-on-metas-clauses cs + + {- Code common to both ⌊⌋ and _≈⌊_⌋_. + Its main job is to call extract-f and cong and constrain the types of their results. + -} + common : ∀ {a} {A : Set a} {x y : A} → RelSide → x ≈ y → Term → Term → Term → TC ⊤ + common {a = a} {A = A} {x = x} {y = y} rel-side x≈y hole fx fy = do + let chosen-side = case rel-side of λ { lhs → fx ; rhs → fy } + f , true ← return $ extract-f $ chosen-side + where _ , false → typeError $ strErr "Tactic.Cong: could not find ⌊_⌋ in" ∷ termErr chosen-side ∷ [] + a ← quoteTC a + A ← quoteTC A + x ← quoteTC x + y ← quoteTC y + x≈y ← quoteTC x≈y + b ← checkType unknown unknown + B ← checkType unknown unknown + *→* ← quoteωTC {A = {a b : Level} (A : Set a) (B : Set b) → Set (a ⊔ b)} (λ A B → (A → B)) + A→B ← ⦇ *→* (hArg a) (hArg b) (vArg A) (vArg B) ⦈ + f ← checkType f A→B + cong ← quoteωTC {A = congT} cong + out ← ⦇ cong (hArg a) (hArg b) (hArg A) (hArg B) (vArg f) (hArg x) (hArg y) (vArg x≈y) ⦈ + _≈_ ← quoteωTC {A = ∀ {a} {A : Set a} → A → A → Set a} _≈_ + _≈B_ ← ⦇ _≈_ (hArg b) (hArg B) ⦈ + fx≈fy-T ← ⦇ (vArg fx) ≈B (vArg fy) ⦈ + out ← checkType out fx≈fy-T + unify hole out + where + congT : Setω + congT = + {a b : Level} + {A : Set a} + {B : Set b} + (f : A → B) + {x y : A} + (p : x ≈ y) + → (f x) ≈ (f y) + +infixr 2 _≈⌊_⌋_ + +macro + {- call cong, inferring the function argument from the use of ⌊_⌋. The side of + the relation inspected is determined by the RelSide parameter + -} + ⌊⌋ : ∀ {a} {A : Set a} {x y : A} → RelSide → x ≈ y → Term → TC ⊤ + ⌊⌋ rel-side x≈y hole = do + hole-T ← inferType hole + just (fy ∷ fx ∷ _) ← return $ Data.Maybe.map reverse $ term-vis-args hole-T + where _ → typeError $ strErr "Tactic.Cong: unexpected form for relation in" ∷ termErr hole-T ∷ [] + block-on-metas $ case rel-side of λ {lhs → fx ; rhs → fy} + common rel-side x≈y hole fx fy + + {- Equivalent to using ⌊⌋ within _≈⟨_⟩_ -} + _≈⌊_⌋_ : ∀ {a} {A : Set a} {B : Param} {x y : A} {fy end : F B} + → F B → x ≈ y → fy < end → Term → TC ⊤ + _≈⌊_⌋_ {B = B} {fy = fy} {end = end} fx x≈y fy