diff --git a/CHANGELOG.md b/CHANGELOG.md index d61111a7f2..240562b7db 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -548,6 +548,11 @@ New modules Reflection.AlphaEquality ``` +* `cong!` tactic for deriving arguments to `cong` + ``` + Tactic.Rewrite + ``` + * Various system types and primitives: ``` System.Clock.Primitive diff --git a/README/Tactic/Rewrite.agda b/README/Tactic/Rewrite.agda new file mode 100644 index 0000000000..d96c9231a5 --- /dev/null +++ b/README/Tactic/Rewrite.agda @@ -0,0 +1,139 @@ +{-# OPTIONS --without-K --safe #-} +module README.Tactic.Rewrite where + +open import Data.Nat +open import Data.Nat.Properties + +open import Relation.Binary.PropositionalEquality as Eq +import Relation.Binary.Reasoning.Preorder as PR + +open import Tactic.Rewrite using (cong!) + +---------------------------------------------------------------------- +-- Usage +---------------------------------------------------------------------- + +-- When performing large equational reasoning proofs, it's quite +-- common to have to construct sophisticated lambdas to pass +-- into 'cong'. This can be extremely tedious, and can bog down +-- large proofs in piles of boilerplate. The 'cong!' tactic +-- simplifies this process by synthesizing the appropriate call +-- to 'cong' by inspecting both sides of the goal. +-- +-- This is best demonstrated with a small example. Consider +-- the following proof: + +verbose-example : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0) +verbose-example m n eq = + let open Eq.≡-Reasoning in + begin + suc (suc (m + 0)) + m + ≡⟨ cong (λ ϕ → suc (suc (ϕ + m))) (+-identityʳ m) ⟩ + suc (suc m) + m + ≡⟨ cong (λ ϕ → suc (suc (ϕ + ϕ))) eq ⟩ + suc (suc n) + n + ≡˘⟨ cong (λ ϕ → suc (suc (n + ϕ))) (+-identityʳ n) ⟩ + suc (suc n) + (n + 0) + ∎ + +-- The calls to 'cong' add a lot of boilerplate, and also +-- clutter up the proof, making it more difficult to read. +-- We can simplify this by using 'cong!' to deduce those +-- lambdas for us. + +succinct-example : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0) +succinct-example m n eq = + let open Eq.≡-Reasoning in + begin + suc (suc (m + 0)) + m + ≡⟨ cong! (+-identityʳ m) ⟩ + suc (suc m) + m + ≡⟨ cong! eq ⟩ + suc (suc n) + n + ≡˘⟨ cong! (+-identityʳ n) ⟩ + suc (suc n) + (n + 0) + ∎ + +---------------------------------------------------------------------- +-- Limitations +---------------------------------------------------------------------- + +-- The 'cong!' tactic can handle simple cases, but will +-- struggle when presented with equality proofs like +-- 'm + n ≡ n + m' or 'm + (n + o) ≡ (m + n) + o'. +-- +-- The reason behind this is that this tactic operates by simple +-- anti-unification; it examines both sides of the equality goal +-- to deduce where to generalize. When presented with two sides +-- of an equality like 'm + n ≡ n + m', it will anti-unify to +-- 'ϕ + ϕ', which is too specific. + +---------------------------------------------------------------------- +-- Unit Tests +---------------------------------------------------------------------- + +module LiteralTests + (assumption : 48 ≡ 42) + (f : ℕ → ℕ → ℕ → ℕ) + where + + test₁ : 40 + 2 ≡ 42 + test₁ = cong! refl + + test₂ : 48 ≡ 42 → 42 ≡ 48 + test₂ eq = cong! (sym eq) + + test₃ : (f : ℕ → ℕ) → f 48 ≡ f 42 + test₃ f = cong! assumption + + test₄ : (f : ℕ → ℕ → ℕ) → f 48 48 ≡ f 42 42 + test₄ f = cong! assumption + + test₅ : f 48 45 48 ≡ f 42 45 42 + test₅ = cong! assumption + +module LambdaTests + (assumption : 48 ≡ 42) + where + + test₁ : (λ x → x + 48) ≡ (λ x → x + 42) + test₁ = cong! assumption + + test₂ : (λ x y z → x + (y + 48 + z)) ≡ (λ x y z → x + (y + 42 + z)) + test₂ = cong! assumption + +module HigherOrderTests + (f g : ℕ → ℕ) + where + + test₁ : f ≡ g → ∀ n → f n ≡ g n + test₁ eq n = cong! eq + + test₂ : f ≡ g → ∀ n → f (f (f n)) ≡ g (g (g n)) + test₂ eq n = cong! eq + +module EquationalReasoningTests where + + test₁ : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0) + test₁ m n eq = + let open Eq.≡-Reasoning in + begin + suc (suc (m + 0)) + m + ≡⟨ cong! (+-identityʳ m) ⟩ + suc (suc m) + m + ≡⟨ cong! eq ⟩ + suc (suc n) + n + ≡˘⟨ cong! (+-identityʳ n) ⟩ + suc (suc n) + (n + 0) + ∎ + + test₂ : ∀ m n → m ≡ n → suc (m + m) ≤ suc (suc (n + n)) + test₂ m n eq = + let open PR ≤-preorder in + begin + suc (m + m) + ≡⟨ cong! eq ⟩ + suc (n + n) + ∼⟨ ≤-step ≤-refl ⟩ + suc (suc (n + n)) + ∎ diff --git a/src/Reflection/AlphaEquality.agda b/src/Reflection/AlphaEquality.agda index 73d90a5a55..4360e31298 100644 --- a/src/Reflection/AlphaEquality.agda +++ b/src/Reflection/AlphaEquality.agda @@ -106,7 +106,7 @@ mutual (arg i a) =α=-ArgPattern (arg i′ a′) = a =α=-Pattern a′ _=α=-Term_ : Term → Term → Bool - (var x args) =α=-Term (var x′ args′) = (x ≡ᵇ x′) ∧ (args =α=-ArgsTerm args′) + (var x args) =α=-Term (var x′ args′) = (x ℕ.≡ᵇ x′) ∧ (args =α=-ArgsTerm args′) (con c args) =α=-Term (con c′ args′) = (c =α= c′) ∧ (args =α=-ArgsTerm args′) (def f args) =α=-Term (def f′ args′) = (f =α= f′) ∧ (args =α=-ArgsTerm args′) (meta x args) =α=-Term (meta x′ args′) = (x =α= x′) ∧ (args =α=-ArgsTerm args′) @@ -210,10 +210,10 @@ mutual _=α=-Sort_ : Sort → Sort → Bool (set t ) =α=-Sort (set t′ ) = t =α=-Term t′ - (lit n ) =α=-Sort (lit n′ ) = n ≡ᵇ n′ + (lit n ) =α=-Sort (lit n′ ) = n ℕ.≡ᵇ n′ (prop t ) =α=-Sort (prop t′ ) = t =α=-Term t′ - (propLit n) =α=-Sort (propLit n′) = n ≡ᵇ n′ - (inf n ) =α=-Sort (inf n′ ) = n ≡ᵇ n′ + (propLit n) =α=-Sort (propLit n′) = n ℕ.≡ᵇ n′ + (inf n ) =α=-Sort (inf n′ ) = n ℕ.≡ᵇ n′ (unknown ) =α=-Sort (unknown ) = true (set _ ) =α=-Sort (lit _ ) = false @@ -267,11 +267,11 @@ mutual _=α=-Pattern_ : Pattern → Pattern → Bool (con c ps) =α=-Pattern (con c′ ps′) = (c =α= c′) ∧ (ps =α=-ArgsPattern ps′) - (var x ) =α=-Pattern (var x′ ) = x ≡ᵇ x′ + (var x ) =α=-Pattern (var x′ ) = x ℕ.≡ᵇ x′ (lit l ) =α=-Pattern (lit l′ ) = l =α= l′ (proj a ) =α=-Pattern (proj a′ ) = a =α= a′ (dot t ) =α=-Pattern (dot t′ ) = t =α=-Term t′ - (absurd x) =α=-Pattern (absurd x′ ) = x ≡ᵇ x′ + (absurd x) =α=-Pattern (absurd x′ ) = x ℕ.≡ᵇ x′ (con x x₁) =α=-Pattern (dot x₂ ) = false (con x x₁) =α=-Pattern (var x₂ ) = false diff --git a/src/Reflection/Literal.agda b/src/Reflection/Literal.agda index 6d7cc492e2..4bd0915e47 100644 --- a/src/Reflection/Literal.agda +++ b/src/Reflection/Literal.agda @@ -8,6 +8,7 @@ module Reflection.Literal where +open import Data.Bool.Base as Bool using (Bool; true; false) import Data.Char as Char import Data.Float as Float import Data.Nat as ℕ @@ -102,3 +103,6 @@ meta x ≟ char x₁ = no (λ ()) meta x ≟ string x₁ = no (λ ()) meta x ≟ name x₁ = no (λ ()) meta x ≟ meta x₁ = Dec.map′ (cong meta) meta-injective (x Meta.≟ x₁) + +_≡ᵇ_ : Literal → Literal → Bool +l ≡ᵇ l′ = Dec.isYes (l ≟ l′) diff --git a/src/Reflection/Meta.agda b/src/Reflection/Meta.agda index 46fe960e29..f0ced0fed3 100644 --- a/src/Reflection/Meta.agda +++ b/src/Reflection/Meta.agda @@ -16,7 +16,7 @@ import Relation.Binary.Construct.On as On open import Relation.Binary.PropositionalEquality open import Agda.Builtin.Reflection public - using (Meta) renaming (primMetaToNat to toℕ) + using (Meta) renaming (primMetaToNat to toℕ; primMetaEquality to _≡ᵇ_) open import Agda.Builtin.Reflection.Properties public renaming (primMetaToNatInjective to toℕ-injective) diff --git a/src/Reflection/Name.agda b/src/Reflection/Name.agda index 26b579ea41..723ca0c619 100644 --- a/src/Reflection/Name.agda +++ b/src/Reflection/Name.agda @@ -21,7 +21,7 @@ open import Relation.Binary.PropositionalEquality -- Re-export built-ins open import Agda.Builtin.Reflection public - using (Name) renaming (primQNameToWord64s to toWords) + using (Name) renaming (primQNameToWord64s to toWords; primQNameEquality to _≡ᵇ_) open import Agda.Builtin.Reflection.Properties public renaming (primQNameToWord64sInjective to toWords-injective) diff --git a/src/Tactic/Rewrite.agda b/src/Tactic/Rewrite.agda new file mode 100644 index 0000000000..a2e64e74db --- /dev/null +++ b/src/Tactic/Rewrite.agda @@ -0,0 +1,222 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A simple tactic for used to automatically compute the function +-- argument to cong. +-- +-- The main use for this tactic is getting a similar experience to +-- 'rewrite' during equational reasoning. This allows us to write very +-- succinct proofs: +-- +-- example : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0) +-- example m n eq = begin +-- suc (suc (m + 0)) + m +-- ≡⟨ cong! (+-identityʳ m) ⟩ +-- suc (suc m) + m +-- ≡⟨ cong! eq ⟩ +-- suc (suc n) + n +-- ≡˘⟨ cong! (+-identityʳ n) ⟩ +-- suc (suc n) + (n + 0) +-- ∎ +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Tactic.Rewrite where + +open import Function using (_$_) + +open import Data.Bool.Base using (true; false; if_then_else_; _∧_) +open import Data.Char.Base as Char using (toℕ) +open import Data.Float.Base as Float using (_≡ᵇ_) +open import Data.List.Base as List using ([]; _∷_) +open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) +open import Data.Nat.Base as Nat using (ℕ; zero; suc; _≡ᵇ_; _+_) +open import Data.Unit.Base using (⊤) +open import Data.Word.Base as Word using (toℕ) +open import Data.Product + +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong) + +-- 'Data.String.Properties' defines this via 'Dec', so let's use the builtin +-- for maximum speed. +import Agda.Builtin.String as String renaming (primStringEquality to _≡ᵇ_) + +open import Reflection +open import Reflection.Abstraction +open import Reflection.AlphaEquality as Alpha +open import Reflection.Argument as Arg +open import Reflection.Argument.Information as ArgInfo +open import Reflection.Argument.Visibility as Visibility +open import Reflection.Literal as Literal +open import Reflection.Meta as Meta +open import Reflection.Name as Name +open import Reflection.Term as Term + +open import Reflection.TypeChecking.Monad.Syntax + +---------------------------------------------------------------------- +-- Utilities +---------------------------------------------------------------------- + +private + -- Descend past a variable. + varDescend : ℕ → ℕ → ℕ + varDescend ϕ x = if ϕ Nat.≤ᵇ x then suc x else x + + -- Descend a variable underneath pattern variables. + patternDescend : ℕ → Pattern → Pattern × ℕ + patternsDescend : ℕ → Args Pattern → Args Pattern × ℕ + + patternDescend ϕ (con c ps) = map₁ (con c) (patternsDescend ϕ ps) + patternDescend ϕ (dot t) = dot t , ϕ + patternDescend ϕ (var x) = var (varDescend ϕ x) , suc ϕ + patternDescend ϕ (lit l) = lit l , ϕ + patternDescend ϕ (proj f) = proj f , ϕ + patternDescend ϕ (absurd x) = absurd (varDescend ϕ x) , suc ϕ + + patternsDescend ϕ ((arg i p) ∷ ps) = + let (p' , ϕ') = patternDescend ϕ p + (ps' , ϕ'') = patternsDescend ϕ' ps + in (arg i p ∷ ps' , ϕ'') + patternsDescend ϕ [] = + [] , ϕ + + -- Construct an error when the goal is not 'x ≡ y' for some 'x' and 'y'. + notEqualityError : ∀ {A : Set} Term → TC A + notEqualityError goal = typeError (strErr "Cannot rewrite a goal that is not equality: " ∷ termErr goal ∷ []) + + record EqualityGoal : Set where + constructor equals + field + level : Term + type : Term + lhs : Term + rhs : Term + + destructEqualityGoal : Term → TC EqualityGoal + destructEqualityGoal goal@(def (quote _≡_) (lvl ∷ tp ∷ lhs ∷ rhs ∷ [])) = + return $ equals (unArg lvl) (unArg tp) (unArg lhs) (unArg rhs) + destructEqualityGoal (meta m args) = + blockOnMeta m + destructEqualityGoal goal = + notEqualityError goal + + -- Helper for constructing applications of 'cong' + `cong : ∀ {a} {A : Set a} {x y : A} → EqualityGoal → Term → x ≡ y → TC Term + `cong {a = a} {A = A} {x = x} {y = y} eqGoal f x≡y = do + -- NOTE: We apply all implicit arguments here to ensure that using + -- equality proofs with implicits don't lead to unsolved metavariable + -- errors. + let open EqualityGoal eqGoal + eq ← quoteTC x≡y + `a ← quoteTC a + `A ← quoteTC A + `x ← quoteTC x + `y ← quoteTC y + return $ def (quote cong) $ `a ⟅∷⟆ `A ⟅∷⟆ level ⟅∷⟆ type ⟅∷⟆ vLam "ϕ" f ⟨∷⟩ `x ⟅∷⟆ `y ⟅∷⟆ eq ⟨∷⟩ [] + +---------------------------------------------------------------------- +-- Anti-Unification +-- +-- The core idea of the tactic is that we can compute the input +-- to 'cong' by syntactically anti-unifying both sides of the +-- equality, and then using that to construct a lambda +-- where all the differences are replaced by the lambda-abstracted +-- variable. +-- +-- For instance, the two terms 'suc (m + (m + 0)) + (m + 0)' and +-- 'suc (m + m) + (m + 0)' would anti unify to 'suc (m + _) + (m + 0)' +-- which we can then use to construct the lambda 'λ ϕ → suc (m + ϕ) + (m + 0)'. +---------------------------------------------------------------------- + +private + antiUnify : ℕ → Term → Term → Term + antiUnifyArgs : ℕ → Args Term → Args Term → Maybe (Args Term) + antiUnifyClauses : ℕ → Clauses → Clauses → Maybe Clauses + antiUnifyClause : ℕ → Clause → Clause → Maybe Clause + + antiUnify ϕ (var x args) (var y args') with x Nat.≡ᵇ y | antiUnifyArgs ϕ args args' + ... | _ | nothing = var ϕ [] + ... | false | just uargs = var ϕ uargs + ... | true | just uargs = var (varDescend ϕ x) uargs + antiUnify ϕ (con c args) (con c' args') with c Name.≡ᵇ c' | antiUnifyArgs ϕ args args' + ... | _ | nothing = var ϕ [] + ... | false | just uargs = var ϕ [] + ... | true | just uargs = con c uargs + antiUnify ϕ (def f args) (def f' args') with f Name.≡ᵇ f' | antiUnifyArgs ϕ args args' + ... | _ | nothing = var ϕ [] + ... | false | just uargs = var ϕ [] + ... | true | just uargs = def f uargs + antiUnify ϕ (lam v (abs s t)) (lam _ (abs _ t')) = + lam v (abs s (antiUnify (suc ϕ) t t')) + antiUnify ϕ (pat-lam cs args) (pat-lam cs' args') with antiUnifyClauses ϕ cs cs' | antiUnifyArgs ϕ args args' + ... | nothing | _ = var ϕ [] + ... | _ | nothing = var ϕ [] + ... | just ucs | just uargs = pat-lam ucs uargs + antiUnify ϕ (Π[ s ∶ arg i a ] b) (Π[ _ ∶ arg _ a' ] b') = + Π[ s ∶ arg i (antiUnify ϕ a a') ] antiUnify (suc ϕ) b b' + antiUnify ϕ (sort (set t)) (sort (set t')) = + sort (set (antiUnify ϕ t t')) + antiUnify ϕ (sort (lit n)) (sort (lit n')) with n Nat.≡ᵇ n' + ... | true = sort (lit n) + ... | false = var ϕ [] + antiUnify ϕ (sort (propLit n)) (sort (propLit n')) with n Nat.≡ᵇ n' + ... | true = sort (propLit n) + ... | false = var ϕ [] + antiUnify ϕ (sort (inf n)) (sort (inf n')) with n Nat.≡ᵇ n' + ... | true = sort (inf n) + ... | false = var ϕ [] + antiUnify ϕ (sort unknown) (sort unknown) = + sort unknown + antiUnify ϕ (lit l) (lit l') with l Literal.≡ᵇ l' + ... | true = lit l + ... | false = var ϕ [] + antiUnify ϕ (meta x args) (meta x' args') with x Meta.≡ᵇ x' | antiUnifyArgs ϕ args args' + ... | _ | nothing = var ϕ [] + ... | false | _ = var ϕ [] + ... | true | just uargs = meta x uargs + antiUnify ϕ unknown unknown = unknown + antiUnify ϕ _ _ = var ϕ [] + + antiUnifyArgs ϕ (arg i t ∷ args) (arg _ t' ∷ args') = + Maybe.map (arg i (antiUnify ϕ t t') ∷_) (antiUnifyArgs ϕ args args') + antiUnifyArgs ϕ [] [] = + just [] + antiUnifyArgs ϕ _ _ = + nothing + + antiUnifyClause ϕ (clause Γ pats t) (clause Δ pats' t') = + Maybe.when ((Γ =α= Δ) ∧ (pats =α= pats')) + let (upats , ϕ') = patternsDescend ϕ pats + in clause Γ upats (antiUnify ϕ' t t') + antiUnifyClause ϕ (absurd-clause Γ pats) (absurd-clause Δ pats') = + Maybe.when ((Γ =α= Δ) ∧ (pats =α= pats')) $ + absurd-clause Γ pats + antiUnifyClause ϕ _ _ = + nothing + + antiUnifyClauses ϕ (c ∷ cs) (c' ∷ cs') = + Maybe.ap (Maybe.map _∷_ (antiUnifyClause ϕ c c')) (antiUnifyClauses ϕ cs cs') + antiUnifyClauses ϕ _ _ = + just [] + + +---------------------------------------------------------------------- +-- Rewriting +---------------------------------------------------------------------- + +macro + cong! : ∀ {a} {A : Set a} {x y : A} → x ≡ y → Term → TC ⊤ + cong! x≡y hole = + -- NOTE: We avoid doing normalisation here as this tactic + -- is mainly meant for equational reasoning. In that context, + -- the endpoints of the equality are already specified in + -- the form that the -- programmer expects them to be in, + -- so normalising buys us nothing. + withNormalisation false $ do + goal ← inferType hole + eqGoal ← destructEqualityGoal goal + let cong-lam = antiUnify 0 (EqualityGoal.lhs eqGoal) (EqualityGoal.rhs eqGoal) + cong-tm ← `cong eqGoal cong-lam x≡y + unify cong-tm hole