From caf975a91dd209d680b4d204110aac6d40ceea98 Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Wed, 3 Jun 2026 10:32:05 +0100 Subject: [PATCH] Add `firstorder` tactic --- Tactic.agda | 4 + Tactic/FirstOrder/Core.agda | 189 +++++++++++++++ Tactic/FirstOrder/Decide.agda | 300 +++++++++++++++++++++++ Tactic/FirstOrder/Search.agda | 113 +++++++++ Tactic/Solver/FirstOrder.agda | 289 ++++++++++++++++++++++ Tactic/Solver/FirstOrder/Tests.agda | 361 ++++++++++++++++++++++++++++ 6 files changed, 1256 insertions(+) create mode 100644 Tactic/FirstOrder/Core.agda create mode 100644 Tactic/FirstOrder/Decide.agda create mode 100644 Tactic/FirstOrder/Search.agda create mode 100644 Tactic/Solver/FirstOrder.agda create mode 100644 Tactic/Solver/FirstOrder/Tests.agda diff --git a/Tactic.agda b/Tactic.agda index 9d2c8f9..fa2f2ed 100644 --- a/Tactic.agda +++ b/Tactic.agda @@ -25,3 +25,7 @@ open import Tactic.Derive.Convertible public open import Tactic.Solver.Ring open import Tactic.Solver.Ring.Tests + +open import Tactic.Solver.FirstOrder +open import Tactic.Solver.FirstOrder.Tests +import Tactic.FirstOrder.Decide diff --git a/Tactic/FirstOrder/Core.agda b/Tactic/FirstOrder/Core.agda new file mode 100644 index 0000000..dfb24d2 --- /dev/null +++ b/Tactic/FirstOrder/Core.agda @@ -0,0 +1,189 @@ +{-# OPTIONS --safe --without-K #-} +-------------------------------------------------------------------------------- +-- First-order solver, propositional core: +-- * a deep embedding of (intuitionistic) propositional formulas, +-- * their denotation into Agda `Set`s, +-- * the contraction-free sequent calculus G4ip (Dyckhoff's LJT) as the +-- certificate calculus, and +-- * soundness: a derivation interprets into an inhabitant of the denotation. +-- +-- G4ip is chosen because its shape-split implication-left rules make proof +-- search terminating and complete for intuitionistic propositional logic: every +-- left rule *deletes* its principal formula (`Γ ∖ i`), so nothing is ever +-- reprocessed. Search (which produces derivations) is still not part of the +-- trusted base: it only has to return a `Γ ⊢ φ`, which `soundness` turns into a +-- real proof. Bugs in search show up as failure, never as unsoundness. +-------------------------------------------------------------------------------- + +module Tactic.FirstOrder.Core where + +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Fin using (Fin; zero; suc) +open import Data.List using (List; []; _∷_) +open import Data.List.Membership.Propositional using (_∈_) +open import Data.List.Relation.Unary.Any using (here; there) +open import Data.Nat using (ℕ; suc) +open import Data.Product using (_×_; _,_; proj₁; proj₂) +open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]) +open import Data.Unit using (⊤; tt) +open import Level using (Level; 0ℓ; _⊔_; Setω) +open import Relation.Binary.PropositionalEquality using (refl) + +private + variable + n : ℕ + λs : Fin n → Level + +-------------------------------------------------------------------------------- +-- Syntax +-- +-- `n` is the number of distinct atomic propositions; the reifier will collect +-- the atoms occurring in a goal into an environment and index them by `Fin n`. +-------------------------------------------------------------------------------- + +infixr 7 _∧′_ +infixr 6 _∨′_ +infixr 5 _⇒′_ +infix 8 ¬′_ + +data Formula (n : ℕ) : Set where + atom : Fin n → Formula n + ⊤′ ⊥′ : Formula n + _∧′_ _∨′_ _⇒′_ : Formula n → Formula n → Formula n + +¬′_ : Formula n → Formula n +¬′ φ = φ ⇒′ ⊥′ + +-------------------------------------------------------------------------------- +-- Denotation +-- +-- Each atom may live at its own level: an environment assigns levels `λs i` to +-- the atoms and types `ρ i : Set (λs i)`. A formula's denotation then sits at +-- the join `levels φ λs` of the levels it mentions (with `⊤′`/`⊥′` the genuine +-- `Set₀` units, not lifted copies — so monomorphic `⊤`/`⊥`/`¬_` goals are +-- matched exactly). This is the most permissive scheme: a goal may freely mix +-- hypotheses at different levels. +-- +-- The environment is an `Env`: a cons-list whose index *constructs* `λs` via +-- `_◂_`. That is what lets the reflection macro emit a flat `A ∷ … ∷ []` and +-- have `n`, `λs` and `ρ = lookupᴱ` all inferred, sidestepping both the `Setω` +-- function type and higher-order unification of `λs`. +-------------------------------------------------------------------------------- + +infixr 5 _◂_ _∷_ + +_◂_ : Level → (Fin n → Level) → (Fin (suc n) → Level) +(ℓ ◂ λs) zero = ℓ +(ℓ ◂ λs) (suc i) = λs i + +data Env : (n : ℕ) → (Fin n → Level) → Setω where + [] : Env 0 (λ ()) + _∷_ : ∀ {ℓ n} {λs : Fin n → Level} → Set ℓ → Env n λs → Env (suc n) (ℓ ◂ λs) + +lookupᴱ : Env n λs → (i : Fin n) → Set (λs i) +lookupᴱ (A ∷ _) zero = A +lookupᴱ (_ ∷ as) (suc i) = lookupᴱ as i + +levels : Formula n → (Fin n → Level) → Level +levels (atom i) λs = λs i +levels ⊤′ λs = 0ℓ +levels ⊥′ λs = 0ℓ +levels (φ ∧′ ψ) λs = levels φ λs ⊔ levels ψ λs +levels (φ ∨′ ψ) λs = levels φ λs ⊔ levels ψ λs +levels (φ ⇒′ ψ) λs = levels φ λs ⊔ levels ψ λs + +⟦_⟧ : (φ : Formula n) (λs : Fin n → Level) → ((i : Fin n) → Set (λs i)) → Set (levels φ λs) +⟦ atom i ⟧ λs ρ = ρ i +⟦ ⊤′ ⟧ λs ρ = ⊤ +⟦ ⊥′ ⟧ λs ρ = ⊥ +⟦ φ ∧′ ψ ⟧ λs ρ = ⟦ φ ⟧ λs ρ × ⟦ ψ ⟧ λs ρ +⟦ φ ∨′ ψ ⟧ λs ρ = ⟦ φ ⟧ λs ρ ⊎ ⟦ ψ ⟧ λs ρ +⟦ φ ⇒′ ψ ⟧ λs ρ = ⟦ φ ⟧ λs ρ → ⟦ ψ ⟧ λs ρ + +levelsᶜ : List (Formula n) → (Fin n → Level) → Level +levelsᶜ [] λs = 0ℓ +levelsᶜ (φ ∷ Γ) λs = levels φ λs ⊔ levelsᶜ Γ λs + +⟦_⟧ᶜ : (Γ : List (Formula n)) (λs : Fin n → Level) → ((i : Fin n) → Set (λs i)) → Set (levelsᶜ Γ λs) +⟦ [] ⟧ᶜ λs ρ = ⊤ +⟦ φ ∷ Γ ⟧ᶜ λs ρ = ⟦ φ ⟧ λs ρ × ⟦ Γ ⟧ᶜ λs ρ + +-------------------------------------------------------------------------------- +-- Context deletion: remove the hypothesis pointed at by a membership proof. +-- Used by the left rules to discard their principal formula. +-------------------------------------------------------------------------------- + +infixl 5 _∖_ +_∖_ : (Γ : List (Formula n)) {φ : Formula n} → φ ∈ Γ → List (Formula n) +(_ ∷ Γ) ∖ here _ = Γ +(x ∷ Γ) ∖ there i = x ∷ (Γ ∖ i) + +-------------------------------------------------------------------------------- +-- Certificate calculus: Dyckhoff's contraction-free sequent calculus G4ip. +-------------------------------------------------------------------------------- + +infix 2 _⊢_ + +data _⊢_ {n} : List (Formula n) → Formula n → Set where + -- axioms + init : ∀ {Γ k} → atom k ∈ Γ → Γ ⊢ atom k + ⊤R : ∀ {Γ} → Γ ⊢ ⊤′ + ⊥L : ∀ {Γ G} → ⊥′ ∈ Γ → Γ ⊢ G + -- right rules + ∧R : ∀ {Γ A B} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧′ B + ∨R₁ : ∀ {Γ A B} → Γ ⊢ A → Γ ⊢ A ∨′ B + ∨R₂ : ∀ {Γ A B} → Γ ⊢ B → Γ ⊢ A ∨′ B + ⊃R : ∀ {Γ A B} → A ∷ Γ ⊢ B → Γ ⊢ A ⇒′ B + -- invertible left rules + ∧L : ∀ {Γ A B G} → (i : A ∧′ B ∈ Γ) → A ∷ B ∷ (Γ ∖ i) ⊢ G → Γ ⊢ G + ∨L : ∀ {Γ A B G} → (i : A ∨′ B ∈ Γ) → A ∷ (Γ ∖ i) ⊢ G → B ∷ (Γ ∖ i) ⊢ G → Γ ⊢ G + -- implication-left, split by the shape of the antecedent + ⊃L⊤ : ∀ {Γ B G} → (i : ⊤′ ⇒′ B ∈ Γ) → B ∷ (Γ ∖ i) ⊢ G → Γ ⊢ G + ⊃L⊥ : ∀ {Γ B G} → (i : ⊥′ ⇒′ B ∈ Γ) → (Γ ∖ i) ⊢ G → Γ ⊢ G + ⊃Lat : ∀ {Γ k B G} → (i : atom k ⇒′ B ∈ Γ) → atom k ∈ (Γ ∖ i) → B ∷ (Γ ∖ i) ⊢ G → Γ ⊢ G + ⊃L∧ : ∀ {Γ C D B G} → (i : (C ∧′ D) ⇒′ B ∈ Γ) → (C ⇒′ (D ⇒′ B)) ∷ (Γ ∖ i) ⊢ G → Γ ⊢ G + ⊃L∨ : ∀ {Γ C D B G} → (i : (C ∨′ D) ⇒′ B ∈ Γ) → (C ⇒′ B) ∷ (D ⇒′ B) ∷ (Γ ∖ i) ⊢ G → Γ ⊢ G + ⊃L⊃ : ∀ {Γ C D B G} → (i : (C ⇒′ D) ⇒′ B ∈ Γ) + → (D ⇒′ B) ∷ (Γ ∖ i) ⊢ C ⇒′ D → B ∷ (Γ ∖ i) ⊢ G → Γ ⊢ G + +-------------------------------------------------------------------------------- +-- Soundness: interpret a derivation into an inhabitant of the denotation. +-- This is the entire trusted base of the solver. +-------------------------------------------------------------------------------- + +private + ρ-syntax : (λs : Fin n → Level) → Setω + ρ-syntax {n} λs = (i : Fin n) → Set (λs i) + +look : ∀ {φ Γ} (ρ : ρ-syntax λs) → φ ∈ Γ → ⟦ Γ ⟧ᶜ λs ρ → ⟦ φ ⟧ λs ρ +look ρ (here refl) (x , _) = x +look ρ (there i) (_ , γ) = look ρ i γ + +drop : ∀ {φ Γ} (ρ : ρ-syntax λs) (i : φ ∈ Γ) → ⟦ Γ ⟧ᶜ λs ρ → ⟦ Γ ∖ i ⟧ᶜ λs ρ +drop ρ (here refl) (_ , γ) = γ +drop ρ (there i) (x , γ) = x , drop ρ i γ + +soundness : ∀ {Γ G} (ρ : ρ-syntax λs) → Γ ⊢ G → ⟦ Γ ⟧ᶜ λs ρ → ⟦ G ⟧ λs ρ +soundness ρ (init i) γ = look ρ i γ +soundness ρ ⊤R γ = tt +soundness ρ (⊥L i) γ = ⊥-elim (look ρ i γ) +soundness ρ (∧R d e) γ = soundness ρ d γ , soundness ρ e γ +soundness ρ (∨R₁ d) γ = inj₁ (soundness ρ d γ) +soundness ρ (∨R₂ d) γ = inj₂ (soundness ρ d γ) +soundness ρ (⊃R d) γ = λ a → soundness ρ d (a , γ) +soundness ρ (∧L i d) γ = soundness ρ d (proj₁ (look ρ i γ) , proj₂ (look ρ i γ) , drop ρ i γ) +soundness ρ (∨L i d e) γ = [ (λ a → soundness ρ d (a , drop ρ i γ)) + , (λ b → soundness ρ e (b , drop ρ i γ)) ] (look ρ i γ) +soundness ρ (⊃L⊤ i d) γ = soundness ρ d (look ρ i γ tt , drop ρ i γ) +soundness ρ (⊃L⊥ i d) γ = soundness ρ d (drop ρ i γ) +soundness ρ (⊃Lat i j d) γ = soundness ρ d (look ρ i γ (look ρ j (drop ρ i γ)) , drop ρ i γ) +soundness ρ (⊃L∧ i d) γ = soundness ρ d ((λ c e → look ρ i γ (c , e)) , drop ρ i γ) +soundness ρ (⊃L∨ i d) γ = soundness ρ d ( (λ c → look ρ i γ (inj₁ c)) + , (λ e → look ρ i γ (inj₂ e)) + , drop ρ i γ) +soundness ρ (⊃L⊃ i d e) γ = + soundness ρ e (look ρ i γ (soundness ρ d ((λ z → look ρ i γ (λ _ → z)) , drop ρ i γ)) , drop ρ i γ) + +-- specialised to the empty context: the entry point the reflection macro uses +solve : ∀ {φ} (ρ : ρ-syntax λs) → [] ⊢ φ → ⟦ φ ⟧ λs ρ +solve ρ p = soundness ρ p tt diff --git a/Tactic/FirstOrder/Decide.agda b/Tactic/FirstOrder/Decide.agda new file mode 100644 index 0000000..1524ee4 --- /dev/null +++ b/Tactic/FirstOrder/Decide.agda @@ -0,0 +1,300 @@ +{-# OPTIONS --safe --without-K #-} +-------------------------------------------------------------------------------- +-- A fuel-free, provably-terminating G4ip proof search. +-- +-- The fuel-bounded `Tactic.FirstOrder.Search.search` is complete only when the +-- fuel exceeds the proof-search depth. Here we remove the fuel by recursing on +-- a well-founded measure: Dyckhoff's termination argument, encoded as a single +-- natural number. +-- +-- The trick: weight formulas with `w (A ⇒ B) = w A + w B` (no `+1`), and take +-- μ (Γ ⊢ G) = Σ_{A ∈ Γ} 3 ^ (w A) + 3 ^ (w G). +-- Every G4ip rule replaces its principal formula (weight k) by at most two +-- formulas of weight < k, and `2 · 3^(k-1) < 3^k`, so μ strictly decreases on +-- every premise. Ordinary `<`-well-foundedness then justifies the recursion. +-- +-- This module proves only termination; what it returns is still a `Γ ⊢ φ` +-- certificate (sound via `Core.soundness`). PART 1 below builds the measure and +-- the arithmetic; PART 2 (the search) consumes it. +-------------------------------------------------------------------------------- + +module Tactic.FirstOrder.Decide where + +open import Data.List using (List; []; _∷_; foldr) +open import Data.List.Membership.Propositional using (_∈_) +open import Data.List.Relation.Unary.Any using (here; there) +open import Data.Maybe using (Maybe; just; nothing; map; _<∣>_) +open import Data.Nat +open import Data.Nat.Induction using (<-wellFounded) +open import Data.Nat.Properties +open import Data.Nat.Solver using (module +-*-Solver) +open import Function using (case_of_) +open import Induction.WellFounded using (Acc; acc) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; cong; sym; trans; subst; subst₂) + +open +-*-Solver + +open import Tactic.FirstOrder.Core hiding (solve) +open import Tactic.FirstOrder.Search using (find; search) + +private + variable + n : ℕ + +-------------------------------------------------------------------------------- +-- PART 1 — the measure +-------------------------------------------------------------------------------- + +-- Dyckhoff weight: note the absent `+1` on implication. +w : Formula n → ℕ +w (atom _) = 1 +w ⊤′ = 1 +w ⊥′ = 1 +w (A ∧′ B) = w A + w B + 1 +w (A ∨′ B) = w A + w B + 1 +w (A ⇒′ B) = w A + w B + +f : Formula n → ℕ +f A = 3 ^ w A + +Σf : List (Formula n) → ℕ +Σf Γ = foldr (λ A → f A +_) 0 Γ + +μ : List (Formula n) → Formula n → ℕ +μ Γ G = Σf Γ + f G + +-------------------------------------------------------------------------------- +-- Deleting a hypothesis removes its weight from the sum. +-------------------------------------------------------------------------------- + +Σf-∖ : ∀ {X : Formula n} {Γ} (i : X ∈ Γ) → Σf Γ ≡ f X + Σf (Γ ∖ i) +Σf-∖ (here refl) = refl +Σf-∖ {X = X} (there {x = y} {xs = Γ} i) = + trans (cong (f y +_) (Σf-∖ i)) + (trans (sym (+-assoc (f y) (f X) (Σf (Γ ∖ i)))) + (trans (cong (_+ Σf (Γ ∖ i)) (+-comm (f y) (f X))) + (+-assoc (f X) (f y) (Σf (Γ ∖ i))))) + +-------------------------------------------------------------------------------- +-- Two arithmetic facts everything reduces to. +-------------------------------------------------------------------------------- + +1<3 : 1 < 3 +1<3 = s≤s (s≤s z≤n) + +-- strict monotonicity of 3 ^_ +one< : ∀ {a b} → a < b → 3 ^ a < 3 ^ b +one< = ^-monoʳ-< 3 1<3 + +-- if both exponents are below c, the sum of the powers is below 3 ^ c +two< : ∀ {a b c} → a < c → b < c → 3 ^ a + 3 ^ b < 3 ^ c +two< {a} {b} {suc c} (s≤s a≤c) (s≤s b≤c) = + ≤-<-trans + (+-mono-≤ (^-monoʳ-≤ 3 a≤c) (^-monoʳ-≤ 3 b≤c)) -- 3^a + 3^b ≤ 3^c + 3^c + (subst (3 ^ c + 3 ^ c <_) (eq c) -- 3^c + 3^c < 3 ^ suc c + (m0 3 c))) + where + -- (3^c + 3^c) + 3^c ≡ 3 * 3^c = 3 ^ suc c + eq : ∀ c → 3 ^ c + 3 ^ c + 3 ^ c ≡ 3 ^ suc c + eq c = trans (+-assoc (3 ^ c) (3 ^ c) (3 ^ c)) + (cong (3 ^ c +_) (cong (3 ^ c +_) (sym (+-identityʳ (3 ^ c))))) + +-------------------------------------------------------------------------------- +-- PART 2 — every G4ip rule strictly decreases μ +-------------------------------------------------------------------------------- + +private + f>0 : ∀ (A : Formula n) → 0 < f A + f>0 A = m^n>0 3 (w A) + + w>0 : ∀ (A : Formula n) → 0 < w A + w>0 (atom _) = s≤s z≤n + w>0 ⊤′ = s≤s z≤n + w>0 ⊥′ = s≤s z≤n + w>0 (A ∧′ B) = subst (0 <_) (+-comm 1 (w A + w B)) (s≤s z≤n) + w>0 (A ∨′ B) = subst (0 <_) (+-comm 1 (w A + w B)) (s≤s z≤n) + w>0 (A ⇒′ B) = <-≤-trans (w>0 A) (m≤m+n (w A) (w B)) + + lt1 : ∀ a b → a < a + b + 1 + lt1 a b = ≤-<-trans (m≤m+n a b) (m0 X))) + + decL1 : ∀ {Γ G} {X Y : Formula n} (i : X ∈ Γ) → f Y < f X + → μ (Y ∷ (Γ ∖ i)) G < μ Γ G + decL1 {Γ = Γ} {G} {X} {Y} i core = + subst (λ z → μ (Y ∷ (Γ ∖ i)) G < z + f G) (sym (Σf-∖ i)) + (+-monoˡ-< (f G) (+-monoˡ-< (Σf (Γ ∖ i)) core)) + + decL2 : ∀ {Γ G} {X Y Z : Formula n} (i : X ∈ Γ) → f Y + f Z < f X + → μ (Y ∷ Z ∷ (Γ ∖ i)) G < μ Γ G + decL2 {Γ = Γ} {G} {X} {Y} {Z} i core = + subst (λ z → μ (Y ∷ Z ∷ (Γ ∖ i)) G < z + f G) (sym (Σf-∖ i)) + (+-monoˡ-< (f G) + (subst (_< f X + Σf (Γ ∖ i)) (+-assoc (f Y) (f Z) (Σf (Γ ∖ i))) + (+-monoˡ-< (Σf (Γ ∖ i)) core))) + + ------------------------------------------------------------------------------ + -- the per-rule decreases + ------------------------------------------------------------------------------ + + dec∨R₁ : ∀ {Γ : List (Formula n)} {A B} → μ Γ A < μ Γ (A ∨′ B) + dec∨R₁ {Γ = Γ} {A} {B} = decG {Γ = Γ} {G = A ∨′ B} {G′ = A} (one< (lt1 (w A) (w B))) + dec∨R₂ : ∀ {Γ : List (Formula n)} {A B} → μ Γ B < μ Γ (A ∨′ B) + dec∨R₂ {Γ = Γ} {A} {B} = decG {Γ = Γ} {G = A ∨′ B} {G′ = B} (one< (lt2 (w A) (w B))) + dec∧R₁ : ∀ {Γ : List (Formula n)} {A B} → μ Γ A < μ Γ (A ∧′ B) + dec∧R₁ {Γ = Γ} {A} {B} = decG {Γ = Γ} {G = A ∧′ B} {G′ = A} (one< (lt1 (w A) (w B))) + dec∧R₂ : ∀ {Γ : List (Formula n)} {A B} → μ Γ B < μ Γ (A ∧′ B) + dec∧R₂ {Γ = Γ} {A} {B} = decG {Γ = Γ} {G = A ∧′ B} {G′ = B} (one< (lt2 (w A) (w B))) + + dec⊃R : ∀ {Γ : List (Formula n)} {A B} → μ (A ∷ Γ) B < μ Γ (A ⇒′ B) + dec⊃R {Γ = Γ} {A} {B} = + subst (_< μ Γ (A ⇒′ B)) (sym (eqR (f A) (Σf Γ) (f B))) + (+-monoʳ-< (Σf Γ) (two< (m0 B)) (m0 A)))) + + dec∧L : ∀ {Γ} (G : Formula n) {A B} (i : A ∧′ B ∈ Γ) → μ (A ∷ B ∷ (Γ ∖ i)) G < μ Γ G + dec∧L G {A} {B} i = decL2 {G = G} {Y = A} {Z = B} i (two< (lt1 (w A) (w B)) (lt2 (w A) (w B))) + + dec∨L₁ : ∀ {Γ} (G : Formula n) {A B} (i : A ∨′ B ∈ Γ) → μ (A ∷ (Γ ∖ i)) G < μ Γ G + dec∨L₁ G {A} {B} i = decL1 {G = G} {Y = A} i (one< (lt1 (w A) (w B))) + dec∨L₂ : ∀ {Γ} (G : Formula n) {A B} (i : A ∨′ B ∈ Γ) → μ (B ∷ (Γ ∖ i)) G < μ Γ G + dec∨L₂ G {A} {B} i = decL1 {G = G} {Y = B} i (one< (lt2 (w A) (w B))) + + dec⊃L⊤ : ∀ {Γ} (G : Formula n) {B} (i : ⊤′ ⇒′ B ∈ Γ) → μ (B ∷ (Γ ∖ i)) G < μ Γ G + dec⊃L⊤ G {B} i = decL1 {G = G} {Y = B} i (one< (m0 C) (m≤m+n (w C) (w D))))) + + dec⊃L⊃₁ : ∀ {Γ} (G : Formula n) {C D B} (i : (C ⇒′ D) ⇒′ B ∈ Γ) + → μ ((D ⇒′ B) ∷ (Γ ∖ i)) (C ⇒′ D) < μ Γ G + dec⊃L⊃₁ {Γ = Γ} G {C} {D} {B} i = + subst (λ z → μ ((D ⇒′ B) ∷ (Γ ∖ i)) (C ⇒′ D) < z + f G) (sym (Σf-∖ i)) + (subst₂ _<_ (eqShift S (f (D ⇒′ B)) (f (C ⇒′ D))) + (eqShift S (f X) (f G)) + (+-monoʳ-< S coreXG)) + where + S = Σf (Γ ∖ i) + X = (C ⇒′ D) ⇒′ B + coreXG : f (D ⇒′ B) + f (C ⇒′ D) < f X + f G + coreXG = <-≤-trans + (two< (+-monoˡ-< (w B) (m0 C))) + (m0 B))) + (m≤m+n (f X) (f G)) + +-------------------------------------------------------------------------------- +-- PART 3 — the fuel-free search, by well-founded recursion on μ +-------------------------------------------------------------------------------- + +private + Rec : ∀ {n} → List (Formula n) → Formula n → Set + Rec Γ G = ∀ {y} → y < μ Γ G → Acc _<_ y + +mutual + searchA : ∀ {n} (Γ : List (Formula n)) (G : Formula n) → Acc _<_ (μ Γ G) → Maybe (Γ ⊢ G) + searchA Γ G (acc rs) = + rightA Γ G rs + <∣> map ⊥L (find ⊥′ Γ) + <∣> fromHypsA Γ G rs + + rightA : ∀ {n} (Γ : List (Formula n)) (G : Formula n) → Rec Γ G → Maybe (Γ ⊢ G) + rightA Γ ⊤′ rs = just ⊤R + rightA Γ (atom k) rs = map init (find (atom k) Γ) + rightA Γ ⊥′ rs = nothing + rightA Γ (A ⇒′ B) rs = map ⊃R (searchA (A ∷ Γ) B (rs (dec⊃R {Γ = Γ} {A} {B}))) + rightA Γ (A ∨′ B) rs = + map ∨R₁ (searchA Γ A (rs (dec∨R₁ {Γ = Γ} {A} {B}))) + <∣> map ∨R₂ (searchA Γ B (rs (dec∨R₂ {Γ = Γ} {A} {B}))) + rightA Γ (A ∧′ B) rs = case searchA Γ A (rs (dec∧R₁ {Γ = Γ} {A} {B})) of λ where + (just d) → map (∧R d) (searchA Γ B (rs (dec∧R₂ {Γ = Γ} {A} {B}))) + nothing → nothing + + fromHypsA : ∀ {n} (Γ : List (Formula n)) (G : Formula n) → Rec Γ G → Maybe (Γ ⊢ G) + fromHypsA {n} Γ G rs = go Γ (λ z → z) + where + go : (Δ : List (Formula n)) → (∀ {x} → x ∈ Δ → x ∈ Γ) → Maybe (Γ ⊢ G) + go [] f = nothing + go (χ ∷ Δ) f = tryHypA Γ G χ rs (f (here refl)) <∣> go Δ (λ z → f (there z)) + + -- χ before rs/i so the shape match drives dispatch + tryHypA : ∀ {n} (Γ : List (Formula n)) (G χ : Formula n) → Rec Γ G → χ ∈ Γ → Maybe (Γ ⊢ G) + tryHypA Γ G (A ∧′ B) rs i = map (∧L i) (searchA (A ∷ B ∷ (Γ ∖ i)) G (rs (dec∧L G i))) + tryHypA Γ G (A ∨′ B) rs i = case searchA (A ∷ (Γ ∖ i)) G (rs (dec∨L₁ G i)) of λ where + (just d) → map (∨L i d) (searchA (B ∷ (Γ ∖ i)) G (rs (dec∨L₂ G i))) + nothing → nothing + tryHypA Γ G (⊤′ ⇒′ B) rs i = map (⊃L⊤ i) (searchA (B ∷ (Γ ∖ i)) G (rs (dec⊃L⊤ G i))) + tryHypA Γ G (⊥′ ⇒′ B) rs i = map (⊃L⊥ i) (searchA (Γ ∖ i) G (rs (dec⊃L⊥ G i))) + tryHypA Γ G (atom k ⇒′ B) rs i = case find (atom k) (Γ ∖ i) of λ where + (just j) → map (⊃Lat i j) (searchA (B ∷ (Γ ∖ i)) G (rs (dec⊃Lat G i))) + nothing → nothing + tryHypA Γ G ((C ∧′ D) ⇒′ B) rs i = + map (⊃L∧ i) (searchA ((C ⇒′ (D ⇒′ B)) ∷ (Γ ∖ i)) G (rs (dec⊃L∧ G i))) + tryHypA Γ G ((C ∨′ D) ⇒′ B) rs i = + map (⊃L∨ i) (searchA ((C ⇒′ B) ∷ (D ⇒′ B) ∷ (Γ ∖ i)) G (rs (dec⊃L∨ G i))) + tryHypA Γ G ((C ⇒′ D) ⇒′ B) rs i = case searchA ((D ⇒′ B) ∷ (Γ ∖ i)) (C ⇒′ D) (rs (dec⊃L⊃₁ G i)) of λ where + (just d) → map (⊃L⊃ i d) (searchA (B ∷ (Γ ∖ i)) G (rs (dec⊃L⊃₂ G i))) + nothing → nothing + tryHypA Γ G χ rs i = nothing + +-- A total, fuel-free decision search for G4ip: terminates by well-founded +-- recursion on μ, and returns a checkable derivation when it succeeds. +decide : ∀ {n} (Γ : List (Formula n)) (G : Formula n) → Maybe (Γ ⊢ G) +decide Γ G = searchA Γ G (<-wellFounded (μ Γ G)) + +-------------------------------------------------------------------------------- +-- Fuel-free *and* fast. +-- +-- `decide` is fuel-free but pays at reduction time: recursing on +-- `Acc _<_ (μ Γ G)` forces Agda to reduce the accessibility proof, which costs +-- O(μ Γ G) — and μ is exponential. The fix is to feed the *same* measure to the +-- fast structural `search` as a fuel ceiling: a `ℕ` ceiling is O(1) per step and +-- the recursion only reaches the real (small) proof depth, never the ceiling. +-- The well-founded development above is what licenses this — it shows every rule +-- strictly decreases μ, so μ is always enough fuel. +-------------------------------------------------------------------------------- + +decideFast : ∀ {n} (Γ : List (Formula n)) (G : Formula n) → Maybe (Γ ⊢ G) +decideFast Γ G = search (μ Γ G) Γ G diff --git a/Tactic/FirstOrder/Search.agda b/Tactic/FirstOrder/Search.agda new file mode 100644 index 0000000..4941ac3 --- /dev/null +++ b/Tactic/FirstOrder/Search.agda @@ -0,0 +1,113 @@ +{-# OPTIONS --safe --without-K #-} +-------------------------------------------------------------------------------- +-- Fuel-bounded proof search in the G4ip calculus of `Tactic.FirstOrder.Core`. +-- +-- `search` is the *untrusted* component: it may fail or give up when fuel runs +-- out, but every derivation it returns is a genuine `Γ ⊢ φ`, which +-- `Core.soundness` turns into a real proof. +-- +-- Because G4ip is contraction-free — every left rule discards its principal +-- formula (`Γ ∖ i`) — the search never reprocesses a hypothesis, so any fuel +-- exceeding the sequent's Dyckhoff weight is complete for IPL. `Decide` turns +-- that into a fuel-free, provably-terminating decision procedure. +-------------------------------------------------------------------------------- + +module Tactic.FirstOrder.Search where + +open import Data.Fin.Properties using (_≟_) +open import Data.List using (List; []; _∷_) +open import Data.List.Membership.Propositional using (_∈_) +open import Data.List.Relation.Unary.Any using (here; there) +open import Data.Maybe using (Maybe; just; nothing; map; _<∣>_) +open import Data.Nat using (ℕ; zero; suc) +open import Function using (case_of_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) +open import Relation.Nullary using (yes; no) + +open import Tactic.FirstOrder.Core + +private + variable + n : ℕ + +-------------------------------------------------------------------------------- +-- Locating hypotheses +-- +-- Partial syntactic equality, returning a proof only on a match. The single +-- catch-all clause is what spares us the quadratic blow-up of a full +-- `DecidableEquality`; the rules only ever need to confirm a match, not refute. +-------------------------------------------------------------------------------- + +eq? : (φ ψ : Formula n) → Maybe (φ ≡ ψ) +eq? (atom i) (atom j) = case i ≟ j of λ where + (yes refl) → just refl + (no _) → nothing +eq? ⊤′ ⊤′ = just refl +eq? ⊥′ ⊥′ = just refl +eq? (a ∧′ b) (c ∧′ d) = case eq? a c of λ where + (just refl) → map (λ { refl → refl }) (eq? b d) + nothing → nothing +eq? (a ∨′ b) (c ∨′ d) = case eq? a c of λ where + (just refl) → map (λ { refl → refl }) (eq? b d) + nothing → nothing +eq? (a ⇒′ b) (c ⇒′ d) = case eq? a c of λ where + (just refl) → map (λ { refl → refl }) (eq? b d) + nothing → nothing +eq? _ _ = nothing + +find : (φ : Formula n) (Γ : List (Formula n)) → Maybe (φ ∈ Γ) +find φ [] = nothing +find φ (ψ ∷ Γ) = case eq? φ ψ of λ where + (just refl) → just (here refl) + nothing → map there (find φ Γ) + +-------------------------------------------------------------------------------- +-- The search. Recursion is on the fuel argument; `search` decrements it before +-- delegating to the helpers. Each left rule recurses on `Γ ∖ i`, so contexts +-- shrink and fuel proportional to formula size suffices. +-------------------------------------------------------------------------------- + +mutual + search : ∀ {n} → ℕ → (Γ : List (Formula n)) (G : Formula n) → Maybe (Γ ⊢ G) + search zero Γ G = nothing + search (suc m) Γ G = + right m Γ G + <∣> map ⊥L (find ⊥′ Γ) + <∣> fromHyps m Γ G + + -- axioms and right rules (decompose the goal) + right : ∀ {n} → ℕ → (Γ : List (Formula n)) (G : Formula n) → Maybe (Γ ⊢ G) + right m Γ ⊤′ = just ⊤R + right m Γ (atom k) = map init (find (atom k) Γ) + right m Γ ⊥′ = nothing + right m Γ (A ⇒′ B) = map ⊃R (search m (A ∷ Γ) B) + right m Γ (A ∨′ B) = map ∨R₁ (search m Γ A) <∣> map ∨R₂ (search m Γ B) + right m Γ (A ∧′ B) = case search m Γ A of λ where + (just d) → map (∧R d) (search m Γ B) + nothing → nothing + + -- left rules: try each hypothesis in turn + fromHyps : ∀ {n} → ℕ → (Γ : List (Formula n)) (G : Formula n) → Maybe (Γ ⊢ G) + fromHyps {n} m Γ G = go Γ (λ z → z) + where + go : (Δ : List (Formula n)) → (∀ {x} → x ∈ Δ → x ∈ Γ) → Maybe (Γ ⊢ G) + go [] f = nothing + go (χ ∷ Δ) f = tryHyp m Γ G χ (f (here refl)) <∣> go Δ (λ z → f (there z)) + + -- the left rule selected by the shape of hypothesis χ (located by i) + tryHyp : ∀ {n} → ℕ → (Γ : List (Formula n)) (G χ : Formula n) → χ ∈ Γ → Maybe (Γ ⊢ G) + tryHyp m Γ G (A ∧′ B) i = map (∧L i) (search m (A ∷ B ∷ (Γ ∖ i)) G) + tryHyp m Γ G (A ∨′ B) i = case search m (A ∷ (Γ ∖ i)) G of λ where + (just d) → map (∨L i d) (search m (B ∷ (Γ ∖ i)) G) + nothing → nothing + tryHyp m Γ G (⊤′ ⇒′ B) i = map (⊃L⊤ i) (search m (B ∷ (Γ ∖ i)) G) + tryHyp m Γ G (⊥′ ⇒′ B) i = map (⊃L⊥ i) (search m (Γ ∖ i) G) + tryHyp m Γ G (atom k ⇒′ B) i = case find (atom k) (Γ ∖ i) of λ where + (just j) → map (⊃Lat i j) (search m (B ∷ (Γ ∖ i)) G) + nothing → nothing + tryHyp m Γ G ((C ∧′ D) ⇒′ B) i = map (⊃L∧ i) (search m ((C ⇒′ (D ⇒′ B)) ∷ (Γ ∖ i)) G) + tryHyp m Γ G ((C ∨′ D) ⇒′ B) i = map (⊃L∨ i) (search m ((C ⇒′ B) ∷ (D ⇒′ B) ∷ (Γ ∖ i)) G) + tryHyp m Γ G ((C ⇒′ D) ⇒′ B) i = case search m ((D ⇒′ B) ∷ (Γ ∖ i)) (C ⇒′ D) of λ where + (just d) → map (⊃L⊃ i d) (search m (B ∷ (Γ ∖ i)) G) + nothing → nothing + tryHyp m Γ G _ i = nothing diff --git a/Tactic/Solver/FirstOrder.agda b/Tactic/Solver/FirstOrder.agda new file mode 100644 index 0000000..fece114 --- /dev/null +++ b/Tactic/Solver/FirstOrder.agda @@ -0,0 +1,289 @@ +------------------------------------------------------------------------ +-- A reflection-based first-order (currently: intuitionistic +-- propositional) logic solver. +-- +-- `firstorder` reifies the goal type into a `Formula`, runs the +-- fuel-bounded `search` from `Tactic.FirstOrder.Search`, and — if a +-- derivation is found — interprets it via `Core.solve`. The search is +-- evaluated by Agda's own conversion checker when the emitted term is +-- unified with the hole, so the macro itself only reifies and assembles. +-- +-- Shared substrate with `Tactic.Solver.Algebra`/`.Ring`: the α-equality +-- atom table (`Reflection.Utils.Core.insertAtom`/`findAtomIndex`) and the +-- stdlib argument combinators. The macro skeleton differs because the +-- goal here is a whole proposition (not an `LHS ≈ RHS` equation) and the +-- implication connective is a `pi`, not a projected `def`. + +{-# OPTIONS --without-K --safe #-} + +module Tactic.Solver.FirstOrder where + +open import Data.Bool using (Bool; true; false; if_then_else_) +open import Data.Empty using (⊥) +open import Data.List as List using (List; []; _∷_; length; foldr) +open import Data.Maybe using (Maybe; just; nothing; from-just) +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Data.Nat.Reflection using (toTerm; toFinTerm) +open import Data.Product using (_×_; _,_; proj₁; proj₂) +open import Data.String using (String) +open import Data.Sum using (_⊎_) +open import Data.Unit using (⊤; tt) +open import Data.Vec.Base as Vec using (Vec) +open import Level using (Level) +open import Function using (case_of_) +open import Relation.Nullary using (¬_) + +open import Agda.Builtin.Reflection using (Visibility) +open import Reflection +open import Reflection.AST.Argument +open import Reflection.AST.DeBruijn using (strengthen; weaken) +import Reflection.AST.Name as Name +open import Reflection.AST.Term +open import Reflection.TCM.Syntax +open import Reflection.Utils.Args using (getVisibleArgs) +open import Reflection.Utils.Core using (insertAtom; findAtomIndex; extractNat) +open import Reflection.Utils.Metas using (firstMeta) + +open import Tactic.FirstOrder.Core using (Formula; atom; ⊤′; ⊥′; _∧′_; _∨′_; _⇒′_; solve) +import Tactic.FirstOrder.Core as Core +open import Tactic.FirstOrder.Decide using (decideFast) +open import Tactic.FirstOrder.Search using (search) + +------------------------------------------------------------------------ +-- I. Connective recognition + +private + data Conn : Set where andC orC : Conn + + -- `_×_` ↦ ∧, `_⊎_` ↦ ∨; anything else is not a binary connective. + connOf : Name → Maybe Conn + connOf nm = + if nm Name.≡ᵇ quote _×_ then just andC + else if nm Name.≡ᵇ quote _⊎_ then just orC + else nothing + + isBot isTop isNeg : Name → Bool + isBot nm = nm Name.≡ᵇ quote ⊥ + isTop nm = nm Name.≡ᵇ quote ⊤ + isNeg nm = nm Name.≡ᵇ quote ¬_ -- `¬ A` ↦ `A ⇒′ ⊥′` + +------------------------------------------------------------------------ +-- II. `Formula` Term builders. `Formula` has a single parameter `n`, +-- supplied as a leading hidden argument to each constructor. + +private + fTop fBot : Term → Term + fTop `n = con (quote ⊤′) (`n ⟅∷⟆ []) + fBot `n = con (quote ⊥′) (`n ⟅∷⟆ []) + + fBin : Name → Term → Term → Term → Term + fBin c `n x y = con c (`n ⟅∷⟆ x ⟨∷⟩ y ⟨∷⟩ []) + + fAtom : Term → ℕ → Term + fAtom `n i = con (quote atom) (`n ⟅∷⟆ toFinTerm i ⟨∷⟩ []) + +------------------------------------------------------------------------ +-- III. Reification. `classify` recognises one connective layer; `collect` +-- (which builds the α-deduplicated atom table) and `reify` (which encodes the +-- goal, looking atoms up in that table) both recurse over it, so they cannot +-- drift apart. A visible, non-dependent `pi` is an implication; a dependent +-- one (its bound variable occurs in the codomain) is treated atomically. + +private + data Shape : Set where + sTop sBot : Shape + sNeg : Term → Shape -- ¬ A + sBin : Name → Term → Term → Shape -- ∧/∨/→, tagged with its `Formula` con + sAtom : Term → Shape + + classify : Term → Shape + classify t@(def nm xs) = + if isBot nm then sBot + else if isTop nm then sTop + else if isNeg nm then + (case getVisibleArgs 1 t of λ where + (just (a Vec.∷ Vec.[])) → sNeg a + _ → sAtom t) + else case (connOf nm , getVisibleArgs 2 t) of λ where + (just andC , just (a Vec.∷ b Vec.∷ Vec.[])) → sBin (quote _∧′_) a b + (just orC , just (a Vec.∷ b Vec.∷ Vec.[])) → sBin (quote _∨′_) a b + _ → sAtom t + classify t@(pi (arg (arg-info visible _) dom) (abs _ cod)) = + case strengthen cod of λ where + (just cod') → sBin (quote _⇒′_) dom cod' + nothing → sAtom t + classify t = sAtom t + +-- Recursion is bounded by `depth` rather than structural: a connective's +-- operands are recovered through `getVisibleArgs`/`strengthen`, which Agda +-- can't see as subterms. The bound only limits formula *nesting* and is far +-- above anything realistic; on exhaustion the remaining term becomes an atom. +private + depth : ℕ + depth = 100000 + + collect : ℕ → Term → List Term → TC (List Term) + collect 0 t acc = pure (insertAtom t acc) + collect (suc d) t acc = case classify t of λ where + sTop → pure acc + sBot → pure acc + (sNeg a) → collect d a acc + (sBin _ a b) → collect d a acc >>= collect d b + (sAtom u) → pure (insertAtom u acc) + + reify : ℕ → List Term → Term → Term → TC Term + reify dpt atoms `n = go dpt + where + atomT : Term → TC Term + atomT t = case findAtomIndex t atoms of λ where + (just i) → pure (fAtom `n i) + nothing → typeError (strErr "firstorder: atom not found in table: " ∷ termErr t ∷ []) + + go : ℕ → Term → TC Term + go 0 t = atomT t + go (suc d) t = case classify t of λ where + sTop → pure (fTop `n) + sBot → pure (fBot `n) + (sNeg a) → do a′ ← go d a; pure (fBin (quote _⇒′_) `n a′ (fBot `n)) + (sBin c a b) → do a′ ← go d a; b′ ← go d b; pure (fBin c `n a′ b′) + (sAtom u) → atomT u + +------------------------------------------------------------------------ +-- IV. Quantifier prefix. +-- +-- A *dependent* leading `pi` (its bound variable occurs in the codomain) is a +-- genuine quantifier: we strip it (this is a selective `stripPis` — stdlib's +-- strips *all* leading pis), reify the body, and re-introduce the binders with +-- stdlib `prependLams` in the proof. A *non-dependent* leading `pi` is an +-- implication and stays in the formula (stripping it would drop the hypothesis, +-- as `solve` proves from the empty context). The body is left in the extended +-- context, so the atom de Bruijn indices line up with the re-introduced λs. + +private + stripQ : Term → List (String × Visibility) × Term + stripQ t@(pi (arg (arg-info v _) _) (abs s cod)) = + case strengthen cod of λ where + nothing → let bs , body = stripQ cod in (s , v) ∷ bs , body -- quantifier + (just _) → [] , t -- implication + stripQ t = [] , t + +------------------------------------------------------------------------ +-- V. Environment: ρ = lookupᴱ ⟨atom₀ , … , atomₙ₋₁⟩ : (i : Fin n) → Set (λs i) +-- +-- A `Core.Env` cons-list of the reified atom types. Its index constructs the +-- per-atom level assignment `λs`, so n, λs and ρ are all inferred from the +-- atoms — each atom keeps its own level, and goals may mix levels freely. + +private + mkAtoms : List Term → Term + mkAtoms [] = con (quote Core.[]) [] + mkAtoms (t ∷ ts) = con (quote Core._∷_) (3 ⋯⟅∷⟆ t ⟨∷⟩ mkAtoms ts ⟨∷⟩ []) + + mkEnv : List Term → Term + mkEnv atoms = def (quote Core.lookupᴱ) (2 ⋯⟅∷⟆ mkAtoms atoms ⟨∷⟩ []) + +------------------------------------------------------------------------ +-- VI. Ambient hypotheses +-- +-- A local variable `h : T` is a usable propositional hypothesis; a type +-- variable like `A : Set` is an atom, not a hypothesis. We prepend the former +-- to the goal as `⇒`-antecedents, prove the resulting closed formula, and apply +-- the proof to the actual variables — so no new soundness lemma is needed, only +-- a bigger `solve` call. + +private + -- A local variable is a usable hypothesis unless its type is *itself a + -- universe* `Set _` — a type variable (`A : Set ℓ`), which forms atoms rather + -- than being one — or `Level`, whose values can never discharge a goal. + -- Everything else qualifies at any level: `h : A` (A : Set ℓ), `f : A → B`, + -- `n : ℕ`, …. Including a redundant hypothesis only ever weakens the sequent, + -- so this never changes which goals are provable; the heterogeneous + -- environment admits a hypothesis at any level directly. + isProp : Term → TC Bool + isProp T = check <$> normalise T + where + check : Term → Bool + check (agda-sort _) = false + check (def (quote Level) _) = false + check _ = true + + -- `collect`/`reify` lifted over a list of terms + collectList : ℕ → List Term → List Term → TC (List Term) + collectList d [] acc = pure acc + collectList d (t ∷ ts) acc = collect d t acc >>= collectList d ts + + reifyList : ℕ → List Term → Term → List Term → TC (List Term) + reifyList d atoms `n [] = pure [] + reifyList d atoms `n (t ∷ ts) = do + t′ ← reify d atoms `n t + ts′ ← reifyList d atoms `n ts + pure (t′ ∷ ts′) + + -- the propositional ambient hypotheses, as (variable , type) pairs, with the + -- type weakened past the `nb` λ-binders the proof will sit under. + contextHyps : ℕ → TC (List (Term × Term)) + contextHyps nb = length <$> getContext >>= λ n → go n 0 + where + go : ℕ → ℕ → TC (List (Term × Term)) + go zero _ = pure [] + go (suc r) i = do + Tᵢ ← inferType (var i []) + ok ← isProp Tᵢ + rest ← go r (suc i) + pure (if ok then (var (i + nb) [] , weaken nb Tᵢ) ∷ rest else rest) + +------------------------------------------------------------------------ +-- VII. The macro + +private + -- `nothing` runs the complete fuel-free `decideFast`; `just k` runs the + -- bounded `search` at fuel `k`. Since `decideFast = search (μ …)`, the two do + -- identical search work — they differ only in who supplies the fuel ceiling. + solveFOL : Maybe ℕ → Term → TC ⊤ + solveFOL mfuel hole = do + -- the goal type as-is: `normalise` would unfold our connectives + -- (`_×_ ↦ Σ`, `⊥ ↦ Irrelevant Empty`, …) + goal ← inferType hole + let binders , body = stripQ goal -- strip the universal-quantifier prefix + -- A function-typed whole-RHS goal whose codomain ignores its domain (`A → ⊤`) + -- arrives with the domain an unsolved metavariable we cannot pin; reject it + -- with the workaround rather than a cryptic "unsolved metas". + _ ← case firstMeta body of λ where + (just _) → typeError + ( strErr "firstorder: the goal contains an unsolved metavariable, so it" + ∷ strErr " cannot be reified. This happens when `firstorder` is the whole" + ∷ strErr " right-hand side of a function-typed goal whose result ignores" + ∷ strErr " the argument (e.g. `A → ⊤`). Introduce the argument(s) first," + ∷ strErr " e.g. `f x = firstorder`." + ∷ []) + nothing → pure tt + -- prepend the ambient hypotheses' types as `⇒`-antecedents; the proof of the + -- resulting closed formula is then applied to the hypothesis variables. + hyps ← contextHyps (length binders) + let hTys = List.map proj₂ hyps + atoms ← collect depth body [] >>= collectList depth hTys + let `n = toTerm (length atoms) + `body ← reify depth atoms `n body + `hyps ← reifyList depth atoms `n hTys + let `φ = foldr (fBin (quote _⇒′_) `n) `body `hyps + let `Γ = con (quote List.List.[]) (2 ⋯⟅∷⟆ []) + let `srch = case mfuel of λ where + (just fuel) → def (quote search) (`n ⟅∷⟆ toTerm fuel ⟨∷⟩ `Γ ⟨∷⟩ `φ ⟨∷⟩ []) + nothing → def (quote decideFast) (`n ⟅∷⟆ `Γ ⟨∷⟩ `φ ⟨∷⟩ []) + let `drv = def (quote from-just) (2 ⋯⟅∷⟆ `srch ⟨∷⟩ []) + -- `solve`'s implicits (n, ℓ, φ) are all pinned by the environment and `drv` + let proof = def (quote solve) (mkEnv atoms ⟨∷⟩ `drv ⟨∷⟩ + List.map (λ h → vArg (proj₁ h)) hyps) + unify hole (prependLams binders proof) + +macro + -- complete, fuel-free + firstorder : Term → TC ⊤ + firstorder = solveFOL nothing + + -- with an explicit fuel bound (a ℕ literal) + firstorderN : Term → Term → TC ⊤ + firstorderN `fuel hole = do + just fuel ← pure (extractNat `fuel) + where nothing → typeError (strErr "firstorderN: first argument must be a ℕ literal" ∷ []) + solveFOL (just fuel) hole diff --git a/Tactic/Solver/FirstOrder/Tests.agda b/Tactic/Solver/FirstOrder/Tests.agda new file mode 100644 index 0000000..009cad8 --- /dev/null +++ b/Tactic/Solver/FirstOrder/Tests.agda @@ -0,0 +1,361 @@ +{-# OPTIONS --without-K --safe #-} +-------------------------------------------------------------------------------- +-- Capabilities and limitations of the `firstorder` solver. +-- +-- PART 1 (capabilities): 44 goals proved automatically by the `firstorder` +-- macro — propositional reasoning over →, ×, ⊎, ¬, ⊤, ⊥ (complete for +-- intuitionistic propositional logic), universal-quantifier prefixes, and +-- ambient hypotheses (local variables of propositional type). Every atom carries +-- its own universe level, so the goals below are stated level-polymorphically +-- and freely mix levels (with `⊤`/`⊥` staying the genuine `Set₀` units). The +-- search runs inside Agda's evaluator during type-checking, so a green module +-- means every goal was discharged. +-- +-- PART 2 (limitations): negative tests. A *failing* macro call is a hard type +-- error and cannot live in a compiling file, so instead we assert at the value +-- level that the search returns `nothing` — a machine-checked demonstration that +-- the solver cannot prove these. The limitations that manifest only at the +-- reflection level (classical reasoning, quantifier instantiation, the `A → ⊤` +-- meta quirk) are shown as commented macro calls at the bottom. +-------------------------------------------------------------------------------- + +module Tactic.Solver.FirstOrder.Tests where + +open import Data.Product using (_×_) +open import Data.Sum using (_⊎_) +open import Data.Unit using (⊤) +open import Data.Empty using (⊥) +open import Level using (Level) +open import Relation.Nullary using (¬_) + +open import Tactic.Solver.FirstOrder + +-------------------------------------------------------------------------------- +-- PART 1 — Capabilities +-------------------------------------------------------------------------------- + +module _ {a b c d : Level} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where + + -- Implication (the {S,K,I} combinators and friends) + I-comb : A → A + I-comb = firstorder + + K-comb : A → B → A + K-comb = firstorder + + S-comb : (A → B → C) → (A → B) → A → C + S-comb = firstorder + + compose : (A → B) → (B → C) → A → C + compose = firstorder + + compose3 : (A → B) → (B → C) → (C → D) → A → D + compose3 = firstorder + + -- Conjunction + ∧-fst : A × B → A + ∧-fst = firstorder + + ∧-snd : A × B → B + ∧-snd = firstorder + + ∧-intro : A → B → A × B + ∧-intro = firstorder + + ∧-comm : A × B → B × A + ∧-comm = firstorder + + ∧-assoc-lr : (A × B) × C → A × (B × C) + ∧-assoc-lr = firstorder + + ∧-assoc-rl : A × (B × C) → (A × B) × C + ∧-assoc-rl = firstorder + + -- Disjunction + ∨-inl : A → A ⊎ B + ∨-inl = firstorder + + ∨-inr : B → A ⊎ B + ∨-inr = firstorder + + ∨-comm : A ⊎ B → B ⊎ A + ∨-comm = firstorder + + ∨-elim : (A → C) → (B → C) → A ⊎ B → C + ∨-elim = firstorder + + ∨-idem : A ⊎ A → A + ∨-idem = firstorder + + -- Interaction + distrib : A × (B ⊎ C) → (A × B) ⊎ (A × C) + distrib = firstorder + + distrib-rev : (A × B) ⊎ (A × C) → A × (B ⊎ C) + distrib-rev = firstorder + + curry′ : (A × B → C) → A → B → C + curry′ = firstorder + + uncurry′ : (A → B → C) → A × B → C + uncurry′ = firstorder + + split : (A ⊎ B → C) → (A → C) × (B → C) + split = firstorder + + -- Units and absurdity + triv : ⊤ + triv = firstorder + + -- `A → ⊤` as a whole RHS would leave the domain as an unsolved meta + -- (see Limitation 4); introducing the argument first sidesteps it. + to-⊤ : A → ⊤ + to-⊤ _ = firstorder + + ex-falso : ⊥ → A + ex-falso = firstorder + + -- Negation: `¬_` is recognised as `_→ ⊥`, so it can be written either way. + dni⊥ : A → ((A → ⊥) → ⊥) -- with an explicit ⊥ + dni⊥ = firstorder + + dni : A → ¬ ¬ A -- with ¬ (double-negation introduction) + dni = firstorder + + contra : (A → B) → ¬ B → ¬ A + contra = firstorder + + tne : ¬ ¬ ¬ A → ¬ A -- triple negation collapses to one + tne = firstorder + + de-morgan : ¬ (A ⊎ B) → ¬ A + de-morgan = firstorder + + -- Harder intuitionistic tautologies. These need G4ip's contraction-free + -- implication-left rules; the earlier naive search could not find them. + dn-lem : ¬ ¬ (A ⊎ ¬ A) -- double-negation of excluded middle + dn-lem = firstorder + + no-contra : ¬ (A × ¬ A) + no-contra = firstorder + + dm-full : ¬ (A ⊎ B) → (¬ A × ¬ B) -- both halves of one De Morgan law + dm-full = firstorder + + nested : ((A → B) → C) → B → C + nested = firstorder + + -- Explicit fuel control + I-comb′ : A → A + I-comb′ = firstorderN 4 + +-- Universal quantifiers at the goal prefix are stripped and re-introduced, so +-- the bound variable can be a proposition or an individual (as long as no +-- quantifier *instantiation* is needed — see Limitation 3). +module _ where + + ∀-id : ∀ {ℓ} (X : Set ℓ) → X → X + ∀-id = firstorder + + ∀-const : ∀ {ℓ₁ ℓ₂} (X : Set ℓ₁) (Y : Set ℓ₂) → X → Y → X + ∀-const = firstorder + + ∀-dup : ∀ {ℓ} (X : Set ℓ) → X → X × X + ∀-dup = firstorder + + -- a genuine ∀ over individuals: the bound `x` appears only inside atoms + ∀-pred : ∀ {ℓ} {D : Set ℓ} {P : D → Set ℓ} → (x : D) → P x → P x + ∀-pred = firstorder + +-- Ambient hypotheses: local variables of propositional type are used as +-- assumptions, not just the goal's own structure. (Type variables like A B C — +-- whose type is itself a universe `Set _` — are atoms, not hypotheses, so the +-- regression goals above still hold.) +module _ {a b c : Level} {A : Set a} {B : Set b} {C : Set c} where + + -- a pattern-introduced argument becomes a usable hypothesis + use-hyp : (h : A) → A + use-hyp h = firstorder + + modus : A → (A → B) → B + modus a f = firstorder + + chain-hyp : A → (A → B) → (B → C) → C + chain-hyp a f g = firstorder + + case-hyp : A ⊎ B → (A → C) → (B → C) → C + case-hyp s f g = firstorder + + contra-hyp : A → ¬ A → C + contra-hyp a na = firstorder + +-- a hypothesis that is a *module parameter* (never part of the goal type) +module _ {a b : Level} {A : Set a} {B : Set b} (f : A → B) where + apply-param : A → B + apply-param a = firstorder + +-------------------------------------------------------------------------------- +-- PART 2 — Limitations (negative tests, verified at the value level) +-------------------------------------------------------------------------------- + +module Limitations where + open import Data.Fin using (zero; suc) + open import Data.List using ([]) + open import Data.Maybe using (nothing; from-just) + open import Relation.Binary.PropositionalEquality using (_≡_; refl) + + open import Tactic.FirstOrder.Core using (Formula; atom; ⊤′; ⊥′; _∧′_; _∨′_; _⇒′_; _⊢_) + open import Tactic.FirstOrder.Search using (search) + + ------------------------------------------------------------------------------ + -- Limitation 1: the logic is INTUITIONISTIC, not classical. + -- + -- The following are classically valid but have no intuitionistic proof. Since + -- G4ip is complete for IPL, exhausting the (finite) search space returns + -- `nothing` definitively — no amount of fuel would help. + ------------------------------------------------------------------------------ + + p q : Formula 2 + p = atom zero + q = atom (suc zero) + + r : Formula 1 + r = atom zero + + -- Peirce's law: ((P → Q) → P) → P + peirce : Formula 2 + peirce = ((p ⇒′ q) ⇒′ p) ⇒′ p + + _ : search 20 [] peirce ≡ nothing + _ = refl + + -- Excluded middle: P ∨ ¬P + excluded-middle : Formula 1 + excluded-middle = r ∨′ (r ⇒′ ⊥′) + + _ : search 20 [] excluded-middle ≡ nothing + _ = refl + + -- Double-negation elimination: ¬¬P → P + dne : Formula 1 + dne = ((r ⇒′ ⊥′) ⇒′ ⊥′) ⇒′ r + + _ : search 20 [] dne ≡ nothing + _ = refl + + ------------------------------------------------------------------------------ + -- Limitation 2: the `search` primitive is FUEL-BOUNDED — but `firstorder` is + -- NOT subject to it. + -- + -- `firstorder` uses the fuel-free decider `decideFast`, whose ceiling is the + -- proven termination measure `μ`, so it is complete for intuitionistic + -- propositional logic. The fuel cap below is a property only of the lower-level + -- `search` primitive (and of `firstorderN`, which exposes it): a goal whose + -- search depth exceeds the given fuel fails. `A → A` needs ≥ 2 steps (⊃R, init). + ------------------------------------------------------------------------------ + + identity : Formula 1 + identity = atom zero ⇒′ atom zero + + -- fuel 1 is not enough → no proof found + _ : search 1 [] identity ≡ nothing + _ = refl + + -- fuel 2 is enough → `found` extracts the derivation (type-checks iff `just`) + _ : [] ⊢ identity + _ = from-just (search 2 [] identity) + + ------------------------------------------------------------------------------ + -- Limitation 3: the solver is PURELY PROPOSITIONAL and SYNTACTIC. + -- + -- Any subterm not built from ×, ⊎, →, ¬, ⊤, ⊥ is an opaque atom, and distinct + -- atoms are logically independent. So there is no way to prove an implication + -- between two unrelated atoms — and in particular a universally quantified + -- hypothesis (an opaque atom) cannot be *instantiated*: `(∀ x → P x) → P a` + -- is out of reach (see the commented `instM` below). + ------------------------------------------------------------------------------ + + _ : search 20 [] (p ⇒′ q) ≡ nothing + _ = refl + +-------------------------------------------------------------------------------- +-- Further limitations, shown as commented macro calls: a failing macro is a hard +-- type error and cannot sit in a compiling file, so uncomment any line to +-- observe the failure it documents. +-------------------------------------------------------------------------------- + +-- module CommentedFailures {A B : Set} {D : Set} {P : D → Set} {a : D} where +-- +-- -- Limitation 1 (classical), via the macro: Peirce's law. +-- peirceM : ((A → B) → A) → A +-- peirceM = firstorder +-- +-- -- Limitation 3: quantifiers can only be *stripped* from the goal prefix +-- -- (see `∀-id`, `∀-pred` above), never *instantiated*. A universally +-- -- quantified hypothesis is an opaque atom, so it cannot be applied to a +-- -- witness: `(∀ x → P x) → P a` is out of reach (`∀ x → P x` and `P a` are +-- -- two unrelated atoms). +-- instM : ((x : D) → P x) → P a +-- instM = firstorder +-- +-- -- Limitation 4: when the macro is the *whole* RHS of a function-typed goal +-- -- whose codomain ignores the domain, Agda hands the macro a goal with an +-- -- unsolvable metavariable domain. This is an elaboration quirk the macro +-- -- cannot fix, but it is *detected*: the line below fails with a clear error +-- -- pointing at the workaround — introduce the argument(s) first, as `to-⊤` +-- -- above does with `to-⊤ _ = firstorder`. +-- to-⊤M : A → ⊤ +-- to-⊤M = firstorder + +-------------------------------------------------------------------------------- +-- PART 3 — engine-level unit tests +-- +-- The macro tests above exercise the whole pipeline; here we test the +-- components directly, at the value level: the G4ip calculus + `solve`, and +-- the three search entry points `search` / `decide` / `decideFast`. +-------------------------------------------------------------------------------- + +module Engine where + open import Data.Fin using (Fin; zero; suc) + open import Data.List using ([]) + open import Data.List.Relation.Unary.Any using (here) + open import Data.Maybe using (nothing; from-just) + open import Relation.Binary.PropositionalEquality using (_≡_; refl) + + open import Level using (0ℓ) + open import Tactic.FirstOrder.Core + open import Tactic.FirstOrder.Search using (search) + open import Tactic.FirstOrder.Decide using (decide; decideFast) + + A B : Formula 2 + A = atom zero + B = atom (suc zero) + + peirce : Formula 2 + peirce = ((A ⇒′ B) ⇒′ A) ⇒′ A + + -- a hand-built G4ip derivation interprets via `solve`, and its soundness + -- payload is exactly the identity function it should be. + ⊢-id : ∀ {ρ : Fin 2 → Set} → ⟦ A ⇒′ A ⟧ (λ _ → 0ℓ) ρ + ⊢-id {ρ} = solve ρ (⊃R (init (here refl))) + + _ : ∀ {ρ : Fin 2 → Set} {a : ρ zero} → ⊢-id {ρ} a ≡ a + _ = refl + + -- each entry point finds a proof… + _ : [] ⊢ (A ∧′ B ⇒′ B ∧′ A) + _ = from-just (search 8 [] (A ∧′ B ⇒′ B ∧′ A)) + + _ : [] ⊢ (A ∧′ B ⇒′ B ∧′ A) + _ = from-just (decide [] (A ∧′ B ⇒′ B ∧′ A)) + + _ : [] ⊢ (¬′ ¬′ (A ∨′ ¬′ A)) -- exercises the ⊃L⊃ rule + _ = from-just (decideFast [] (¬′ ¬′ (A ∨′ ¬′ A))) + + -- …and `decide`/`decideFast` reject the (classically valid) Peirce's law + -- (`search` on Peirce is covered by Limitation 1 above) + _ : decide [] peirce ≡ nothing + _ = refl + + _ : decideFast [] peirce ≡ nothing + _ = refl