From 803ccb0ffe3742a0ee340366502d07671f2821cf Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Sat, 14 May 2022 12:29:05 +0200 Subject: [PATCH 1/6] Move lambda prepending functions (#1116) --- src/Reflection/AST/DeBruijn.agda | 14 +++++++++++++- src/Reflection/AST/Term.agda | 9 --------- src/Tactic/RingSolver.agda | 1 + 3 files changed, 14 insertions(+), 10 deletions(-) diff --git a/src/Reflection/AST/DeBruijn.agda b/src/Reflection/AST/DeBruijn.agda index 174abe2874..c2dba6c03f 100644 --- a/src/Reflection/AST/DeBruijn.agda +++ b/src/Reflection/AST/DeBruijn.agda @@ -10,7 +10,9 @@ module Reflection.AST.DeBruijn where open import Data.Bool.Base using (Bool; true; false; _∨_; if_then_else_) open import Data.Nat.Base as Nat using (ℕ; zero; suc; _+_; _∸_; _<ᵇ_; _≡ᵇ_) -open import Data.List.Base using (List; []; _∷_; _++_) +open import Data.List.Base using (List; []; _∷_; _++_; foldr; reverse; map) +open import Data.Product using (_×_; _,_) +open import Data.String as String using (String) open import Data.Maybe.Base using (Maybe; nothing; just) import Data.Maybe.Effectful as Maybe import Function.Identity.Effectful as Identity @@ -53,6 +55,16 @@ module _ where weakenClauses : (by : ℕ) → Clauses → Clauses weakenClauses = weakenFrom′ traverseClauses 0 +-- Apply Weakening to substitute under lambdas + +prependLams : List (String × Visibility) → Term → Term +prependLams xs t = foldr (λ {(s , v) t → lam v (abs s t)}) t (reverse xs) + +prependHLams : List String → Term → Term +prependHLams vs = prependLams (map (_, hidden) vs) + +prependVLams : List String → Term → Term +prependVLams vs = prependLams (map (_, visible) vs) ------------------------------------------------------------------------ -- η-expansion diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda index ddb02b4afe..a740117727 100644 --- a/src/Reflection/AST/Term.agda +++ b/src/Reflection/AST/Term.agda @@ -96,15 +96,6 @@ stripPis : Term → List (String × Arg Type) × Term stripPis (Π[ s ∶ t ] x) = map₁ ((s , t) ∷_) (stripPis x) stripPis x = [] , x -prependLams : List (String × Visibility) → Term → Term -prependLams xs t = foldr (λ {(s , v) t → lam v (abs s t)}) t (reverse xs) - -prependHLams : List String → Term → Term -prependHLams vs = prependLams (List.map (_, hidden) vs) - -prependVLams : List String → Term → Term -prependVLams vs = prependLams (List.map (_, visible) vs) - ------------------------------------------------------------------------ -- Decidable equality diff --git a/src/Tactic/RingSolver.agda b/src/Tactic/RingSolver.agda index c79abc8174..3811b04fcd 100644 --- a/src/Tactic/RingSolver.agda +++ b/src/Tactic/RingSolver.agda @@ -27,6 +27,7 @@ open import Reflection.AST.Argument open import Reflection.AST.Term as Term open import Reflection.AST.AlphaEquality open import Reflection.AST.Name as Name +open import Reflection.AST.DeBruijn using (prependVLams; prependHLams) open import Reflection.TCM.Syntax open import Data.Nat.Reflection open import Data.List.Reflection From 1f9d5894bdc74f0da4f4eae80ad31bc4caf97e2d Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 21 Jul 2022 10:22:38 +0200 Subject: [PATCH 2/6] fix broken reference in comment --- src/Data/Integer/Tactic/RingSolver.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Integer/Tactic/RingSolver.agda b/src/Data/Integer/Tactic/RingSolver.agda index ea4a00403f..500fd394ef 100644 --- a/src/Data/Integer/Tactic/RingSolver.agda +++ b/src/Data/Integer/Tactic/RingSolver.agda @@ -4,7 +4,7 @@ -- Automatic solvers for equations over integers ------------------------------------------------------------------------ --- See README.Integer for examples of how to use this solver +-- See README.Data.Integer for examples of how to use this solver {-# OPTIONS --without-K --safe #-} From 997abe2b7a73206be23da0d8fbe6b3476d6777ef Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 21 Jul 2022 11:16:14 +0200 Subject: [PATCH 3/6] example solver applications --- src/Tactic/RingSolver/Examples.agda | 58 +++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 src/Tactic/RingSolver/Examples.agda diff --git a/src/Tactic/RingSolver/Examples.agda b/src/Tactic/RingSolver/Examples.agda new file mode 100644 index 0000000000..8fa0563d26 --- /dev/null +++ b/src/Tactic/RingSolver/Examples.agda @@ -0,0 +1,58 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some simple use cases of the ring solver +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Tactic.RingSolver.Examples where + +open import Algebra + +open import Data.Integer.Base using (ℤ) +open import Data.Integer.Properties +open import Data.Maybe + +open import Agda.Builtin.Equality using (_≡_ ; refl) + +open import Tactic.RingSolver +open import Tactic.RingSolver.Core.AlmostCommutativeRing + + +module IntegerExamples where + ℤAsCRing : CommutativeRing _ _ + ℤAsCRing = record + { Carrier = ℤ + ; _≈_ = _ + ; _+_ = _ + ; _*_ = _ + ; -_ = _ + ; 0# = _ + ; 1# = _ + ; isCommutativeRing = +-*-isCommutativeRing + } + + ℤAsAlmostCRing : _ + ℤAsAlmostCRing = fromCommutativeRing ℤAsCRing (λ _ → nothing) + open AlmostCommutativeRing ℤAsAlmostCRing + + works : ∀ x y → x + y ≡ y + x + works = solve-∀ ℤAsAlmostCRing + + {- + nope : ∀ x y → (x + y) * (x - y) ≡ (x * x) - (y * y) + nope = solve-∀ ℤAsAlmostCRing + -} + +module GenericExamples {r s} (R : CommutativeRing r s) where + RAsAlmostCRing = fromCommutativeRing R (λ _ → nothing) + open AlmostCommutativeRing RAsAlmostCRing + + works : ∀ x y → x + y ≈ y + x + works = solve-∀ RAsAlmostCRing + + {- + nope : ∀ x y → (x + y) * (x - y) ≡ (x * x) - (y * y) + nope = solve-∀ RAsAlmostCRing + -} From 18a46d3c6a74285195b69d88546585f19bdd5063 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 21 Jul 2022 11:32:44 +0200 Subject: [PATCH 4/6] de bruijn index problem --- src/Tactic/RingSolver/Examples.agda | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/Tactic/RingSolver/Examples.agda b/src/Tactic/RingSolver/Examples.agda index 8fa0563d26..92dcd717ba 100644 --- a/src/Tactic/RingSolver/Examples.agda +++ b/src/Tactic/RingSolver/Examples.agda @@ -56,3 +56,16 @@ module GenericExamples {r s} (R : CommutativeRing r s) where nope : ∀ x y → (x + y) * (x - y) ≡ (x * x) - (y * y) nope = solve-∀ RAsAlmostCRing -} + +module SolverCanOnlyUseNames {r s} (R : CommutativeRing r s) where + RAsAlmostCRing = fromCommutativeRing R (λ _ → nothing) + open AlmostCommutativeRing RAsAlmostCRing + + {- + nope : ∀ x y → x + y ≈ y + x + nope = solve-∀ (fromCommutativeRing R (λ _ → nothing)) + -} + + {- + to make this work, one has to lift deBruijn indices in the expression defining the ring + -} From 7d79ab154c8d88da467e0a0057562af68eaf4eb1 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Sun, 24 Jul 2022 09:45:50 +0200 Subject: [PATCH 5/6] Use suggestion: Remove solvable fields from record construction Co-authored-by: G. Allais --- src/Tactic/RingSolver/Examples.agda | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/Tactic/RingSolver/Examples.agda b/src/Tactic/RingSolver/Examples.agda index 92dcd717ba..0efd8f1a01 100644 --- a/src/Tactic/RingSolver/Examples.agda +++ b/src/Tactic/RingSolver/Examples.agda @@ -24,12 +24,6 @@ module IntegerExamples where ℤAsCRing : CommutativeRing _ _ ℤAsCRing = record { Carrier = ℤ - ; _≈_ = _ - ; _+_ = _ - ; _*_ = _ - ; -_ = _ - ; 0# = _ - ; 1# = _ ; isCommutativeRing = +-*-isCommutativeRing } From 8f0b3a8d64c250d0cb6000388c73acb2b89c86d3 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Sun, 24 Jul 2022 09:50:15 +0200 Subject: [PATCH 6/6] Use suggestion: Remove pattern lambda --- src/Reflection/AST/DeBruijn.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Reflection/AST/DeBruijn.agda b/src/Reflection/AST/DeBruijn.agda index c2dba6c03f..31e9b00931 100644 --- a/src/Reflection/AST/DeBruijn.agda +++ b/src/Reflection/AST/DeBruijn.agda @@ -58,7 +58,7 @@ module _ where -- Apply Weakening to substitute under lambdas prependLams : List (String × Visibility) → Term → Term -prependLams xs t = foldr (λ {(s , v) t → lam v (abs s t)}) t (reverse xs) +prependLams xs t = foldr (λ (s , v) t → lam v (abs s t)) t (reverse xs) prependHLams : List String → Term → Term prependHLams vs = prependLams (map (_, hidden) vs)