如何在Agda中证明Test true false类型不可居？

你之前的模式匹配尝试失败，核心原因是indirect构造器的中间参数j1可以取任意Bool值，Agda无法通过固定j1的两个可能值来覆盖所有情况。必须对Test的结构进行归纳证明——这和你猜测的基于构造器深度的归纳思路一致，具体实现可以分两种方式：

方式一：借助单调性辅助引理（更清晰） #

首先定义Bool上的自然序，然后证明所有Test a b的实例都满足a ≤ b（即true不可能指向false）：

1. 定义Bool的≤关系 #

open import Relation.Binary
open import Data.Bool
open import Data.Empty

data _≤_ : Bool → Bool → Set where
  ff : false ≤ false
  ft : false ≤ true
  tt : true ≤ true

2. 证明Test的单调性引理 #

对Test的构造器进行归纳，验证每个构造出来的关系都符合a ≤ b：

test-monotonic : ∀ {a b} → Test a b → a ≤ b
test-monotonic direct = ft  -- direct对应false→true，符合false ≤ true
test-monotonic (indirect p q) with test-monotonic p | test-monotonic q
... | ff | ff = ff
... | ff | ft = ft
... | ff | tt = ft  -- 实际不会出现：p是false→false的话，不存在这样的Test实例
... | ft | tt = ft  -- false→true 传递 true→true，结果还是false→true
... | tt | tt = tt  -- true→true 传递 true→true，结果还是true→true

3. 完成不可居证明 #

如果存在Test true false，根据引理会导出true ≤ false，但这个类型没有任何构造器，直接用空类型消除器即可：

testNot : ¬ Test true false
testNot t with test-monotonic t
... | ()  -- true ≤ false无对应构造器，用洞排除所有可能

方式二：直接对Test结构归纳（更简洁） #

不引入辅助引理，直接递归处理Test true false的所有可能构造：

testNot : ¬ Test true false
-- 排除direct构造器：direct是Test false true，不可能匹配Test true false
testNot direct = ⊥-elim impossible
  where impossible : false ≡ true → ⊥
        impossible ()
-- 处理indirect构造器：indirect p q : Test true false 意味着 q : Test j1 false
testNot (indirect p q) = testNot q

这里的逻辑是：

• 若indirect p q是Test true false，则q必须是Test j1 false；
• 若j1为false，Test false false无法被任何构造器生成；
• 若j1为true，q就是Test true false，递归调用testNot q即可终止（因为Test的构造深度有限，没有无限递归的构造器）。

为什么你之前的写法不生效？ #

你尝试固定indirect的j1为false或true，但Agda无法确认这两个模式覆盖了所有情况——每个模式只处理了j1的一个取值，且Agda无法自动合并这两个子句为完整覆盖。而归纳法则通过递归处理所有构造深度的实例，完美解决了这个问题。

内容的提问来源于stack exchange，提问作者Sam_W