Proving a theorem using equality relation: ∀[ x ] ∀[ y ] (¬ Eq x y → ¬ Eq (f x) (f y))

Question

I am trying to solve the following first order logic problem using Agda:

  problem : {A B : Set} {f : A → B} → inj f → ∀[ x ] ∀[ y ] (¬ Eq x y → ¬ Eq (f x) (f y))

using the following definitions of equality relations and some supporting defintions:

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

infix 3 ¬_ 
¬_ : Set → Set
¬ A = A → ⊥

Π : (A : Set) → (B : A → Set) → Set
Π A B = (a : A) → B a

forAll : {A : Set} → (B : A → Set) → Set
forAll {A} B = Π A B

∀-syntax = forAll
infix 0 ∀-syntax
syntax ∀-syntax (λ a → B) = ∀[ a ] B

apply : {A : Set} → {B : A → Set} → Π A B → (a : A) → B a
apply f x = f x

data Σ (A : Set) (B : A → Set) : Set where
    ⟨_,_⟩ : (a : A) → B a → Σ A B

thereExists : ∀ {A : Set} (B : A → Set) → Set
thereExists {A} B = Σ A B

∃-syntax = thereExists
infix 0 ∃-syntax
syntax ∃-syntax (λ x → B) = ∃[ x ] B

∃-elim : {A : Set} {B : A → Set} {C : Set} → (∀ (a : A) → B a → C) → Σ A B → C
∃-elim a→b→c ⟨ a , b ⟩ = a→b→c a b

dfst : {A : Set} {B : A → Set} → Σ A B → A
dfst ⟨ a , _ ⟩ = a

dsnd : {A : Set} {B : A → Set} → (p : Σ A B) → B (dfst p)
dsnd ⟨ _ , b ⟩ = b

module IFOL 
    (Eq : {A : Set} → A → A → Set) 
    (subst : {A B : Set} → (f : A → B) → ∀[ a1 ] ∀[ a2 ] (Eq a1 a2 → Eq (f a1) (f a2))) 
    (trans : {A : Set} → (a1 a2 a3 : A) → Eq a1 a2 → Eq a2 a3 → Eq a1 a3) 
  where

  inj : {A B : Set} → (A → B) → Set
  inj {A} {B} f = ∀[ a1 ] ∀[ a2 ] (Eq (f a1) (f a2) → Eq a1 a2)

  surj : {A B : Set} → (A → B) → Set
  surj {A} {B} f = ∀[ b ] ∃[ a ] Eq (f a) b

  infix 20 _∘_
  _∘_ : {A B C : Set} → (A → B) → (B → C) → A → C
  (f ∘ g) a = g (f a)

My approach to solve it has been the following:

problem : {A B : Set} {f : A → B} → inj f → ∀[ x ] ∀[ y ] (¬ Eq x y → ¬ Eq (f x) (f y))
problem injf x y noteqxy eqfxfy = noteqxy ?

However, I am stuck in there and can't work out further a solution that will let me get the goal Eq x y. I've tried using injf function in multiple ways but the main problem seems to be that I don't know how to return a function type.

As this is a student assignment I am working on, I am not asking for a solution, only for a guidance as to how I should progress with that solution (is this the right direction? should I use subst or trans in my solution?).

user_8988486 · Answer

It's quite hard to help you out without giving you the solution, for it is very short, but I shall try.

HINT 1 : you don't need either subst nor trans

HINT 2 : the solution is just a simple combination of the elements in the context

HINT 3 : If you want to give back a function, as your sentence

but the main problem seems to be that I don't know how to return a function type.

suggests, you need to remove the parameter eqfxfy and use the dependent version of _∘_ which is not the one you defined. You can find such definition in the standard library file Function.agda but I suppose you don't intend to use any import from the std lib. However, I don't see why you should do such thing, because giving back a function from A to B is the same as giving back an element of B with the addition of a parameter of type A, which is what you were going for, since you added the parameter eqfxfy.

HINT 4 : asking Agsy to build the term for you using CTRL-C CTRL-A provides you with the solution, which you could try and understand afterwards

Proving a theorem using equality relation: ∀[ x ] ∀[ y ] (¬ Eq x y → ¬ Eq (f x) (f y))

1 Answers