------------------------------------------------------------------------
-- 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)
-- ∎
--
-- Please see README.Tactic.Cong for more details.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Tactic.Cong where
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 ℕ using (ℕ; zero; suc; _≡ᵇ_; _+_)
open import Data.Unit.Base using (⊤)
open import Data.Word64.Base as Word64 using (toℕ)
open import Data.Product.Base using (_×_; map₁; _,_)
open import Function.Base using (_$_; flip; case_of_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
open import Relation.Nullary.Decidable.Core using (yes; no)
-- '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.AST.Abstraction
open import Reflection.AST.AlphaEquality as Alpha
open import Reflection.AST.Argument as Arg
open import Reflection.AST.Argument.Information as ArgInfo
open import Reflection.AST.Argument.Visibility as Visibility
open import Reflection.AST.Literal as Literal
open import Reflection.AST.Meta as Meta
open import Reflection.AST.Name as Name
open import Reflection.AST.Term as Term
import Reflection.AST.Traversal as Traversal
open import Reflection.TCM.Syntax
open import Reflection.TCM.Utilities
-- Marker to keep anti-unification from descending into the wrapped
-- subterm.
--
-- For instance, anti-unification of ⌞ a + b ⌟ + c and b + a + c
-- yields λ ϕ → ϕ + c, as opposed to λ ϕ → ϕ + ϕ + c without ⌞_⌟.
--
-- The marker is only visible to the cong! tactic, which inhibits
-- normalisation. Anywhere else, ⌞ a + b ⌟ reduces to a + b.
--
-- Thus, proving ⌞ a + b ⌟ + c ≡ b + a + c via cong! (+-comm a b)
-- also proves a + b + c ≡ b + a + c.
⌞_⌟ : ∀ {a} {A : Set a} → A → A
⌞_⌟ x = x
------------------------------------------------------------------------
-- Utilities
------------------------------------------------------------------------
private
-- Descend past a variable.
varDescend : ℕ → ℕ → ℕ
varDescend ϕ x = if ϕ ℕ.≤ᵇ 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 ∷ [])
unificationError : ∀ {A : Set} → TC Term → TC Term → TC A
unificationError term symTerm = do
term' ← term
symTerm' ← symTerm
-- Don't show the same term twice.
let symErr = case term' Term.≟ symTerm' of λ where
(yes _) → []
(no _) → strErr "\n" ∷ termErr symTerm' ∷ []
typeError (strErr "cong! failed, tried:\n" ∷ termErr term' ∷ symErr)
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 ∷ [])) =
pure $ 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
pure $ 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
pattern apply-⌞⌟ t = (def (quote ⌞_⌟) (_ ∷ _ ∷ arg _ t ∷ []))
antiUnify ϕ (var x args) (var y args') with x ℕ.≡ᵇ 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) (apply-⌞⌟ t) = antiUnify ϕ (def f args) t
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 ℕ.≡ᵇ n'
... | true = sort (lit n)
... | false = var ϕ []
antiUnify ϕ (sort (propLit n)) (sort (propLit n')) with n ℕ.≡ᵇ n'
... | true = sort (propLit n)
... | false = var ϕ []
antiUnify ϕ (sort (inf n)) (sort (inf n')) with n ℕ.≡ᵇ 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 makeTerm = λ lhs rhs → `cong eqGoal (antiUnify 0 lhs rhs) x≡y
let lhs = EqualityGoal.lhs eqGoal
let rhs = EqualityGoal.rhs eqGoal
let term = makeTerm lhs rhs
let symTerm = makeTerm rhs lhs
let uni = _>>= flip unify hole
-- When using ⌞_⌟ with ≡⟨ ... ⟨, (uni term) fails and
-- (uni symTerm) succeeds.
catchTC (uni term) $
catchTC (uni symTerm) $ do
-- If we failed because of unresolved metas, restart.
blockOnMetas goal
-- If we failed for a different reason, show an error.
unificationError term symTerm
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4