[Agda] proprietà dell'equipotenza

Messaggioda caulacau » 15/07/2019, 20:49

La relazione di equipotenza tra due tipi in Agda si definisce così:

Codice:
record _⇔_ (A B : Set) : Set where
  constructor Bijection
  field
    A→B : A → B
    B→A : B → A
    A→B→A : ∀ (a : A) → B→A (A→B a) ≡ a
    B→A→B : ∀ (b : B) → A→B (B→A b) ≡ b

open _⇔_


Sarebbe bello, ora, saper dimostrare almeno che A ⇔ A. In effetti è sufficiente dimostrare che

Codice:
Idempotent : ∀ {a} → (a → a) → Set
Idempotent f = ∀ b → f (f b) ≡ f b

idIdem : ∀ a → Idempotent (id {A = a})
idIdem _ _ = refl

per poter poi dire

Codice:
⇔-refl : ∀ {A : Set} → A ⇔ A
⇔-refl = Bijection id id idIdem idIdem


Purtroppo però non funziona, e non riesco a interpretare l'errore che ricevo, che è chiaramete un type-mismatch, ma che non so come correggere perché a me sembra giusto:

Codice:
A !=< Set of type Set
when checking that the expression id∘id=id has type (a : A) → a ≡ a


(PS: davvero questo obbrobrio verde vomito è l'unica maniera di inserire degli snippet di codice?)
Avatar utente
caulacau
Junior Member
Junior Member
 
Messaggio: 151 di 233
Iscritto il: 08/05/2019, 18:30

Re: [Agda] proprietà dell'equipotenza

Messaggioda Indrjo Dedej » 17/07/2019, 09:29

Riporta il testo dell'errore che ricevi. Anche se laconico, qualcuno potrà aiutarti più facilmente.
Io non sono uomo, sono dinamite. ~ Nietzsche
Avatar utente
Indrjo Dedej
Average Member
Average Member
 
Messaggio: 736 di 788
Iscritto il: 31/05/2016, 19:58
Località: Milano

Re: [Agda] proprietà dell'equipotenza

Messaggioda caulacau » 17/07/2019, 10:07

Alla fine ci sono riuscito, ma ho un altro problema.

Intanto, sono riuscito a dimostrare che l'equipotenza è una relazione di equivalenza.

Codice:
id : ∀ {A : Set} → A → A
id x = x

Idempotent : ∀ {a} → (a → a) → Set
Idempotent f = ∀ b → f (f b) ≡ f b

idIdem : ∀ a → Idempotent (id {A = a})
idIdem _ _ = refl

⇔-refl : ∀ {A : Set} → A ⇔ A
⇔-refl = Bijection id id (idIdem _) (idIdem _)

E per la proprietà simmetrica,
Codice:
⇔-sym : ∀ {A B : Set} → A ⇔ B → B ⇔ A
⇔-sym (Bijection f g gf=id fg=id) = Bijection g f fg=id gf=id

E per la proprietà transitiva, che com'era giusto aspettarsi è la più dura, servono due lemmi preliminari:
Codice:
oneId : ∀ {A B C : Set}
  (f : A → B) →
  (g : B → A) →
  (u : B → C) →
  (v : C → B) →
  (vu=id : ∀ x → v (u x) ≡ x)
  (gf=id : ∀ x → g (f x) ≡ x)
  (a : A) →
  g (v (u (f a))) ≡ a
oneId f g u v vu=id gf=id x =
  begin
    g (v (u (f x)))
  ≡⟨ cong' g (vu=id (f x)) ⟩
    g (f x)
  ≡⟨ gf=id x ⟩
    x
  ∎

otherId : ∀ {A B C : Set}
  (f : A → B) →
  (g : B → A) →
  (u : B → C) →
  (v : C → B) →
  (fg=id : ∀ x → f (g x) ≡ x)
  (uv=id : ∀ x → u (v x) ≡ x)
  (c : C) →
  u (f (g (v c))) ≡ c
otherId f g u v fg=id uv=id c =
  begin
    u (f (g (v c)))
  ≡⟨ cong' u (fg=id (v c)) ⟩
    u (v c)
  ≡⟨ uv=id c ⟩
    c
  ∎

-- Task 1-3. Prove that _⇔_ relation is transitive.
⇔-trans : ∀ {A B C : Set} → A ⇔ B → B ⇔ C → A ⇔ C
⇔-trans (Bijection f g gf=id fg=id) (Bijection u v vu=id uv=id) =
  Bijection (u o f) (g o v) (oneId f g u v vu=id gf=id) (otherId f g u v fg=id uv=id)
Avatar utente
caulacau
Junior Member
Junior Member
 
Messaggio: 157 di 233
Iscritto il: 08/05/2019, 18:30


Torna a Informatica

Chi c’è in linea

Visitano il forum: Nessuno e 13 ospiti