[Agda] Re: How to solve goals that involve a vertical bar?
Martin Stone Davis
martin.stone.davis at gmail.com
Sat Jan 16 20:20:09 CET 2016
FWIW, here is a shorter version of the same problem:
module Map0WIP' {K : Set} where
open import Data.Product
open import Data.Sum
open import Data.Maybe
open import Data.Empty
open import Relation.Nullary.Negation
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
record _∉_ (𝑘 : K) (m₀ : Maybe K) : Set where
inductive
field
un∉ : m₀ ≡ nothing ⊎
∃ λ m₁ → 𝑘 ∉ m₁ ×
∃ λ k₀ → k₀ ≢ 𝑘 ×
∃ λ (k₀∉m₁ : k₀ ∉ m₁)
→ m₀ ≡ just k₀
_∈_ : (𝑘 : K) (m₀ : Maybe K) → Set
𝑘 ∈ m₀ = ¬ 𝑘 ∉ m₀
here : ∀ {k₀ : K} → k₀ ∈ just k₀
here record { un∉ = (inj₁ ()) }
here record { un∉ = inj₂ (_ , _ , _ , k₀≢k₀ , _ , refl) } = ⊥-elim
(k₀≢k₀ refl)
module _ {isDecEquivalence : IsDecEquivalence {A = K} _≡_} where
open IsDecEquivalence isDecEquivalence using (_≟_)
get : ∀ {𝑘 : K} {m₀ : Maybe K} (𝑘∈m₀ : 𝑘 ∈ m₀) → K
get {𝑘} {m₀ = nothing} 𝑘∈m₀ = 𝑘
get {𝑘} {just k₀} 𝑘∈m₀ with k₀ ≟ 𝑘
get {𝑘} {just k₀} 𝑘∈m₀ | kk = k₀
put : (k₀ : K) → (m₁ : Maybe K) → k₀ ∉ m₁ → ∃ λ (m₀ : Maybe K) → ∃ λ
(k₀∈m₀ : k₀ ∈ m₀) → get k₀∈m₀ ≡ k₀
put k₀ m₁ k₀∉m₁ with k₀ ≟ k₀
put k₀ m₁ k₀∉m₁ | kk = just k₀ , here , {!!}
--
Martin Stone Davis
Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
On Fri, Jan 15, 2016 at 7:05 PM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:
> In the hole of the function 'put' (see code below), Agda reports that the
> goal is
>
> (get {α} {K} V {isDecEquivalence} {k₀}
>> {.Sandbox.Record.Map0WIP.recCon-NOT-PRINTED
>> (.Sandbox.Record.Map0WIP.recCon-NOT-PRINTED
>> (inj₂ (k₀ , v₀ , m₁ , k₀∉m₁)))}
>> here
>> | k₀ ≟ k₀)
>> ≡ v₀
>>
>
> I have tried invoking a with-abstraction on k₀ ≟ k₀ but to no avail: the
> vertical bar remains. TIA for any help resolving this.
>
> CODE BEGINS
> open import Level
> open import Relation.Binary.Core
> open import Data.Product
> open import Data.Sum
> open import Data.Unit.Base
>
> record Maybe {α} (A : Set α) : Set α where
> field
> unmaybe : ⊤ ⊎ A
>
> nothing : ∀ {α} {A : Set α} → Maybe A
> nothing = record { unmaybe = inj₁ tt }
>
> just : ∀ {α} {A : Set α} (a : A) → Maybe A
> just a = record { unmaybe = inj₂ a }
>
> mutual
> record Map : Set α where
> inductive
> field
> unmap : Maybe (∃ λ k₀ → V k₀ × ∃ λ m₁ → k₀ ∉ m₁)
>
> record _∉_ (𝑘 : K) (m₀ : Map) : Set α where
> inductive
> field
> un∉ : m₀ ≡ record { unmap = nothing } ⊎
> ∃ λ m₁ → 𝑘 ∉ m₁ ×
> ∃ λ k₀ → k₀ ≢ 𝑘 ×
> ∃ λ (k₀∉m₁ : k₀ ∉ m₁) → ∃ λ v₀
> → m₀ ≡ record { unmap = just (k₀ , v₀ , m₁ , k₀∉m₁) }
>
> open import Data.Empty
> open import Relation.Nullary.Negation
> open import Relation.Nullary
>
> _∈_ : (𝑘 : K) (m₀ : Map) → Set α
> 𝑘 ∈ m₀ = ¬ 𝑘 ∉ m₀
>
> pattern ∅ = record { unmap = record { unmaybe = inj₁ tt } }
> pattern M⟦_+_⋆_∣_⟧ m₁ k₀ v₀ k₀∉m₁ = record { unmap = record { unmaybe
> = inj₂ (k₀ , v₀ , m₁ , k₀∉m₁) } }
> pattern M⟦_+_∣_⟧ m₁ v₀ k₀∉m₁ = record { unmap = record { unmaybe =
> inj₂ (_ , v₀ , m₁ , k₀∉m₁) } }
> pattern M⟦_⋆_∣_⟧ k₀ v₀ k₀∉m₁ = record { unmap = record { unmaybe =
> inj₂ (k₀ , v₀ , _ , k₀∉m₁) } }
> pattern M⟦_∣_⟧ v₀ k₀∉m₁ = record { unmap = record { unmaybe = inj₂ (_
> , v₀ , _ , k₀∉m₁) } }
>
> pattern ∉∅ = record { un∉ = (inj₁ refl) }
> pattern ¬∉∅ = record { un∉ = (inj₁ ()) }
> pattern ∉⟦_/_⟧ 𝑘∉m₁ k₀≢𝑘 = record { un∉ = inj₂ (_ , 𝑘∉m₁ , _ ,
> k₀≢𝑘 , _ , _ , refl) }
>
> here : ∀ {k₀ : K} {v₀ : V k₀} {m₁ : Map} {k₀∉m₁ : k₀ ∉ m₁} → k₀ ∈ M⟦
> v₀ ∣ k₀∉m₁ ⟧
> here ¬∉∅
> here ∉⟦ _ / k₀≢k₀ ⟧ = ⊥-elim (k₀≢k₀ refl)
>
> infixl 40 _⊂_∣_
> _⊂_∣_ : Map → Map → (K → Set α) → Set α
> m ⊂ m' ∣ c = ∀ {𝑘} → c 𝑘 → 𝑘 ∉ m' → 𝑘 ∉ m
>
> shrink : ∀ {k₀ v₀ m₁ k₀∉m₁} → M⟦ m₁ + v₀ ∣ k₀∉m₁ ⟧ ⊂ m₁ ∣ λ 𝑘 → k₀ ≢
> 𝑘
> shrink k₀≢𝑘 ∉∅ = ∉⟦ ∉∅ / k₀≢𝑘 ⟧
> shrink k₀≢𝑘 ∉⟦ 𝑘∉m₀ / k₁≢𝑘 ⟧ = ∉⟦ shrink k₁≢𝑘 𝑘∉m₀ / k₀≢𝑘 ⟧
>
> somewhere : ∀ {𝑘 k₀ v₀ m₁ k₀∉m₁} → 𝑘 ∈ M⟦ m₁ + v₀ ∣ k₀∉m₁ ⟧ → k₀ ≢
> 𝑘 → 𝑘 ∈ m₁
> somewhere 𝑘∈m₀ k₀≢𝑘 𝑘∉m₁ = contradiction (shrink k₀≢𝑘 𝑘∉m₁) 𝑘∈m₀
>
> open import Relation.Binary
> open import Relation.Binary.PropositionalEquality
> module _ {isDecEquivalence : IsDecEquivalence {A = K} _≡_} where
> open IsDecEquivalence isDecEquivalence using (_≟_)
>
> get : ∀ {𝑘 : K} {m₀ : Map} (𝑘∈m₀ : 𝑘 ∈ m₀) → V 𝑘
> get {m₀ = ∅} 𝑘∈m₀ = contradiction ∉∅ 𝑘∈m₀
> get {𝑘} {M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧} 𝑘∈m₀ with k₀ ≟ 𝑘
> get {𝑘} {M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧} 𝑘∈m₀ | yes k₀≡𝑘 rewrite k₀≡𝑘
> = v₀
> get {𝑘} {M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧} 𝑘∈m₀ | no k₀≢𝑘 = get
> (somewhere 𝑘∈m₀ k₀≢𝑘)
>
> put : (k₀ : K) → (v₀ : V k₀) (m₁ : Map) → k₀ ∉ m₁ → ∃ λ (m₀ : Map) →
> ∃ λ (k₀∈m₀ : k₀ ∈ m₀) → get k₀∈m₀ ≡ v₀
> put k₀ v₀ m₁ k₀∉m₁ = M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧ , here , {!!}
>
> CODE ENDS
>
> --
> Martin Stone Davis
>
> Postal/Residential:
> 1223 Ferry St
> Apt 5
> Eugene, OR 97401
> Talk / Text / Voicemail: (310) 699-3578 <3106993578>
> Electronic Mail: martin.stone.davis at gmail.com
> Website: martinstonedavis.com
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160116/95a4879f/attachment.html
More information about the Agda
mailing list