[Agda] Re: How to solve goals that involve a vertical bar?

Martin Stone Davis martin.stone.davis at gmail.com
Sun Jan 17 07:31:04 CET 2016


I've solved my own problem: it turned out that I needed a supporting lemma.
The below sketches the idea: lemma-hard cannot be proved without the
supporting lemma-easy.

  module VerticalBarProblemSolved where
    open import Data.Bool.Base using (Bool ; true ; false)
    open import Data.Product using (∃ ; _,_)
    open import Relation.Nullary using (yes ; no)
    open import Relation.Binary using (IsDecEquivalence)
    open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
    open import Data.Nat.Base using (ℕ ; suc)
    open import Data.Empty using (⊥-elim)

    module _ {isDecEquivalence : IsDecEquivalence {A = ℕ} _≡_} where
      open IsDecEquivalence isDecEquivalence using (_≟_)

      sucIffTrue : ℕ → Bool → ℕ
      sucIffTrue n true = suc n
      sucIffTrue n false with n ≟ n
      sucIffTrue n false | yes refl = n
      sucIffTrue n false | no n≢n = n

      lemma-easy : (n : ℕ) → sucIffTrue n false ≡ n
      lemma-easy n with n ≟ n
      lemma-easy n | yes refl = refl
      lemma-easy n | no n≢n = refl

      lemma-hard : (n : ℕ) → ∃ λ (b : Bool) → sucIffTrue n b ≡ n
      lemma-hard n = false , lemma-easy n


--
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 Sat, Jan 16, 2016 at 7:49 PM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> Oops. Please ignore all the prior emails. It turns out that my second and
> third emails were cases in which case-splitting on the with-abstraction
> makes the vertical-bar go away!
>
> Sorry about that. I will come up with a simpler example in which the
> problem arises before I post again.
>
> --
> 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 Sat, Jan 16, 2016 at 7:35 PM, Martin Stone Davis <
> martin.stone.davis at gmail.com> wrote:
>
>> 1000 apologies for not doing this before asking in the first place: I've
>> *considerably* shortened the code.
>>
>>   module Map0WIP'' {K : Set} where
>>
>>     open import Data.Product
>>     open import Data.Maybe
>>     open import Relation.Binary
>>     open import Relation.Binary.PropositionalEquality
>>
>>     module _ {isDecEquivalence : IsDecEquivalence {A = K} _≡_} where
>>       open IsDecEquivalence isDecEquivalence using (_≟_)
>>
>>       get : K → Maybe K → K
>>       get 𝑘 nothing = 𝑘
>>       get 𝑘 (just k₀) with k₀ ≟ 𝑘
>>       ... | kk = k₀
>>
>>       put : (k₀ : K) → ∃ λ (m₀ : Maybe K) → get k₀ m₀ ≡ k₀
>>       put k₀ with k₀ ≟ k₀
>>       put k₀ | k₀≟k₀ = just k₀ , {!!}
>>
>>
>> --
>> 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 Sat, Jan 16, 2016 at 11:20 AM, Martin Stone Davis <
>> martin.stone.davis at gmail.com> wrote:
>>
>>> 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/9de8ba65/attachment-0001.html


More information about the Agda mailing list