5

I want to write a function which take set as input and return true if it is top and false if it is bottom. I have tried in this way..

isTop : Set → Bool
isTop x = if (x eq ⊤) then true
              else false

But i am not able to define eq correctly. I tried as..

_eq_ : Set → Set → Bool
⊤ eq ⊥ = false

This is not working because when i check T eq T it is also returning false.

Please help me to write this eq function or any other ways to write isTop.

ajayv
  • 641
  • 6
  • 21
  • 2
    It is possible to, for example, define a Set whose inhabitants are proofs of the Goldbach conjecture. What does that tell you about `isTop`? – luqui Jun 12 '15 at 02:34
  • 3
    I'm not sure how to define `isTop`, but the reason `⊤ eq ⊤` is returning false is because you cannot pattern match on something of type `Set`. Agda is interpreting `⊤` and `⊥` as ordinary variable names. It would be same same as saying `x eq y = false`. – Matt Jun 12 '15 at 02:53
  • @luqui I am not getting how to define a set with that proof. Can you elaborate?? – ajayv Jun 12 '15 at 04:39
  • 3
    In short, this is impossible. You should instead state what broader goal you are trying to accomplish. – user2407038 Jun 12 '15 at 07:16
  • 2
    The universe `Set` is not an inductively defined type, so you can't use pattern matching on that. Suppose you could somehow have a definition for `_eq_` using pattern matching. Later on you could add a custom type `data Foo : Set where ...`, where `Foo` was not considered in the definition of `_eq_`. – chi Jun 12 '15 at 08:37

1 Answers1

8

It's impossible in Agda, but is not senseless in general.

You could write something not very meaninigful:

open import Data.Empty
open import Data.Unit
open import Data.Bool

data U : Set where
  bot top : U

⟦_⟧ : U -> Set
⟦ bot ⟧ = ⊥
⟦ top ⟧ = ⊤

record Is {α} {A : Set α} (x : A) : Set where

is : ∀ {α} {A : Set α} -> (x : A) -> Is x
is _ = _

isTop : ∀ {u} -> Is ⟦ u ⟧ -> Bool
isTop {bot} _ = false
isTop {top} _ = true

open import Relation.Binary.PropositionalEquality

test-bot : isTop (is ⊥) ≡ false
test-bot = refl

test-top : isTop (is ⊤) ≡ true
test-top = refl

u can be inferred from Is ⟦ u ⟧, because ⟦_⟧ is constructor headed. Is is a singleton, so it allows to lift values to the type level. You can find an example of using here.

Community
  • 1
  • 1
effectfully
  • 12,325
  • 2
  • 17
  • 40
  • This is really helpful. Thanks a lot. But still my problem does not resolve. I want to write if(isTop (is (chkTop))) and definition of chkTop is `chkTop : something -> Set chkTop x = if (x is true) then T else bot.` When i compile this i get error set != [[ _u x y_]]. – ajayv Jun 12 '15 at 11:14
  • 1
    @ajayv, I don't understand your code, but, AFAIK, there is no way to break parametricity in Agda, so it's not possible to somehow emulate your `isTop` function. But your original question looks like an [XY problem](http://meta.stackexchange.com/questions/66377/what-is-the-xy-problem). Why do you need this `isTop`? – effectfully Jun 12 '15 at 12:48
  • Actually this is the root problem of mine. If this get solved I do not require isTop function. Please take a look https://stackoverflow.com/questions/30817693/how-can-i-change-working-of-forall-in-agda – ajayv Jun 13 '15 at 10:41
  • 1
    @ajayv, your definition of `isCut` looks ok to me (I would rather use `T` from `Data.Bool.Base`, but that's a minor point). You don't need the `isTop` function — you need to pattern match on this big expression `((((p mem (getLC x)) ...` using `with` in every function, that exploits the `isCut` property, and handle `false` and `true` cases differently. – effectfully Jun 13 '15 at 12:05
  • Now I am relax that I dont need isTop function. Can you write some line of code I still dint get to handle false and true case seperately. Is it possible to write isCut : cut -> Bool. If it is please help me I am struck on this from last 4 days. I need to resolve this ASAP. – ajayv Jun 13 '15 at 14:59
  • 1
    @ajayv, "Is it possible to write isCut : cut -> Bool" — no, because the definition of `isCut` contains quantification. Please, minimize your problem and make the question self-contained, otherwise it's hard to help you. – effectfully Jun 13 '15 at 16:29
  • thanks for your patience.. I have minimized my problem ..please look at this..http://stackoverflow.com/questions/30820714/how-to-use-logical-and-operation-between-two-sets-in-agda – ajayv Jun 13 '15 at 16:45