Inspect pattern needed? [Re: [Agda] Re: Agda bug]

[Andreas Abel]

I looked at your proof, but already the first step fails (in your 
original proof, the zeroth step).

idempotent (v ∷ dom) rng (mkSubs {.v} {τ₀} {.dom} {.rng} vsτ₀⊆rng s' 
(v∉dom , v∉rng , dom∩̸rng)) (Var .v) | (yes refl) rewrite (lemRepVar₀ v τ₀) =
   begin
    apply s' (replace v τ₀ (apply s' τ₀))
       ≡⟨⟩
    apply (mkSubs vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (apply (mkSubs 
vsτ₀⊆rng s' (v∉dom , v∉rng , dom∩̸rng)) (Var v))
       ≡⟨ {!!} ⟩
    apply s' τ₀
   ∎

[I do not see why the lemma lemRepVar_0 would help here, since replace 
is applied to (apply s tau_0); it is the same without the rewrite step.]

Looks like you need inspect (on steroids) to complete your proof, a 
simple "with" seems not sufficient.   You will probably need a proof that

   v =?= v'  \equiv  yes refl

that is what the inspect-pattern can provide you with.

Cheers,
Andreas

On 11.01.2014 02:13, Carlos Camarao wrote:
> On Wed, Nov 6, 2013 at 3:14 PM, Carlos Camarao <carlos.camarao at gmail.com
> <mailto:carlos.camarao at gmail.com>> wrote:
>
>     I am trying to write in Agda the simplest piece of code I can for
>     proving soundness and completeness of a most general unification
>     function; I think this is a good, instructive example of a problem that
>     should have a simple but non-structurally recursive solution.
>
>     ...
>
>
> Hi. I am continuing to work on this. I have defined "idempotence" (an
> essential property of unifiers according to which):  for all unifier s
> and type τ, apply s (apply s τ) ≡ apply s τ holds given that the domain
> and range of s are disjoint.
> It is almost done (I have almost succeeded), but I have encountered a
> problematic situation. Please see the error in the included file
> Subst.agda (that uses Ty.agda).
>
> Maybe the following can help to find a solution; I have tried to use
> rewrite to convince Agda that replace v τ₀ (Var v)  ≡ τ₀, in the process
> of proving idempotence, but rewrite has not been enough the "second
> time" it is needed (which happens to be in the context of using sym, but
> probably being in the context of using sym is irrelevant).
>
> Thank you in advance for your help, or comments.
>
> Cheers,
>
> Carlos
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>