[Agda] with x =? x

[Sergei Meshveliani]

On Wed, 2014-12-31 at 18:26 +0100, Andrea Vezzosi wrote:
> You could prove that  "x ≟ x" equals "yes refl" in a separate lemma
> (by using "with x ≟ x") and use rewrite with that lemma in foo,
> that way you don't have to care about the "no .." case there.

I have  x : K,  _≈_ and _≟_  on K  (of a DecSetoid over Carrier = K).
And try you suggestion: 

  x≟x≡yes : (x : K) → (x ≟ x) ≡ (yes ≈refl)
  x≟x≡yes x  with x ≟ x
  ...             | yes x≈x =  ...PropositionalEquality.refl
  ...             | no x≉x  =  ⊥-elim $ x≉x ≈refl

This is not type-checked. 
I do not know, something needs to be fixed here ... 

Regards,

------
Sergei


> On Wed, Dec 31, 2014 at 3:31 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > People,
> > I discover that Agda requires even  " with k ≟ k" :
> >
> >   foo : .. -> ins (k , v) (ins (k , u) ps)  =pn  ins (k , comb k v u) ps
> >
> >   foo {k} {u} {v} {[]}  with k ≟ k
> >   ...                 | yes _  =  =pn-refl          -- instance of  refl
> >   ...                 | no k≉k =  ⊥-elim $ k≉k ≈refl
> >
> > _=pn_ is the pointwise equality for lists of certain pairs, when pairs
> > are compared by a certain _=p_.
> > ins  inserts a pair into a list "by the key". It compares  k ≟ k',  and
> > acts respectively.
> > And in  foo,   ins  is applied with   k for k'.
> >
> > And a mere  " =pn-refl"  is not sufficient!
> > I have satisfied `ins' only with `with'.
> >
> > This looks like a minor feature, but still:
> > is there a way to write nicer proofs than by using  "with x ≟ x"
> > ?
> >
> > Thanks,
> >
> > ------
> > Sergei
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>