Início / coding / Perguntas / 77674687
Accepted
lemongyros
Asked: 2023-12-17 22:02:17 +0800 CST

Agda provando Bool ≢ ⊤

  • 772

Então esse é o problema que tenho em uma tarefa de casa, tenho que provar que bool não é igual a top, também tenho um sinal de igual redefinido que devo usar.

module TranspEq where

open import Agda.Primitive
open import Agda.Builtin.Equality renaming (_≡_ to _≡ᵣ_ ; refl to reflᵣ)
open import Agda.Builtin.Nat renaming (Nat to ℕ)

_≡_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
_≡_ {A = A} a b = ∀{κ}(P : A → Set κ) → P a → P b

infix 4 _≡_

-- define conversion between the two 'equals'
transp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ b → a ≡ᵣ b
transp a b x = x (_≡ᵣ_ a) reflᵣ

untransp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ᵣ b → a ≡ b
untransp a .a reflᵣ P y = y

-- prove properties of ≡

refl : ∀{ℓ}{A : Set ℓ}{a : A} → a ≡ a
refl P a = a

sym : ∀{ℓ}{A : Set ℓ}{a b : A} → a ≡ b → b ≡ a
sym {l} {A} {a} {b} = λ z P → z (λ z₁ → (x : P z₁) → P a) (λ x → x)

trans : ∀{ℓ}{A : Set ℓ}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans = λ a b P c → b P (a P c)

cong : ∀{ℓ κ}{A : Set ℓ}{B : Set κ}(f : A → B){a b : A} → a ≡ b → f a ≡ f b
cong = λ f a P → a (λ b → P (f b))

-- types
record ⊤ : Set where
  instance constructor tt

data Bool : Set where
  true : Bool
  false : Bool

data ⊥ : Set where

_≢_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
a ≢ b = a ≡ b → ⊥

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ = {!!}

Eu tentei algo assim, mas sim, não consegui:/não consigo criar um predicado que seja Set -> Set


⊤≠⊥ : ⊤ ≢ ⊥ 
⊤≠⊥ x = x (λ x → x) tt
 

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ x = ⊤≠⊥ λ P y → {!   !}
--Bool≠⊤ : Bool ≢ ⊤
--Bool≠⊤ x = x (λ y → y tt) p
--    where
--    p : {Set : (Bool ≡ ⊤)}→ ⊥
--    p (true ≡ tt) = ⊥
--    p (false ≡ tt) = ⊥
functional-programming

2 respostas

  1. Best Answer

    A única maneira de provar que dois conjuntos são diferentes em Agda é explorar as suas diferenças em termos de cardinalidade.

    No caso de Boole ⊤isso é particularmente útil para explorar, porque cada elemento de ⊤é igual a todos os outros elementos dele, o que não é verdade para Bool( truenão é igual a false). Portanto, tudo que você precisa é

    Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ x with sym x (λ A -> (x y : A) -> x ≡ᵣ y) (λ _ _ -> reflᵣ) true false
... | ()
    • 1

  2. O primeiro passo é pensar em um predicado P : Set → Settal que P Boolseja habitado e P ⊤refutável, ou vice-versa. Agda não vai te ajudar muito na escolha de um bom porque Set → Seté um tipo muito vago, com muitos habitantes (a maioria deles inúteis para você). Deixarei esta escolha Pprincipalmente como um exercício, mas darei algumas dicas, visto que acho que encontrar tal Pé o ponto principal desta questão do dever de casa.

    Na verdade, achei mais fácil fazer o contrário – escolher um Pwith P ⊤but P Bool → ⊥. Ao produzir tal P, você normalmente usará T : Setuma abstração λ. Isso Tserá instanciado para ⊤e Boolpela definição de _≡_. Com isso T, você pode quantificar universalmente os elementos usando (x : T) → .... Se você conheceu os tipos Σ (pares dependentes), poderá usá-los para quantificação existencial, embora eu finalmente tenha encontrado uma propriedade que precisava apenas de quantificação universal. Você não pode usar _≡_para produzir o necessário Setdevido a problemas de tamanho, mas pode usar _≡ᵣ_em seu lugar. Você não pode combinar padrões Tcom seus habitantes, porque eles não são dataourecordtipo.

    Eu precisava de um lema true≢ᵣfalse : true ≡ᵣ false → ⊥. Eu provei isso por meio de correspondência de padrões absurda ( ()), mas também deve ser provado untranspe definido uma propriedade de booleanos que é verdadeira truee falsa de false. Essa propriedade é mais fácil de definir, no sentido de que é do tipo Bool → Set, para que você possa combinar padrões no Boolargumento.

    A prova resultante deve ser semelhante à seguinte. Eu recomendaria começar com just true≢ᵣfalse ?e preencher Pand p, que informará quantos argumentos sym q P pdevem ser necessários.

    Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ q = true≢ᵣfalse (sym q P p {- instantiation of universal quantifiers -})
  where
  P : Set → Set
  P T = ?

  p : P ⊤
  p = ?
    • 0

relate perguntas