logicagda

How to use agda almost without data, only with postulates?

module sets where

postulate
    š•Š : Set
    _āˆˆ_ : š•Š ā†’ š•Š ā†’ Set
infix 50 _āˆˆ_

data _and_ : Set ā†’ Set ā†’ Set where
    _āˆ§_ : (x y : Set) ā†’ x and y
infixl 40 _and_
infixl 40 _āˆ§_

data _ā‰”_ : Set ā†’ Set ā†’ Set where
    _eq_ : (a b : Set) ā†’ a ā†’ b and b ā†’ a ā†’ a ā‰” b
infixr 30 _ā‰”_
infixr 30 _eq_

postulate
    _==_ : š•Š ā†’ š•Š ā†’ Set
    ==-def : (x y z : š•Š) ā†’ ((z āˆˆ x ā‰” z āˆˆ y) ā‰” x == y)
infixr 50 _==_

postulate
    eq_ax : (x y : š•Š) ā†’ (x == y) ā†’ (z : š•Š) ā†’ (x āˆˆ z ā‰” y āˆˆ z)
    āˆƒ : (x : Set) ā†’ (z : x ā†’ Set) ā†’ Set
    āˆƒ-def : (x : Set) ā†’ (y : x) ā†’ (z : x ā†’ Set) ā†’ (z y ā‰” āˆƒ x z)
    pair_ax : (x y : š•Š) ā†’ āˆƒ š•Š Ī» { z ā†’ x āˆˆ z and y āˆˆ z }
    āˆŖ : š•Š ā†’ š•Š
    āˆŖ_def : (x y : š•Š) ā†’ x āˆˆ āˆŖ y ā‰” āˆƒ š•Š Ī» { z ā†’ x āˆˆ z and z āˆˆ y }
    _āŠ†_ : š•Š ā†’ š•Š ā†’ Set
    āŠ†-def : (x y : š•Š) ā†’ ((z : š•Š) ā†’ z āˆˆ x ā†’ z āˆˆ y) ā‰” x āŠ† y
infixl 50 _āŠ†_

first-proof : (x y : š•Š) ā†’ x āŠ† y ā†’ (āˆŖ x) āŠ† (āˆŖ y)
first-proof x y z = {!!}

I am new to Agda. I try to find something that can verify my evidence. And so far Agda seems to be the best option (but still not enough convenient). I am implementing ZFC. And don't know, how to proof the last sentence.

I expect to proof without data, closest to the usual proof with quantifiers and connectives.

Solution 
  • module sets where

data _and_ : Set ā†’ Set ā†’ Set where
    _āˆ§_ : {x y : Set} ā†’ x ā†’ y ā†’ x and y
infixl 40 _and_
infixl 40 _āˆ§_

data _ā‰”_ : Set ā†’ Set ā†’ Set where
    eq : {x y : Set} ā†’ (x ā†’ y) and (y ā†’ x) ā†’ x ā‰” y
infixr 30 _ā‰”_

straight : {x y : Set} ā†’ x ā‰” y ā†’ x ā†’ y
straight (eq (z āˆ§ w)) = z

back : {x y : Set} ā†’ x ā‰” y ā†’ y ā†’ x
back (eq (z āˆ§ w)) = w

data āˆƒ : {x : Set} ā†’ (z : x ā†’ Set) ā†’ Set where
    exists : {x : Set} ā†’ (y : x) ā†’ (z : x ā†’ Set) ā†’ z y ā†’ āˆƒ z

postulate
    š•Š : Set
    _āˆˆ_ : š•Š ā†’ š•Š ā†’ Set
infix 50 _āˆˆ_

postulate
    _==_ : š•Š ā†’ š•Š ā†’ Set
    ==-def : (x y z : š•Š) ā†’ ((z āˆˆ x ā‰” z āˆˆ y) ā‰” x == y)
infixr 50 _==_

postulate
    eq_ax : (x y : š•Š) ā†’ (x == y) ā†’ (z : š•Š) ā†’ (x āˆˆ z ā‰” y āˆˆ z)
    pair_ax : (x y : š•Š) ā†’ āˆƒ Ī» { z ā†’ x āˆˆ z and y āˆˆ z }
    āˆŖ : š•Š ā†’ š•Š
    āˆŖ-def : (x y : š•Š) ā†’ (āˆƒ Ī» { z ā†’ x āˆˆ z and z āˆˆ y }) ā‰” x āˆˆ āˆŖ y
    _āŠ†_ : š•Š ā†’ š•Š ā†’ Set
    āŠ†-def : (x y : š•Š) ā†’ ((z : š•Š) ā†’ z āˆˆ x ā†’ z āˆˆ y) ā‰” x āŠ† y 
infixr 50 _āŠ†_
 
th-1 : (x y : š•Š) ā†’ x āŠ† y ā†’ (āˆŖ x) āŠ† (āˆŖ y)
th-1 x y z = straight (āŠ†-def (āˆŖ x) (āˆŖ y)) Ī» w i ā†’ straight (āˆŖ-def w y) (lm-1 w (back (āˆŖ-def w x) i))
    where lm-1 : (a : š•Š) ā†’ āˆƒ (Ī» { z ā†’ a āˆˆ z and z āˆˆ x }) ā†’ āˆƒ (Ī» { z ā†’ a āˆˆ z and z āˆˆ y })
          lm-1 a (exists b _ (c āˆ§ d)) = exists b (Ī» { z ā†’ a āˆˆ z and z āˆˆ y }) (c āˆ§ (back (āŠ†-def x y) z b d))

    I was able to done this proof. I had to add one data more. Several data blocks were wrong - now they are right - partly because of it I couldn't proof. Now I see Agda more convenient - I began to understand it more. I also added two auxiliary functions: straight and back.

    It's sad that the answers are hard to find on the topic of Agda(

    -----edited------

    It is possible sometimes to use only functions. For example

    postulate
    _and_ : Set ā†’ Set ā†’ Set
    and-def : {x y : Set} ā†’ x ā†’ y ā†’ x and y
    right : {x y : Set} ā†’ x and y ā†’ y
    left : {x y : Set} ā†’ x and y ā†’ x

    But, in the end, I came to use data. Functions don't allow to introduce parameters not in implication. For example we cannot write something like this

    data āˆƒ : {x : Set} ā†’ (z : x ā†’ Set) ā†’ Set where
    c-āˆƒ : {x : Set} ā†’ (y : x) ā†’ (z : x ā†’ Set) ā†’ z y ā†’ āˆƒ z
āˆƒ-element : {x : Set} ā†’ (z : x ā†’ Set) ā†’ āˆƒ z ā†’ (and-def (y : x) (z y))

    It produces parse error at "y : x".