[Agda] Wildcards

[Andreas Abel]

 On Sun, 25 Mar 2012 20:49:58 +0200, Guillaume Brunerie wrote:
> 2012/3/25 Nils Anders Danielsson <nad at chalmers.se>:
>>  [112] ((_89 p q r s ∘ _90 p q r s) ∘ _91 p q r s) = ((p ∘ q) ∘ (r ∘ 
>> s)) :
>> .x ≡ .u
>>  [112] (_89 p q r s ∘ (_90 p q r s ∘ _91 p q r s)) = (p ∘ (q ∘ (r ∘ 
>> s))) :
>> .x ≡ .u
>>  _92 := λ {.A} {.x} {.y} {.z} {.t} {.u} p q r s →
>>    assoc (_89 p q r s) (_90 p q r s) (_91 p q r s) [blocked by 
>> problem 112]
>
> But why Agda does not solve the constraints automatically?
>
> It seems to me that Agda could try to simplify the first constraint 
> to
> (_89 p q r s ∘ _90 p q r s) = (p ∘ q)
> _91 p q r s = (r ∘ s)
>
> and then to
> _89 p q r s = p
> _90 p q r s = q
> _91 p q r s = (r ∘ s)
>
> which solves the first constraint, and then notice that the second is
> also satisfied.
>
> Is there a reason Agda does not do this?

 Agda does not apply heuristics, it only solves metas when the solution 
 is unique.
 (This is quite different to Coq.)

 The heuristics you suggest, aka "first-order unification", is not 
 followed by
 Agda since it does not know that the composition is injective.

 The problem is that _89 is in head position, if it would be 
 instantiated to refl,
 composition (refl o ...) would reduce.

 Once _89 = p is given, (p o _90) is neutral, and so is (p o _90) o _91.
 Thus, the arguments need to match, and you get the equation written 
 above,

   _90 = q
   _91 = r o s

 This explains Agda's behavior.  If Agda would just return any fitting 
 solution,
 this would fire back, especially if you are not only interested in 
 proofs,
 but also in programs with wildcards.

 Cheers,
 Andreas


-- 
 Andreas Abel  <><     Du bist der geliebte Mensch.

 Theoretical Computer Science, University of Munich 
 http://www.tcs.informatik.uni-muenchen.de/~abel/