Rewriting Tactic

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

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))
+    ∎

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

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′)

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)

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)