利用平等关系证明定理：∀[ x ]∀[ y ] (¬ Eq x y →¬ Eq (f x) (f y))

Question

我试图用Agda.NET来解决以下一阶逻辑问题。

  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：如果你想回馈一个函数，就像你的句子一样。

但主要问题似乎是我不知道如何返回一个函数类型。

建议，你需要删除参数 eqfxfy 并使用附属版本的 _∘_ 而不是你定义的那个。您可以在标准库文件 Function.agda 但我想你并不打算使用任何来自std lib的导入。但是，我不明白为什么要这样做，因为把一个函数从 A 回传给 B 等于把 B 中的一个元素回传给你，只是增加了一个 A 类型的参数，而这正是你要做的，因为你添加了参数 eqfxfy.

提示4：要求Agsy用CTRL-C CTRL-A为你建立术语，为你提供解法，你可以尝试着理解之后的解法