Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison BAlgbra.agda @ 369:17adeeee0c2a
fix Select and Replace
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 19 Jul 2020 10:02:43 +0900 |
parents | 2a8a51375e49 |
children | 6c72bee25653 |
comparison
equal
deleted
inserted
replaced
368:30de2d9b93c1 | 369:17adeeee0c2a |
---|---|
1 {-# OPTIONS --allow-unsolved-metas #-} | |
1 open import Level | 2 open import Level |
2 open import Ordinals | 3 open import Ordinals |
3 module BAlgbra {n : Level } (O : Ordinals {n}) where | 4 module BAlgbra {n : Level } (O : Ordinals {n}) where |
4 | 5 |
5 open import zf | 6 open import zf |
53 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A | 54 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A |
54 (record { proj1 = case1 refl ; proj2 = subst (λ k → odef A k) (sym diso) A∋x})) | 55 (record { proj1 = case1 refl ; proj2 = subst (λ k → odef A k) (sym diso) A∋x})) |
55 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B | 56 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B |
56 (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x})) | 57 (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x})) |
57 | 58 |
58 ∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) | 59 ∩-Select : { A B : HOD } → Select A ( λ x _ → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) |
59 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | 60 ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
60 lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x | 61 lemma1 : {x : Ordinal} → odef (Select A (λ x₁ _ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x |
61 lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) } | 62 lemma1 {x} lt = record { proj1 = proj1 {!!} ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 {!!} )) } |
62 lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x | 63 lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ _ → (A ∋ x₁) ∧ (B ∋ x₁))) x |
63 lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 = | 64 lemma2 {x} lt = {!!} -- record { proj1 = proj1 lt ; proj2 = |
64 record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } } | 65 -- record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } } |
65 | 66 |
66 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) | 67 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) |
67 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | 68 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
68 lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x | 69 lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x |
69 lemma1 {x} lt with proj2 lt | 70 lemma1 {x} lt with proj2 lt |