<div dir="ltr">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. <br><br> module VerticalBarProblemSolved where<br> open import Data.Bool.Base using (Bool ; true ; false)<br> open import Data.Product using (∃ ; _,_)<br> open import Relation.Nullary using (yes ; no)<br> open import Relation.Binary using (IsDecEquivalence)<br> open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)<br> open import Data.Nat.Base using (ℕ ; suc)<br> open import Data.Empty using (⊥-elim)<br> <br> module _ {isDecEquivalence : IsDecEquivalence {A = ℕ} _≡_} where<br> open IsDecEquivalence isDecEquivalence using (_≟_)<br><br> sucIffTrue : ℕ → Bool → ℕ<br> sucIffTrue n true = suc n<br> sucIffTrue n false with n ≟ n<br> sucIffTrue n false | yes refl = n<br> sucIffTrue n false | no n≢n = n<br><br> lemma-easy : (n : ℕ) → sucIffTrue n false ≡ n<br> lemma-easy n with n ≟ n<br> lemma-easy n | yes refl = refl<br> lemma-easy n | no n≢n = refl<br><br> lemma-hard : (n : ℕ) → ∃ λ (b : Bool) → sucIffTrue n b ≡ n<br> lemma-hard n = false , lemma-easy n<br><br></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
<br><div class="gmail_quote">On Sat, Jan 16, 2016 at 7:49 PM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>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! <br><br>Sorry about that. I will come up with a simpler example in which the problem arises before I post again.<br></div></div><div class="gmail_extra"><span class=""><br clear="all"><div><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
<br></span><div><div class="h5"><div class="gmail_quote">On Sat, Jan 16, 2016 at 7:35 PM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">1000 apologies for not doing this before asking in the first place: I've *considerably* shortened the code.<span><br><br> module Map0WIP'' {K : Set} where<br><br> open import Data.Product<br></span> open import Data.Maybe<span><br> open import Relation.Binary<br> open import Relation.Binary.PropositionalEquality<br><br> module _ {isDecEquivalence : IsDecEquivalence {A = K} _≡_} where<br> open IsDecEquivalence isDecEquivalence using (_≟_)<br><br></span> get : K → Maybe K → K<br> get 𝑘 nothing = 𝑘<br> get 𝑘 (just k₀) with k₀ ≟ 𝑘 <br> ... | kk = k₀<br><br> put : (k₀ : K) → ∃ λ (m₀ : Maybe K) → get k₀ m₀ ≡ k₀<br> put k₀ with k₀ ≟ k₀<br> put k₀ | k₀≟k₀ = just k₀ , {!!}<br><br></div><div class="gmail_extra"><span><br clear="all"><div><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
<br></span><div><div><div class="gmail_quote">On Sat, Jan 16, 2016 at 11:20 AM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">FWIW, here is a shorter version of the same problem:<br><br> module Map0WIP' {K : Set} where<span><br> open import Data.Product<br> open import Data.Sum<br></span> open import Data.Maybe<span><br> open import Data.Empty<br> open import Relation.Nullary.Negation<br> open import Relation.Nullary <br></span><span> open import Relation.Binary<br> open import Relation.Binary.PropositionalEquality<br><br></span> record _∉_ (𝑘 : K) (m₀ : Maybe K) : Set where<br> inductive<br> field<br> un∉ : m₀ ≡ nothing ⊎<span><br> ∃ λ m₁ → 𝑘 ∉ m₁ ×<br> ∃ λ k₀ → k₀ ≢ 𝑘 ×<br> ∃ λ (k₀∉m₁ : k₀ ∉ m₁) <br></span> → m₀ ≡ just k₀<br><br> _∈_ : (𝑘 : K) (m₀ : Maybe K) → Set<br> 𝑘 ∈ m₀ = ¬ 𝑘 ∉ m₀<br><br> here : ∀ {k₀ : K} → k₀ ∈ just k₀<br> here record { un∉ = (inj₁ ()) }<br> here record { un∉ = inj₂ (_ , _ , _ , k₀≢k₀ , _ , refl) } = ⊥-elim (k₀≢k₀ refl)<span><br><br> module _ {isDecEquivalence : IsDecEquivalence {A = K} _≡_} where<br> open IsDecEquivalence isDecEquivalence using (_≟_)<br><br></span> get : ∀ {𝑘 : K} {m₀ : Maybe K} (𝑘∈m₀ : 𝑘 ∈ m₀) → K<br> get {𝑘} {m₀ = nothing} 𝑘∈m₀ = 𝑘<br> get {𝑘} {just k₀} 𝑘∈m₀ with k₀ ≟ 𝑘 <br> get {𝑘} {just k₀} 𝑘∈m₀ | kk = k₀<br><br> put : (k₀ : K) → (m₁ : Maybe K) → k₀ ∉ m₁ → ∃ λ (m₀ : Maybe K) → ∃ λ (k₀∈m₀ : k₀ ∈ m₀) → get k₀∈m₀ ≡ k₀<br> put k₀ m₁ k₀∉m₁ with k₀ ≟ k₀<br> put k₀ m₁ k₀∉m₁ | kk = just k₀ , here , {!!}<br><br></div><div class="gmail_extra"><span><br clear="all"><div><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
<br></span><div><div><div class="gmail_quote">On Fri, Jan 15, 2016 at 7:05 PM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">In the hole of the function 'put' (see code below), Agda reports that the goal is<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">(get {α} {K} V {isDecEquivalence} {k₀}<br> {.Sandbox.Record.Map0WIP.recCon-NOT-PRINTED<br> (.Sandbox.Record.Map0WIP.recCon-NOT-PRINTED<br> (inj₂ (k₀ , v₀ , m₁ , k₀∉m₁)))}<br> here<br> | k₀ ≟ k₀)<br> ≡ v₀<br></blockquote><div><br></div><div>I have tried invoking a with-abstraction on k₀ ≟ k₀ but to no avail: the vertical bar remains. TIA for any help resolving this.<br><br>CODE BEGINS<br> open import Level<br> open import Relation.Binary.Core<br> open import Data.Product<br> open import Data.Sum<br> open import Data.Unit.Base<br><br> record Maybe {α} (A : Set α) : Set α where<br> field<br> unmaybe : ⊤ ⊎ A<br> <br> nothing : ∀ {α} {A : Set α} → Maybe A<br> nothing = record { unmaybe = inj₁ tt }<br> <br> just : ∀ {α} {A : Set α} (a : A) → Maybe A<br> just a = record { unmaybe = inj₂ a }<br> <br> mutual<br> record Map : Set α where<br> inductive<br> field<br> unmap : Maybe (∃ λ k₀ → V k₀ × ∃ λ m₁ → k₀ ∉ m₁)<br> <br> record _∉_ (𝑘 : K) (m₀ : Map) : Set α where<br> inductive<br> field<br> un∉ : m₀ ≡ record { unmap = nothing } ⊎<br> ∃ λ m₁ → 𝑘 ∉ m₁ ×<br> ∃ λ k₀ → k₀ ≢ 𝑘 ×<br> ∃ λ (k₀∉m₁ : k₀ ∉ m₁) → ∃ λ v₀<br> → m₀ ≡ record { unmap = just (k₀ , v₀ , m₁ , k₀∉m₁) }<br><br> open import Data.Empty<br> open import Relation.Nullary.Negation<br> open import Relation.Nullary <br><br> _∈_ : (𝑘 : K) (m₀ : Map) → Set α<br> 𝑘 ∈ m₀ = ¬ 𝑘 ∉ m₀<br><br> pattern ∅ = record { unmap = record { unmaybe = inj₁ tt } }<br> pattern M⟦_+_⋆_∣_⟧ m₁ k₀ v₀ k₀∉m₁ = record { unmap = record { unmaybe = inj₂ (k₀ , v₀ , m₁ , k₀∉m₁) } }<br> pattern M⟦_+_∣_⟧ m₁ v₀ k₀∉m₁ = record { unmap = record { unmaybe = inj₂ (_ , v₀ , m₁ , k₀∉m₁) } }<br> pattern M⟦_⋆_∣_⟧ k₀ v₀ k₀∉m₁ = record { unmap = record { unmaybe = inj₂ (k₀ , v₀ , _ , k₀∉m₁) } }<br> pattern M⟦_∣_⟧ v₀ k₀∉m₁ = record { unmap = record { unmaybe = inj₂ (_ , v₀ , _ , k₀∉m₁) } }<br> <br> pattern ∉∅ = record { un∉ = (inj₁ refl) }<br> pattern ¬∉∅ = record { un∉ = (inj₁ ()) }<br> pattern ∉⟦_/_⟧ 𝑘∉m₁ k₀≢𝑘 = record { un∉ = inj₂ (_ , 𝑘∉m₁ , _ , k₀≢𝑘 , _ , _ , refl) }<br><br> here : ∀ {k₀ : K} {v₀ : V k₀} {m₁ : Map} {k₀∉m₁ : k₀ ∉ m₁} → k₀ ∈ M⟦ v₀ ∣ k₀∉m₁ ⟧<br> here ¬∉∅<br> here ∉⟦ _ / k₀≢k₀ ⟧ = ⊥-elim (k₀≢k₀ refl)<br><br> infixl 40 _⊂_∣_<br> _⊂_∣_ : Map → Map → (K → Set α) → Set α<br> m ⊂ m' ∣ c = ∀ {𝑘} → c 𝑘 → 𝑘 ∉ m' → 𝑘 ∉ m<br><br> shrink : ∀ {k₀ v₀ m₁ k₀∉m₁} → M⟦ m₁ + v₀ ∣ k₀∉m₁ ⟧ ⊂ m₁ ∣ λ 𝑘 → k₀ ≢ 𝑘<br> shrink k₀≢𝑘 ∉∅ = ∉⟦ ∉∅ / k₀≢𝑘 ⟧<br> shrink k₀≢𝑘 ∉⟦ 𝑘∉m₀ / k₁≢𝑘 ⟧ = ∉⟦ shrink k₁≢𝑘 𝑘∉m₀ / k₀≢𝑘 ⟧<br> <br> somewhere : ∀ {𝑘 k₀ v₀ m₁ k₀∉m₁} → 𝑘 ∈ M⟦ m₁ + v₀ ∣ k₀∉m₁ ⟧ → k₀ ≢ 𝑘 → 𝑘 ∈ m₁<br> somewhere 𝑘∈m₀ k₀≢𝑘 𝑘∉m₁ = contradiction (shrink k₀≢𝑘 𝑘∉m₁) 𝑘∈m₀<br><br> open import Relation.Binary<br> open import Relation.Binary.PropositionalEquality<br> module _ {isDecEquivalence : IsDecEquivalence {A = K} _≡_} where<br> open IsDecEquivalence isDecEquivalence using (_≟_)<br><br> get : ∀ {𝑘 : K} {m₀ : Map} (𝑘∈m₀ : 𝑘 ∈ m₀) → V 𝑘<br> get {m₀ = ∅} 𝑘∈m₀ = contradiction ∉∅ 𝑘∈m₀<br> get {𝑘} {M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧} 𝑘∈m₀ with k₀ ≟ 𝑘 <br> get {𝑘} {M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧} 𝑘∈m₀ | yes k₀≡𝑘 rewrite k₀≡𝑘 = v₀<br> get {𝑘} {M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧} 𝑘∈m₀ | no k₀≢𝑘 = get (somewhere 𝑘∈m₀ k₀≢𝑘)<br><br> put : (k₀ : K) → (v₀ : V k₀) (m₁ : Map) → k₀ ∉ m₁ → ∃ λ (m₀ : Map) → ∃ λ (k₀∈m₀ : k₀ ∈ m₀) → get k₀∈m₀ ≡ v₀<br> put k₀ v₀ m₁ k₀∉m₁ = M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧ , here , {!!}<br></div><div><br>CODE ENDS<br></div><div><br clear="all"><div><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div></div>
</blockquote></div><br></div></div></div>
</blockquote></div><br></div></div></div>
</blockquote></div><br></div></div></div>
</blockquote></div><br></div>