CODEWITHSUNDEEP
agda
Nathan BeDell
Nathan BeDell

Reputation: 2293

Irrelevant implicits: Why doesn't agda infer this proof?

Recently I made a type for finite sets in Agda with the following implementation:

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Empty
open import Data.Unit
open import Relation.Binary.PropositionalEquality
open import Data.Nat

suc-inj : (n m : ℕ) → (suc n) ≡ (suc m) → n ≡ m
suc-inj n .n refl = refl

record Eq (A : Set) : Set₁ where
  constructor mkEqInst
  field
    _decide≡_ : (a b : A) → Dec (a ≡ b)
open Eq {{...}}

mutual
  data FinSet (A : Set) {{_ : Eq A }} : Set where
    ε   : FinSet A
    _&_ : (a : A) → (X : FinSet A) → .{ p : ¬ (a ∈ X)} → FinSet A

  _∈_ : {A : Set} → {{p : Eq A}} → (a : A) → FinSet A → Set
  a ∈ ε = ⊥
  a ∈ (b & B) with (a decide≡ b)
  ...            | yes _     = ⊤
  ...            | no _    = a ∈ B

  _∉_ : {A : Set} → {{p : Eq A}} → (a : A) → FinSet A → Set
  _∉_ a X = ¬ (a ∈ X)

decide∈ : {A : Set} → {{_ : Eq A}} → (a : A) → (X : FinSet A) → Dec (a ∈ X)
decide∈ a ε = no (λ z → z)
decide∈ a (b & X) with (a decide≡ b)
decide∈ a (b & X)    | yes _ = yes tt
...                  | no _  = decide∈ a X

decide∉ : {A : Set} → {{_ : Eq A}} → (a : A) → (X : FinSet A) → Dec (a ∉ X)
decide∉ a X = ¬? (decide∈ a X)

instance
  eqℕ : Eq ℕ
  eqℕ = mkEqInst decide
    where decide : (a b : ℕ) → Dec (a ≡ b)
          decide zero zero = yes refl
          decide zero (suc b) = no (λ ())
          decide (suc a) zero = no (λ ())
          decide (suc a) (suc b) with (decide a b)
          ...                       | yes p = yes (cong suc p)
          ...                       | no  p = no (λ x → p ((suc-inj a b) x))

However, when I test this type out with the following:

test : FinSet ℕ
test = _&_ zero ε

Agda for some reason can't infer the implicit argument of type ¬ ⊥! However, auto of course finds the proof of this trivial proposition: λ x → x : ¬ ⊥.

My question is this: Since I've marked the implicit proof as irrelevant, why can't Agda simply run auto to find the proof of ¬ ⊥ during type checking? Presumably, whenever filling in other implicit arguments, it might matter exactly what proof Agda finda, so it shouldn't just run auto, but if the proof has been marked irrelevant, like it my case, why can't Agda find a proof?

Note: I have a better implementation of this, where I implement ∉ directly, and Agda can find the relevant proof, but I want to understand in general why Agda can't automatically find these sorts of proofs for implicit arguments. Is there any way in the current implementation of Agda to get these "auto implicits" like I want here? Or is there some theoretical reason why this would be a bad idea?

Upvotes: 4

Views: 278

Answers (2)

Jesper
Jesper

Reputation: 2955

If you give a more direct definition of ∉, then the implicit argument gets type ⊤ instead of ¬ ⊥. Agda can fill in arguments of type ⊤ automatically by eta-expansion, so your code just works:

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Empty
open import Data.Unit
open import Relation.Binary.PropositionalEquality
open import Data.Nat

suc-inj : (n m : ℕ) → (suc n) ≡ (suc m) → n ≡ m
suc-inj n .n refl = refl

record Eq (A : Set) : Set₁ where
  constructor mkEqInst
  field
    _decide≡_ : (a b : A) → Dec (a ≡ b)
open Eq {{...}}

mutual
  data FinSet (A : Set) {{_ : Eq A}} : Set where
    ε   : FinSet A
    _&_ : (a : A) → (X : FinSet A) → .{p : (a ∉ X)} → FinSet A

  _∉_ : {A : Set} → {{p : Eq A}} → (a : A) → FinSet A → Set
  a ∉ ε = ⊤
  a ∉ (b & X) with (a decide≡ b)
  ...            | yes _ = ⊥
  ...            | no  _ = a ∉ X

decide∉ : {A : Set} → {{_ : Eq A}} → (a : A) → (X : FinSet A) → Dec (a ∉ X)
decide∉ a ε = yes tt
decide∉ a (b & X) with (a decide≡ b)
...                  | yes _ = no (λ z → z)
...                  | no  _ = decide∉ a X

instance
  eqℕ : Eq ℕ
  eqℕ = mkEqInst decide
    where decide : (a b : ℕ) → Dec (a ≡ b)
          decide zero zero = yes refl
          decide zero (suc b) = no (λ ())
          decide (suc a) zero = no (λ ())
          decide (suc a) (suc b) with (decide a b)
          ...                       | yes p = yes (cong suc p)
          ...                       | no  p = no (λ x → p ((suc-inj a b) x))

test : FinSet ℕ
test = _&_ zero ε

Upvotes: 1

Saizan
Saizan

Reputation: 1401

There's no fundamental reason why irrelevant arguments couldn't be solved by proof search, however the fear is that in many cases it would be slow and/or not find a solution.

A more user-directed thing would be to allow the user to specify that a certain argument should be inferred using a specific tactic, but that has not been implemented either. In your case you would provide a tactic that tries to solve the goal with (\ x -> x).

Upvotes: 2

Related Questions