logic - 使用等式关系证明定理 : ∀[ x ] ∀[ y ] (¬ Eq x y → ¬ Eq (f x) (f y))

Question

我正在尝试使用 Agda 解决以下一阶逻辑问题:

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

使用以下平等关系定义和一些支持定义:

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)

我解决这个问题的方法如下:

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 ?

但是，我被困在那里，无法进一步找到一个解决方案来让我实现目标Eq x y。我尝试过以多种方式使用 injf 函数，但主要问题似乎是我不知道如何返回函数类型。

由于这是我正在做的学生作业，我并不是要求解决方案，只是寻求关于我应该如何推进该解决方案的指导(这是正确的方向吗？我应该使用 subst 或 trans 在我的解决方案中？)。

Answer 1

如果不给你解决方案，很难帮助你，因为它很短，但我会尝试。

提示 1:您不需要 subst 也不需要 trans

提示 2:解决方案只是上下文中元素的简单组合

提示3:如果你想返回一个函数，如你的句子

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

建议，您需要删除参数eqfxfy并使用_∘_的依赖版本，该版本不是您定义的版本。您可以在标准库文件 Function.agda 中找到此类定义，但我想您不打算使用来自 std lib 的任何导入。但是，我不明白为什么你应该这样做，因为返回从 A 到 B 的函数与返回 B 的元素并添加 A 类型的参数相同，这就是你想要的，因为您添加了参数 eqfxfy。

提示 4:要求 Agsy 使用 CTRL-C CTRL-A 为您构建术语，为您提供解决方案，您可以稍后尝试并理解该解决方案