Использование Agda Data.Bool solver - PullRequest
Новая
       11

Использование Agda Data.Bool solver

0 голосов
/ 28 октября 2019

Я пытался использовать Agda Data.Bool solver в Agda версии 2.6.1-4e989c1 

module example where

  open import Data.Bool hiding ( _∨_ )
  open import Relation.Binary
  open import Relation.Binary.PropositionalEquality

  open import Data.Bool.Solver using (module xor-∧-Solver)
  open xor-∧-Solver

  problem0' :  ( Cat : Bool ) → (Cat xor Cat ) ≡ false
  problem0' = solve 1 (λ c → (c :+ c ) := con false ) refl

, пока все хорошо. 

  problem1' :  ( Cat : Bool ) → (Cat ∧ (Cat xor true ))  ≡ false
  problem1' = solve 1 (λ c → ((c :* (c :+ con true )) ) := con false ) ?

Ввод refl в?, дайте нам очень долгий конфликт, включая Data.Vec.Vec.[]) !=< false of type Bool. Я что-то пропустил?

1 Ответ

1 голос
/ 28 октября 2019

Если вы попросите нормализованную цель (большинство команд, относящихся к печати цели, могут иметь префикс C-u C-u, чтобы отобразить нормальную форму вывода), вы получите: 

{x : Bool} → (x xor true) ∧ x xor false ≡ false

, как далекорешатель смог «упростить» задачу.

Я могу ошибаться, но это равенство, похоже, не следует только из законов коммутативных колец, с которыми работает решатель.

Решатель, специфичный для Bool, может воспользоваться преимуществами дополнительной структуры или даже просто разделением регистра, если не слишком много переменных.

...