Skip to content

Instantly share code, notes, and snippets.

@UlfNorell
Created June 3, 2020 14:31
Show Gist options
  • Save UlfNorell/7bd96a4f13acf3fbf62e2b2a7c05c438 to your computer and use it in GitHub Desktop.
Save UlfNorell/7bd96a4f13acf3fbf62e2b2a7c05c438 to your computer and use it in GitHub Desktop.
{-# OPTIONS --rewriting #-}
module _ where
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
open import Agda.Builtin.String renaming (primStringEquality to _==_)
open import Agda.Builtin.List
data ⊥ : Set where
postulate
primExec : String → List String → String
postulate
Problem : Set
⟦_⟧ : Problem → Set
formatP : Problem → String
prover : Problem → Bool
prover p = primExec "z3" (formatP p ∷ []) == "OK"
postulate
sound : ∀ p → prover p ≡ true → ⟦ p ⟧
Proof : ∀ p → Set
Proof p with prover p
... | true = ⟦ p ⟧
... | false = ⊤
prove : ∀ p → Proof p
prove p with prover p | sound p
... | true | s = s refl
... | false | _ = _
{-# BUILTIN REWRITE _≡_ #-}
postulate
hard-problem : Problem
eval-format : formatP hard-problem ≡ "hard-problem"
eval-exec : primExec "z3" ("hard-problem" ∷ []) ≡ "OK"
{-# REWRITE eval-format #-}
{-# REWRITE eval-exec #-}
test : ⟦ hard-problem ⟧
test = prove hard-problem
check : test ≡ sound hard-problem refl
check = refl
@UlfNorell
Copy link
Author

What it might look like with a TC version of primExec:

{-# OPTIONS --rewriting #-}

module _ where

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
open import Agda.Builtin.String renaming (primStringEquality to _==_)
open import Agda.Builtin.List
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)

data  : Set where

primExec : String  List String  TC String
primExec "z3" ("hard-problem" ∷ []) = returnTC "OK"
primExec _ _ = returnTC "NO"

postulate
  Problem : Set
  ⟦_⟧ : Problem  Set
  formatP : Problem  String

private
  data Witness (p : Problem) : Set where
    proved-by : String  Witness p
  
postulate
  sound :  p  Witness p  ⟦ p ⟧

pattern vArg x = arg (arg-info visible relevant) x

macro
  prove : Problem  Term  TC ⊤
  prove p hole = do
    "OK"  primExec "z3" (formatP p ∷ [])
      where _  typeError (strErr "Not provable" ∷ [])
    `p  quoteTC p
    unify hole (def (quote sound) ( vArg `p
                                  ∷ vArg (con (quote proved-by) (vArg (lit (string "z3")) ∷ []))
                                  ∷ []))
    
{-# BUILTIN REWRITE _≡_ #-}

postulate
  hard-problem : Problem
  eval-format : formatP hard-problem ≡ "hard-problem"
  
{-# REWRITE eval-format #-}

test : ⟦ hard-problem ⟧
test = prove hard-problem

check : test ≡ sound hard-problem (proved-by "z3")
check = refl

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment