From 068aa43b842d5c31d2d0f47ef6c925057a3d89a0 Mon Sep 17 00:00:00 2001 From: Dylan Ede Date: Fri, 10 Apr 2020 17:04:27 +0100 Subject: [PATCH 1/8] [ new ] Tactic.Cong --- CHANGELOG.md | 5 + README/Tactic/Cong.agda | 67 ++++++++++++ src/Reflection/Apply.agda | 200 ++++++++++++++++++++++++++++++++++++ src/Reflection/Pattern.agda | 14 +++ src/Tactic/Cong.agda | 185 +++++++++++++++++++++++++++++++++ src/Tactic/Cong/Id.agda | 16 +++ 6 files changed, 487 insertions(+) create mode 100644 README/Tactic/Cong.agda create mode 100644 src/Reflection/Apply.agda create mode 100644 src/Tactic/Cong.agda create mode 100644 src/Tactic/Cong/Id.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 4656d2f2b0..6d7ade2d51 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 ------------------- @@ -57,3 +61,4 @@ Other minor additions * Made first argument of [,]-∘-distr in `Data.Sum.Properties` explicit * Added map-id, map₁₂-commute, [,]-cong, [-,]-cong, [,-]-cong, map-cong, map₁-cong and map₂-cong to `Data.Sum.Properties` +* `Reflection.Pattern`: Calculation of number of bound variables in patterns with `pattern-size` and `pattern-args-size` diff --git a/README/Tactic/Cong.agda b/README/Tactic/Cong.agda new file mode 100644 index 0000000000..66fffa6181 --- /dev/null +++ b/README/Tactic/Cong.agda @@ -0,0 +1,67 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Examples of how to use Tactic.Cong +------------------------------------------------------------------------ + +{-# OPTIONS --without-K #-} + +module README.Tactic.Cong where + +-- 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. + +-- For this README, the relation used is _≡_, though any (non-dependent) relation +-- with congruence and transitivity defined should work +open import Relation.Binary.PropositionalEquality +open ≡-Reasoning + +--import this to use ⌊_⌋ +open import Tactic.Cong.Id + +-- import this to use ⌊⌋ , lhs , rhs and _≡⌊_⌋_ +-- Arguments supplied: +-- * Recursion upper limit when evaluating reflected terms - typically does not +-- need to be large, and mostly depends on the cong and trans supplied, not +-- the equations you want to use this in. +-- * Relation that congruence operates over +-- * The congruence definition itself +-- * Transitivity definition for _≡_. Needed for _≡⌊_⌋_ +open import Tactic.Cong 1 _≡_ cong trans + +-- To use this tactic with _≡_ and cong from Cubical Agda, use +-- something like the following: +-- +-- open import Tactic.Cong 2 _≡_ (λ f p → cong f p) _∙_ + +-- The following proofs show example uses of the macros ⌊⌋ and _≡⌊_⌋_ +-- See Tactic.Cong for more details of how to use these macros + +open import Data.Integer +open import Data.Integer.Properties +open import Function.Base + +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 + b ⌋ + c ≡⌊ +-comm a b ⌋ + b + a + c ∎ + +baz : (a b c : ℤ) → ⌊ a + b ⌋ + c ≡ b + a + c +baz a b c = ⌊⌋ lhs (+-comm a b) diff --git a/src/Reflection/Apply.agda b/src/Reflection/Apply.agda new file mode 100644 index 0000000000..247058fd90 --- /dev/null +++ b/src/Reflection/Apply.agda @@ -0,0 +1,200 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Function application of reflected terms +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Data.Nat + +module Reflection.Apply (limit : ℕ) where + +open import Level renaming (suc to lsuc; _⊔_ to lmax) +open import Data.List +open import Data.Sum.Base +open import Data.Product +open import Function.Base +open import Data.Nat.Base +open import Relation.Nullary +open import Data.Bool.Base +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 Data.Maybe.Base hiding (_>>=_) + +Result : Set 0ℓ → Set 0ℓ +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 import Category.Monad + 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 + + 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 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 + +open import Relation.Binary.PropositionalEquality + +open import Relation.Unary + +{- 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 +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 import Data.Maybe 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 0ℓ} → 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..67843fbba0 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 = 1 +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/Tactic/Cong.agda b/src/Tactic/Cong.agda new file mode 100644 index 0000000000..796bf5c78c --- /dev/null +++ b/src/Tactic/Cong.agda @@ -0,0 +1,185 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Macros for making working with cong more convenient +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Level renaming (suc to lsuc; _⊔_ to lmax) +open import Relation.Binary.Definitions +open import Tactic.Cong.Id +open import Data.Nat renaming (_≟_ to _≟ℕ_) + +module Tactic.Cong + (recursion-limit : ℕ) + (_≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ) + (cong : {aℓ bℓ : Level} + {A : Set aℓ} + {B : Set bℓ} + (f : A → B) + {x y : A} + (p : x ≡ y) + → f x ≡ f y) + (trans : ∀ {ℓ} {A : Set ℓ} → Transitive {A = A} _≡_) + where + +open import Reflection.Term hiding (_≟_) +open import Reflection.Abstraction +open import Reflection.Argument renaming (map to arg-map) +open import Reflection.Apply recursion-limit +open import Reflection.Name using () renaming (_≟_ to _≟ⁿ_) +open import Reflection.Pattern hiding (_≟_) +open import Data.Unit +open import Data.List +open import Function.Base +open import Relation.Nullary +open import Data.Bool +open import Data.Product +open import Data.Maybe hiding (_>>=_) + +infixr 2 _≡⌊_⌋_ + +private + extract-f : Term → Term × Bool + extract-f term = let (term , state) = ex 0 term false in (vLam "hole" term , state ) + where + open import Category.Monad.State + open RawMonadState (StateMonadState Bool) + + ex : ℕ → Term → State Bool Term + ex-args : ℕ → List (Arg Term) → State Bool (List (Arg Term)) + ex-clauses : ℕ → List Clause → State Bool (List Clause) + + ex hole-i (var var-i args) with does (var-i ≥? hole-i) + ... | true = do + args ← ex-args hole-i args + return $ var (suc var-i) args + ... | false = do + args ← ex-args hole-i args + return $ var var-i args + ex hole-i (def f _ ) with does (f ≟ⁿ quote ⌊_⌋) + ex hole-i (def _ (_ ⟅∷⟆ _ ⟅∷⟆ _ ⟨∷⟩ args)) | true = do + put true + args ← ex-args hole-i args + return $ var hole-i args + ex hole-i (def f args) | _ = do + args ← ex-args hole-i args + return $ def f args + ex hole-i (con c args) = do + args ← ex-args hole-i args + return $ con c args + ex hole-i (lam v (abs s t)) = do + t ← ex (suc hole-i) t + return $ lam v $ abs s t + ex hole-i (pat-lam cs args) = do + cs ← ex-clauses hole-i cs + args ← ex-args hole-i args + return $ pat-lam cs args + ex hole-i (meta x args) = do + args ← ex-args hole-i args + return $ meta x args + ex hole-i (Π[ s ∶ arg v A ] t) = do + A ← ex hole-i A + t ← ex (suc hole-i) t + return $ Π[ s ∶ arg v A ] t + ex hole-i (sort s) = return $ sort s + ex hole-i (lit l) = return $ lit l + ex hole-i unknown = return unknown + + ex-args hole-i [] = return [] + ex-args hole-i (arg v t ∷ as) = do + t ← ex hole-i t + as ← ex-args hole-i as + return $ arg v t ∷ as + + ex-clauses hole-i [] = return [] + ex-clauses hole-i (clause ps t ∷ cs) = do + t ← ex (hole-i + pattern-args-size ps) t + cs ← ex-clauses hole-i cs + return $ clause ps t ∷ cs + ex-clauses hole-i (absurd-clause ps ∷ cs) = do + cs ← ex-clauses hole-i cs + return $ absurd-clause ps ∷ cs + +open import Reflection hiding (map-Args ; _≟_) + +data RelSide : Set 0ℓ where + lhs : RelSide + rhs : RelSide + +private + Sort→Level : Sort → TC Level + Sort→Level unknown = typeError (strErr "Tactic.Cong: Could not determine sort of return type" ∷ []) + Sort→Level (set ℓ) = unquoteTC ℓ + Sort→Level (lit n) = return (for-n n) + where + for-n : ℕ → Level + for-n ℕ.zero = 0ℓ + for-n (suc n) = lsuc (for-n 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 + } + + ⌊⌋' : ∀ {ℓ} {A : Set ℓ} {x y : A} → RelSide → x ≡ y → Term → TC ⊤ + ⌊⌋' {ℓ = aℓ} {A = A} {x = x} {y = y} rel-side x≡y hole = do + hole-T ← inferType hole + agda-sort hole-sort ← withNormalisation true $ inferType hole-T + where other → typeError $ strErr "Tactic.Cong: expected a sort, got" ∷ termErr other ∷ [] + bℓ ← Sort→Level hole-sort + just (fx ∷ fy ∷ _) ← return $ term-vis-args hole-T + where _ → typeError $ strErr "Tactic.Cong: unexpected form for relation in" ∷ termErr hole-T ∷ [] + cong ← quoteTC {A = congT aℓ bℓ} cong + Set-bℓ ← quoteTC (Set bℓ) + A→ ← quoteTC (λ (B : Set bℓ) → (A → B)) + A ← quoteTC A + B ← checkType unknown Set-bℓ + A→B ← ⦇ A→ (vArg B) ⦈ + 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 ∷ [] + f ← checkType f A→B + x ← quoteTC x + y ← quoteTC y + x≡y ← quoteTC x≡y + out ← ⦇ cong (hArg A) (hArg B) (vArg f) (hArg x) (hArg y) (vArg x≡y) ⦈ + unify hole out + where + congT : ∀ aℓ bℓ → Set (lsuc (lmax aℓ bℓ)) + congT aℓ bℓ = + {A : Set aℓ} + {B : Set bℓ} + (f : A → B) + {x y : A} + (p : x ≡ y) + → f x ≡ f y + +macro + {- call cong, inferring the function argument from the use of ⌊_⌋. The side of + the relation inspected is determined by the RelSide parameter + -} + ⌊⌋ : ∀ {ℓ} {A : Set ℓ} {x y : A} → RelSide → x ≡ y → Term → TC ⊤ + ⌊⌋ side = ⌊⌋' side + + {- Convenience macro equivalent to using ⌊⌋ within _≡⟨_⟩_ -} + _≡⌊_⌋_ : ∀ {ℓ} {A : Set ℓ} → Term → {x y : A} → x ≡ y → Term → Term → TC ⊤ + _≡⌊_⌋_ start x≡y end hole = do + start-T ← inferType start + agda-sort start-sort ← withNormalisation true $ inferType start-T + where other → typeError (strErr "Tactic.Cong: expected a sort, got " ∷ termErr other ∷ []) + bℓ ← Sort→Level start-sort + trans ← quoteTC {A = {B : Set bℓ} → Transitive {A = B} _≡_} trans + subhole ← checkType unknown unknown + out ← ⦇ trans (hArg unknown) (hArg start) (hArg unknown) (hArg unknown) (vArg subhole) (vArg end) ⦈ + unify hole out + ⌊⌋' lhs x≡y subhole diff --git a/src/Tactic/Cong/Id.agda b/src/Tactic/Cong/Id.agda new file mode 100644 index 0000000000..a62772e837 --- /dev/null +++ b/src/Tactic/Cong/Id.agda @@ -0,0 +1,16 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Version of id used to annotate expressions for use with Tactic.Cong +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Tactic.Cong.Id where + +open import Level + +⌊_⌋ : ∀ {ℓ} {A : Set ℓ} → A → A +⌊ a ⌋ = a + +{-# NOINLINE ⌊_⌋ #-} From 5e889d7a7b3acaef2b571a882d790a60b28e9996 Mon Sep 17 00:00:00 2001 From: Dylan Ede Date: Sat, 11 Apr 2020 13:47:40 +0100 Subject: [PATCH 2/8] Most changes from review. --- CHANGELOG.md | 6 +- README/Tactic/Cong.agda | 10 +- src/Reflection/Apply.agda | 54 +++++---- src/Reflection/Pattern.agda | 10 +- src/Tactic/Cong.agda | 225 +++++++++++++++++++----------------- 5 files changed, 163 insertions(+), 142 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6d7ade2d51..77dc256de1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -61,4 +61,8 @@ Other minor additions * Made first argument of [,]-∘-distr in `Data.Sum.Properties` explicit * Added map-id, map₁₂-commute, [,]-cong, [-,]-cong, [,-]-cong, map-cong, map₁-cong and map₂-cong to `Data.Sum.Properties` -* `Reflection.Pattern`: Calculation of number of bound variables in patterns with `pattern-size` and `pattern-args-size` +* 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 index 66fffa6181..63def0672e 100644 --- a/README/Tactic/Cong.agda +++ b/README/Tactic/Cong.agda @@ -22,20 +22,20 @@ open ≡-Reasoning --import this to use ⌊_⌋ open import Tactic.Cong.Id --- import this to use ⌊⌋ , lhs , rhs and _≡⌊_⌋_ +-- import this to use ⌊⌋ , lhs , rhs and _≈⌊_⌋_ -- Arguments supplied: -- * Recursion upper limit when evaluating reflected terms - typically does not -- need to be large, and mostly depends on the cong and trans supplied, not -- the equations you want to use this in. --- * Relation that congruence operates over +-- * _≈_, relation that congruence operates over -- * The congruence definition itself --- * Transitivity definition for _≡_. Needed for _≡⌊_⌋_ -open import Tactic.Cong 1 _≡_ cong trans +-- * Transitivity definition for _≈_. Needed for _≈⌊_⌋_ +open import Tactic.Cong 0 _≡_ cong trans renaming (_≈⌊_⌋_ to _≡⌊_⌋_) -- To use this tactic with _≡_ and cong from Cubical Agda, use -- something like the following: -- --- open import Tactic.Cong 2 _≡_ (λ f p → cong f p) _∙_ +-- open import Tactic.Cong 2 _≡_ (λ f p → cong f p) _∙_ renaming (_≈⌊_⌋_ to _≡⌊_⌋_) -- The following proofs show example uses of the macros ⌊⌋ and _≡⌊_⌋_ -- See Tactic.Cong for more details of how to use these macros diff --git a/src/Reflection/Apply.agda b/src/Reflection/Apply.agda index 247058fd90..f85cde207c 100644 --- a/src/Reflection/Apply.agda +++ b/src/Reflection/Apply.agda @@ -6,26 +6,28 @@ {-# OPTIONS --without-K --safe #-} -open import Data.Nat +open import Data.Nat hiding (_⊔_) module Reflection.Apply (limit : ℕ) where -open import Level renaming (suc to lsuc; _⊔_ to lmax) +open import Category.Monad +open import Data.Bool.Base open import Data.List -open import Data.Sum.Base +open import Data.Maybe.Base hiding (_>>=_) open import Data.Product +open import Data.Sum.Base open import Function.Base -open import Data.Nat.Base -open import Relation.Nullary -open import Data.Bool.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 Data.Maybe.Base hiding (_>>=_) +open import Relation.Binary.PropositionalEquality using (_≡_) +open import Relation.Nullary using (does) +open import Relation.Unary using (Decidable ; _⊢_) -Result : Set 0ℓ → Set 0ℓ +Result : Set → Set Result A = List ErrorPart ⊎ A pattern ok v = inj₂ v @@ -33,7 +35,6 @@ pattern err e = inj₁ e module _ where import Data.Sum.Categorical.Left (List ErrorPart) 0ℓ as S - open import Category.Monad open RawMonad S.monad failed-app : Term → Arg Term → Result Term @@ -42,6 +43,16 @@ module _ where 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 @@ -170,18 +181,15 @@ module _ where apply : Term → Arg Term → Result Term apply f x = app ⦃ fuel limit ⦄ x f -open import Relation.Binary.PropositionalEquality - -open import Relation.Unary - {- 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 (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 -term-args other = nothing +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) @@ -189,12 +197,12 @@ term-vis-args t = do args ← term-args t just $ Data.List.map (λ {(arg _ t) → t}) $ filter is-vis args where - open import Data.Maybe using (_>>=_) - args = term-args t - is-vis : Decidable ((λ {(arg (arg-info v _) _) → v}) ⊢ (_≡ visible)) - is-vis (arg (arg-info v r) x) = v ≟ᵥ visible + 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 0ℓ} → Result A → TC A +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 67843fbba0..0fa4dfad9d 100644 --- a/src/Reflection/Pattern.agda +++ b/src/Reflection/Pattern.agda @@ -104,11 +104,11 @@ pattern-size : Pattern → ℕ pattern-args-size : List (Arg Pattern) → ℕ pattern-size (Pattern.con _ ps) = pattern-args-size ps -pattern-size Pattern.dot = 1 -pattern-size (Pattern.var _) = 1 -pattern-size (Pattern.lit _) = 0 -pattern-size (Pattern.proj _) = 0 -pattern-size Pattern.absurd = 0 +pattern-size Pattern.dot = 1 +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/Tactic/Cong.agda b/src/Tactic/Cong.agda index 796bf5c78c..49439dec21 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -6,103 +6,113 @@ {-# OPTIONS --without-K --safe #-} -open import Level renaming (suc to lsuc; _⊔_ to lmax) +import Category.Monad.State +open import Data.Nat renaming (_≟_ to _≟ℕ_) hiding (_⊔_) +open import Level renaming (suc to lsuc) +open import Level.Literals open import Relation.Binary.Definitions open import Tactic.Cong.Id -open import Data.Nat renaming (_≟_ to _≟ℕ_) +open import Data.Product module Tactic.Cong (recursion-limit : ℕ) - (_≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ) - (cong : {aℓ bℓ : Level} - {A : Set aℓ} - {B : Set bℓ} + (_≈_ : ∀ {a} {A : Set a} → A → A → Set a) + (cong : ∀ {a b} + {A : Set a} + {B : Set b} (f : A → B) {x y : A} - (p : x ≡ y) - → f x ≡ f y) - (trans : ∀ {ℓ} {A : Set ℓ} → Transitive {A = A} _≡_) + (p : x ≈ y) + → f x ≈ f y) + (trans : ∀{a} {A : Set a} → Transitive {A = A} _≈_) where -open import Reflection.Term hiding (_≟_) +open import Data.Bool +open import Data.List +open import Data.Maybe hiding (_>>=_) +open import Data.Product +open import Data.Unit +open import Function.Base +import Reflection open import Reflection.Abstraction -open import Reflection.Argument renaming (map to arg-map) 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 Data.Unit -open import Data.List -open import Function.Base +open import Reflection.Term hiding (_≟_) open import Relation.Nullary -open import Data.Bool -open import Data.Product -open import Data.Maybe hiding (_>>=_) - -infixr 2 _≡⌊_⌋_ private + {- This function turns a term containing ⌊_⌋ into a lambda term with all + instances of ⌊_⌋ replaced with the argument variable of the lambda. + + Returns the transformed term plus a Bool indicating whether any ⌊_⌋ were + found. Not finding any ⌊_⌋ generally indicates that the macro has been used + incorrectly. + -} extract-f : Term → Term × Bool extract-f term = let (term , state) = ex 0 term false in (vLam "hole" term , state ) where - open import Category.Monad.State - open RawMonadState (StateMonadState Bool) - - ex : ℕ → Term → State Bool Term - ex-args : ℕ → List (Arg Term) → State Bool (List (Arg Term)) - ex-clauses : ℕ → List Clause → State Bool (List Clause) - - ex hole-i (var var-i args) with does (var-i ≥? hole-i) - ... | true = do - args ← ex-args hole-i args - return $ var (suc var-i) args - ... | false = do - args ← ex-args hole-i args - return $ var var-i args - ex hole-i (def f _ ) with does (f ≟ⁿ quote ⌊_⌋) - ex hole-i (def _ (_ ⟅∷⟆ _ ⟅∷⟆ _ ⟨∷⟩ args)) | true = do - put true - args ← ex-args hole-i args - return $ var hole-i args - ex hole-i (def f args) | _ = do - args ← ex-args hole-i args - return $ def f args - ex hole-i (con c args) = do - args ← ex-args hole-i args - return $ con c args - ex hole-i (lam v (abs s t)) = do - t ← ex (suc hole-i) t - return $ lam v $ abs s t - ex hole-i (pat-lam cs args) = do - cs ← ex-clauses hole-i cs - args ← ex-args hole-i args - return $ pat-lam cs args - ex hole-i (meta x args) = do - args ← ex-args hole-i args - return $ meta x args - ex hole-i (Π[ s ∶ arg v A ] t) = do - A ← ex hole-i A - t ← ex (suc hole-i) t - return $ Π[ s ∶ arg v A ] t - ex hole-i (sort s) = return $ sort s - ex hole-i (lit l) = return $ lit l - ex hole-i unknown = return unknown - - ex-args hole-i [] = return [] - ex-args hole-i (arg v t ∷ as) = do - t ← ex hole-i t - as ← ex-args hole-i as - return $ arg v t ∷ as - - ex-clauses hole-i [] = return [] - ex-clauses hole-i (clause ps t ∷ cs) = do - t ← ex (hole-i + pattern-args-size ps) t - cs ← ex-clauses hole-i cs - return $ clause ps t ∷ cs - ex-clauses hole-i (absurd-clause ps ∷ cs) = do - cs ← ex-clauses hole-i cs - return $ absurd-clause ps ∷ cs - -open import Reflection hiding (map-Args ; _≟_) + -- State Monad is used to track whether any ⌊_⌋ have been found + open Category.Monad.State + open RawMonadState (StateMonadState Bool) + + ex : ℕ → Term → State Bool Term + ex-args : ℕ → List (Arg Term) → State Bool (List (Arg Term)) + ex-clauses : ℕ → List Clause → State Bool (List Clause) + + ex hole-i (var var-i args) with does (var-i ≥? hole-i) + ... | true = do + args ← ex-args hole-i args + return $ var (suc var-i) args + ... | false = do + args ← ex-args hole-i args + return $ var var-i args + ex hole-i (def f _ ) with does (f ≟ⁿ quote ⌊_⌋) + ex hole-i (def _ (_ ⟅∷⟆ _ ⟅∷⟆ _ ⟨∷⟩ args)) | true = do + put true -- ⌊_⌋ has been found + args ← ex-args hole-i args + return $ var hole-i args + ex hole-i (def f args) | _ = do + args ← ex-args hole-i args + return $ def f args + ex hole-i (con c args) = do + args ← ex-args hole-i args + return $ con c args + ex hole-i (lam v (abs s t)) = do + t ← ex (suc hole-i) t + return $ lam v $ abs s t + ex hole-i (pat-lam cs args) = do + cs ← ex-clauses hole-i cs + args ← ex-args hole-i args + return $ pat-lam cs args + ex hole-i (meta x args) = do + args ← ex-args hole-i args + return $ meta x args + ex hole-i (Π[ s ∶ arg v A ] t) = do + A ← ex hole-i A + t ← ex (suc hole-i) t + return $ Π[ s ∶ arg v A ] t + ex hole-i (sort s) = return $ sort s + ex hole-i (lit l) = return $ lit l + ex hole-i unknown = return unknown + + ex-args hole-i [] = return [] + ex-args hole-i (arg v t ∷ as) = do + t ← ex hole-i t + as ← ex-args hole-i as + return $ arg v t ∷ as + + ex-clauses hole-i [] = return [] + ex-clauses hole-i (clause ps t ∷ cs) = do + t ← ex (hole-i + pattern-args-size ps) t + cs ← ex-clauses hole-i cs + return $ clause ps t ∷ cs + ex-clauses hole-i (absurd-clause ps ∷ cs) = do + cs ← ex-clauses hole-i cs + return $ absurd-clause ps ∷ cs + +open Reflection hiding (map-Args ; _≟_) data RelSide : Set 0ℓ where lhs : RelSide @@ -111,12 +121,8 @@ data RelSide : Set 0ℓ where private Sort→Level : Sort → TC Level Sort→Level unknown = typeError (strErr "Tactic.Cong: Could not determine sort of return type" ∷ []) - Sort→Level (set ℓ) = unquoteTC ℓ - Sort→Level (lit n) = return (for-n n) - where - for-n : ℕ → Level - for-n ℕ.zero = 0ℓ - for-n (suc n) = lsuc (for-n n) + Sort→Level (set a) = unquoteTC a + Sort→Level (lit n) = return (# n) -- for idiom brackets pure : Term → TC Term @@ -131,19 +137,20 @@ private (ok t) → return t } - ⌊⌋' : ∀ {ℓ} {A : Set ℓ} {x y : A} → RelSide → x ≡ y → Term → TC ⊤ - ⌊⌋' {ℓ = aℓ} {A = A} {x = x} {y = y} rel-side x≡y hole = do + ⌊⌋' : ∀ {a} {A : Set a} {x y : A} → RelSide → x ≈ y → Term → TC ⊤ + ⌊⌋' {a = a} {A = A} {x = x} {y = y} rel-side x≈y hole = do hole-T ← inferType hole agda-sort hole-sort ← withNormalisation true $ inferType hole-T where other → typeError $ strErr "Tactic.Cong: expected a sort, got" ∷ termErr other ∷ [] - bℓ ← Sort→Level hole-sort + b ← Sort→Level hole-sort + -- TODO: Take tail arguments of hole-T, not head just (fx ∷ fy ∷ _) ← return $ term-vis-args hole-T where _ → typeError $ strErr "Tactic.Cong: unexpected form for relation in" ∷ termErr hole-T ∷ [] - cong ← quoteTC {A = congT aℓ bℓ} cong - Set-bℓ ← quoteTC (Set bℓ) - A→ ← quoteTC (λ (B : Set bℓ) → (A → B)) + cong ← quoteTC {A = congT a b} cong + Set-b ← quoteTC (Set b) + A→ ← quoteTC (λ (B : Set b) → (A → B)) A ← quoteTC A - B ← checkType unknown Set-bℓ + B ← checkType unknown Set-b A→B ← ⦇ A→ (vArg B) ⦈ let chosen-side = case rel-side of λ { lhs → fx ; rhs → fy } f , true ← return $ extract-f $ chosen-side @@ -151,35 +158,37 @@ private f ← checkType f A→B x ← quoteTC x y ← quoteTC y - x≡y ← quoteTC x≡y - out ← ⦇ cong (hArg A) (hArg B) (vArg f) (hArg x) (hArg y) (vArg x≡y) ⦈ + x≈y ← quoteTC x≈y + out ← ⦇ cong (hArg A) (hArg B) (vArg f) (hArg x) (hArg y) (vArg x≈y) ⦈ unify hole out where - congT : ∀ aℓ bℓ → Set (lsuc (lmax aℓ bℓ)) - congT aℓ bℓ = - {A : Set aℓ} - {B : Set bℓ} - (f : A → B) - {x y : A} - (p : x ≡ y) - → f x ≡ f y + congT : ∀ a b → Set (lsuc (a ⊔ b)) + congT a b = + {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 : Set ℓ} {x y : A} → RelSide → x ≡ y → Term → TC ⊤ + ⌊⌋ : ∀ {a} {A : Set a} {x y : A} → RelSide → x ≈ y → Term → TC ⊤ ⌊⌋ side = ⌊⌋' side - {- Convenience macro equivalent to using ⌊⌋ within _≡⟨_⟩_ -} - _≡⌊_⌋_ : ∀ {ℓ} {A : Set ℓ} → Term → {x y : A} → x ≡ y → Term → Term → TC ⊤ - _≡⌊_⌋_ start x≡y end hole = do + {- Convenience macro equivalent to using ⌊⌋ within _≈⟨_⟩_ -} + _≈⌊_⌋_ : ∀ {a} {A : Set a} → Term → {x y : A} → x ≈ y → Term → Term → TC ⊤ + _≈⌊_⌋_ start x≈y end hole = do start-T ← inferType start agda-sort start-sort ← withNormalisation true $ inferType start-T where other → typeError (strErr "Tactic.Cong: expected a sort, got " ∷ termErr other ∷ []) - bℓ ← Sort→Level start-sort - trans ← quoteTC {A = {B : Set bℓ} → Transitive {A = B} _≡_} trans + b ← Sort→Level start-sort + trans ← quoteTC {A = {B : Set b} → Transitive {A = B} _≈_} trans subhole ← checkType unknown unknown out ← ⦇ trans (hArg unknown) (hArg start) (hArg unknown) (hArg unknown) (vArg subhole) (vArg end) ⦈ unify hole out - ⌊⌋' lhs x≡y subhole + ⌊⌋' lhs x≈y subhole From bf67445b00fe76a72e6df801bd07e863def50894 Mon Sep 17 00:00:00 2001 From: Dylan Ede Date: Sun, 12 Apr 2020 16:12:57 +0100 Subject: [PATCH 3/8] Tactic.Cong reworked to be more general. --- README/Tactic/Cong.agda | 123 +++++++++++------- src/Reflection/Apply.agda | 2 +- src/Reflection/TypeChecking/Monad.agda | 2 +- src/Tactic/Cong.agda | 161 ++++++++---------------- src/Tactic/Cong/Common.agda | 37 ++++++ src/Tactic/Cong/Id.agda | 16 --- src/Tactic/Cong/Impl.agda | 86 +++++++++++++ src/Tactic/Cong/PropEq.agda | 24 ++++ src/Tactic/Cong/PropEq/ForAllTypes.agda | 21 ++++ src/Tactic/Cong/PropEq/ForOneType.agda | 24 ++++ 10 files changed, 323 insertions(+), 173 deletions(-) create mode 100644 src/Tactic/Cong/Common.agda delete mode 100644 src/Tactic/Cong/Id.agda create mode 100644 src/Tactic/Cong/Impl.agda create mode 100644 src/Tactic/Cong/PropEq.agda create mode 100644 src/Tactic/Cong/PropEq/ForAllTypes.agda create mode 100644 src/Tactic/Cong/PropEq/ForOneType.agda diff --git a/README/Tactic/Cong.agda b/README/Tactic/Cong.agda index 63def0672e..123bfde70c 100644 --- a/README/Tactic/Cong.agda +++ b/README/Tactic/Cong.agda @@ -8,60 +8,89 @@ 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 ⌊_⌋. +-- the relation instance you are operating on, through use of ⌞_⌟. -- Tactic.Cong is inspired by the agda-holes project. --- For this README, the relation used is _≡_, though any (non-dependent) relation --- with congruence and transitivity defined should work -open import Relation.Binary.PropositionalEquality -open ≡-Reasoning - ---import this to use ⌊_⌋ -open import Tactic.Cong.Id - --- import this to use ⌊⌋ , lhs , rhs and _≈⌊_⌋_ --- Arguments supplied: --- * Recursion upper limit when evaluating reflected terms - typically does not --- need to be large, and mostly depends on the cong and trans supplied, not --- the equations you want to use this in. --- * _≈_, relation that congruence operates over --- * The congruence definition itself --- * Transitivity definition for _≈_. Needed for _≈⌊_⌋_ -open import Tactic.Cong 0 _≡_ cong trans renaming (_≈⌊_⌋_ to _≡⌊_⌋_) - --- To use this tactic with _≡_ and cong from Cubical Agda, use --- something like the following: --- --- open import Tactic.Cong 2 _≡_ (λ f p → cong f p) _∙_ renaming (_≈⌊_⌋_ to _≡⌊_⌋_) - --- The following proofs show example uses of the macros ⌊⌋ and _≡⌊_⌋_ --- See Tactic.Cong for more details of how to use these macros +--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 -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 + b ⌋ + c ≡⌊ +-comm a b ⌋ - b + a + c ∎ - -baz : (a b c : ℤ) → ⌊ a + b ⌋ + c ≡ b + a + c -baz a b c = ⌊⌋ lhs (+-comm a b) +-- 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 index f85cde207c..bb8e61eeb3 100644 --- a/src/Reflection/Apply.agda +++ b/src/Reflection/Apply.agda @@ -133,7 +133,7 @@ module _ where 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 x + 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 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 index 49439dec21..6994f32211 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -11,112 +11,42 @@ open import Data.Nat renaming (_≟_ to _≟ℕ_) hiding (_⊔_) open import Level renaming (suc to lsuc) open import Level.Literals open import Relation.Binary.Definitions -open import Tactic.Cong.Id +open import Tactic.Cong.Common open import Data.Product module Tactic.Cong (recursion-limit : ℕ) (_≈_ : ∀ {a} {A : Set a} → A → A → Set a) - (cong : ∀ {a b} + (cong : {a b : Level} {A : Set a} {B : Set b} (f : A → B) {x y : A} (p : x ≈ y) - → f x ≈ f y) - (trans : ∀{a} {A : Set a} → Transitive {A = A} _≈_) + → (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 +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 -import Reflection +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 - -private - {- This function turns a term containing ⌊_⌋ into a lambda term with all - instances of ⌊_⌋ replaced with the argument variable of the lambda. - - Returns the transformed term plus a Bool indicating whether any ⌊_⌋ were - found. Not finding any ⌊_⌋ generally indicates that the macro has been used - incorrectly. - -} - extract-f : Term → Term × Bool - extract-f term = let (term , state) = ex 0 term false in (vLam "hole" term , state ) - where - -- State Monad is used to track whether any ⌊_⌋ have been found - open Category.Monad.State - open RawMonadState (StateMonadState Bool) - - ex : ℕ → Term → State Bool Term - ex-args : ℕ → List (Arg Term) → State Bool (List (Arg Term)) - ex-clauses : ℕ → List Clause → State Bool (List Clause) - - ex hole-i (var var-i args) with does (var-i ≥? hole-i) - ... | true = do - args ← ex-args hole-i args - return $ var (suc var-i) args - ... | false = do - args ← ex-args hole-i args - return $ var var-i args - ex hole-i (def f _ ) with does (f ≟ⁿ quote ⌊_⌋) - ex hole-i (def _ (_ ⟅∷⟆ _ ⟅∷⟆ _ ⟨∷⟩ args)) | true = do - put true -- ⌊_⌋ has been found - args ← ex-args hole-i args - return $ var hole-i args - ex hole-i (def f args) | _ = do - args ← ex-args hole-i args - return $ def f args - ex hole-i (con c args) = do - args ← ex-args hole-i args - return $ con c args - ex hole-i (lam v (abs s t)) = do - t ← ex (suc hole-i) t - return $ lam v $ abs s t - ex hole-i (pat-lam cs args) = do - cs ← ex-clauses hole-i cs - args ← ex-args hole-i args - return $ pat-lam cs args - ex hole-i (meta x args) = do - args ← ex-args hole-i args - return $ meta x args - ex hole-i (Π[ s ∶ arg v A ] t) = do - A ← ex hole-i A - t ← ex (suc hole-i) t - return $ Π[ s ∶ arg v A ] t - ex hole-i (sort s) = return $ sort s - ex hole-i (lit l) = return $ lit l - ex hole-i unknown = return unknown - - ex-args hole-i [] = return [] - ex-args hole-i (arg v t ∷ as) = do - t ← ex hole-i t - as ← ex-args hole-i as - return $ arg v t ∷ as - - ex-clauses hole-i [] = return [] - ex-clauses hole-i (clause ps t ∷ cs) = do - t ← ex (hole-i + pattern-args-size ps) t - cs ← ex-clauses hole-i cs - return $ clause ps t ∷ cs - ex-clauses hole-i (absurd-clause ps ∷ cs) = do - cs ← ex-clauses hole-i cs - return $ absurd-clause ps ∷ cs - -open Reflection hiding (map-Args ; _≟_) - -data RelSide : Set 0ℓ where - lhs : RelSide - rhs : RelSide +open import Tactic.Cong.Impl private Sort→Level : Sort → TC Level @@ -140,36 +70,39 @@ private ⌊⌋' : ∀ {a} {A : Set a} {x y : A} → RelSide → x ≈ y → Term → TC ⊤ ⌊⌋' {a = a} {A = A} {x = x} {y = y} rel-side x≈y hole = do hole-T ← inferType hole - agda-sort hole-sort ← withNormalisation true $ inferType hole-T - where other → typeError $ strErr "Tactic.Cong: expected a sort, got" ∷ termErr other ∷ [] - b ← Sort→Level hole-sort - -- TODO: Take tail arguments of hole-T, not head + -- TODO: Use the tail of the list just (fx ∷ fy ∷ _) ← return $ term-vis-args hole-T where _ → typeError $ strErr "Tactic.Cong: unexpected form for relation in" ∷ termErr hole-T ∷ [] - cong ← quoteTC {A = congT a b} cong - Set-b ← quoteTC (Set b) - A→ ← quoteTC (λ (B : Set b) → (A → B)) - A ← quoteTC A - B ← checkType unknown Set-b - A→B ← ⦇ A→ (vArg B) ⦈ 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 ∷ [] - f ← checkType f A→B + a ← quoteTC a + A ← quoteTC A x ← quoteTC x y ← quoteTC y x≈y ← quoteTC x≈y - out ← ⦇ cong (hArg A) (hArg B) (vArg f) (hArg x) (hArg y) (vArg 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 : ∀ a b → Set (lsuc (a ⊔ b)) - congT a b = + 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 + → (f x) ≈ (f y) infixr 2 _≈⌊_⌋_ @@ -178,17 +111,29 @@ macro the relation inspected is determined by the RelSide parameter -} ⌊⌋ : ∀ {a} {A : Set a} {x y : A} → RelSide → x ≈ y → Term → TC ⊤ - ⌊⌋ side = ⌊⌋' side + ⌊⌋ = ⌊⌋' {- Convenience macro equivalent to using ⌊⌋ within _≈⟨_⟩_ -} - _≈⌊_⌋_ : ∀ {a} {A : Set a} → Term → {x y : A} → x ≈ y → Term → Term → TC ⊤ - _≈⌊_⌋_ start x≈y end hole = do - start-T ← inferType start - agda-sort start-sort ← withNormalisation true $ inferType start-T - where other → typeError (strErr "Tactic.Cong: expected a sort, got " ∷ termErr other ∷ []) - b ← Sort→Level start-sort - trans ← quoteTC {A = {B : Set b} → Transitive {A = B} _≈_} trans - subhole ← checkType unknown unknown - out ← ⦇ trans (hArg unknown) (hArg start) (hArg unknown) (hArg unknown) (vArg subhole) (vArg end) ⦈ + _≈⌊_⌋_ : ∀ {a} {A : Set a} {B : Param} {x y : A} {fy end : F B} + → F B → x ≈ y → fy < end → Term → TC ⊤ + _≈⌊_⌋_ {a = a} {A = A} {B = B} {fy = fy} {end = end} fx x≈y fy Date: Sun, 12 Apr 2020 19:27:37 +0100 Subject: [PATCH 4/8] Added header to Tactic.Cong.Impl --- src/Tactic/Cong/Impl.agda | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Tactic/Cong/Impl.agda b/src/Tactic/Cong/Impl.agda index ca18073561..61f01ccea0 100644 --- a/src/Tactic/Cong/Impl.agda +++ b/src/Tactic/Cong/Impl.agda @@ -1,3 +1,9 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Implementation details of Tactic.Cong - do not use directly +------------------------------------------------------------------------ + {-# OPTIONS --without-K --safe #-} module Tactic.Cong.Impl where From c818edad1f2fbcf0341114f66af9c90f4d29e17a Mon Sep 17 00:00:00 2001 From: Dylan Ede Date: Sun, 12 Apr 2020 19:33:31 +0100 Subject: [PATCH 5/8] Reordered module imports --- src/Tactic/Cong.agda | 2 +- src/Tactic/Cong/Common.agda | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index 6994f32211..fc31e13c63 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -8,11 +8,11 @@ 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 -open import Data.Product module Tactic.Cong (recursion-limit : ℕ) diff --git a/src/Tactic/Cong/Common.agda b/src/Tactic/Cong/Common.agda index 89c99291f2..22c34d75c3 100644 --- a/src/Tactic/Cong/Common.agda +++ b/src/Tactic/Cong/Common.agda @@ -8,11 +8,11 @@ module Tactic.Cong.Common where +open import Data.Unit +open import Function.Base open import Level open import Reflection -open import Data.Unit open import Reflection.Apply 64 -open import Function.Base ⌞_⌟ : ∀ {ℓ} {A : Set ℓ} → A → A ⌞ a ⌟ = a From 1b838bd7c6a8d83f71c79192e713b15c612ba89f Mon Sep 17 00:00:00 2001 From: Dylan Ede Date: Mon, 13 Apr 2020 18:04:29 +0100 Subject: [PATCH 6/8] pattern bound variable count corrected --- src/Reflection/Pattern.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Reflection/Pattern.agda b/src/Reflection/Pattern.agda index 0fa4dfad9d..4fe6c1cf88 100644 --- a/src/Reflection/Pattern.agda +++ b/src/Reflection/Pattern.agda @@ -104,7 +104,7 @@ pattern-size : Pattern → ℕ pattern-args-size : List (Arg Pattern) → ℕ pattern-size (Pattern.con _ ps) = pattern-args-size ps -pattern-size Pattern.dot = 1 +pattern-size Pattern.dot = 0 pattern-size (Pattern.var _) = 1 pattern-size (Pattern.lit _) = 0 pattern-size (Pattern.proj _) = 0 From bb0fe12277b8f2250f6c302d2b821ff1f473a5a7 Mon Sep 17 00:00:00 2001 From: Dylan Ede Date: Mon, 13 Apr 2020 19:31:55 +0100 Subject: [PATCH 7/8] =?UTF-8?q?Refactored=20=E2=8C=8A=E2=8C=8B=20and=20=5F?= =?UTF-8?q?=E2=89=88=E2=8C=8A=5F=E2=8C=8B=5F=20so=20that=20=5F=E2=89=88?= =?UTF-8?q?=E2=8C=8A=5F=E2=8C=8B=5F=20can=20accept=20more=20forms=20for=20?= =?UTF-8?q?=5F=E2=89=88=5F.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Tactic/Cong.agda | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index fc31e13c63..9a273b8dc1 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -67,12 +67,11 @@ private (ok t) → return t } - ⌊⌋' : ∀ {a} {A : Set a} {x y : A} → RelSide → x ≈ y → Term → TC ⊤ - ⌊⌋' {a = a} {A = A} {x = x} {y = y} rel-side x≈y hole = do - hole-T ← inferType hole - -- TODO: Use the tail of the list - just (fx ∷ fy ∷ _) ← return $ term-vis-args hole-T - where _ → typeError $ strErr "Tactic.Cong: unexpected form for relation in" ∷ termErr hole-T ∷ [] + {- 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 ∷ [] @@ -83,8 +82,8 @@ private 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) ⦈ + *→* ← 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) ⦈ @@ -111,29 +110,31 @@ macro the relation inspected is determined by the RelSide parameter -} ⌊⌋ : ∀ {a} {A : Set a} {x y : A} → RelSide → x ≈ y → Term → TC ⊤ - ⌊⌋ = ⌊⌋' + ⌊⌋ 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 ∷ [] + common side x≈y hole fx fy - {- Convenience macro equivalent to using ⌊⌋ within _≈⟨_⟩_ -} + {- 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 ⊤ - _≈⌊_⌋_ {a = a} {A = A} {B = B} {fy = fy} {end = end} fx x≈y fy Date: Wed, 15 Apr 2020 19:05:39 +0100 Subject: [PATCH 8/8] Use blockOnMeta to delay function extraction until the target term is fully solved. --- src/Tactic/Cong.agda | 32 ++++++++++++++++++++++++++++++-- 1 file changed, 30 insertions(+), 2 deletions(-) diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index 9a273b8dc1..d585a2fe1f 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -67,6 +67,32 @@ private (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. -} @@ -110,11 +136,12 @@ macro the relation inspected is determined by the RelSide parameter -} ⌊⌋ : ∀ {a} {A : Set a} {x y : A} → RelSide → x ≈ y → Term → TC ⊤ - ⌊⌋ side x≈y hole = do + ⌊⌋ 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 ∷ [] - common side x≈y hole fx fy + 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} @@ -122,6 +149,7 @@ macro _≈⌊_⌋_ {B = B} {fy = fy} {end = end} fx x≈y fy