<br><div class="gmail_quote">On Sun, Sep 9, 2012 at 7:57 AM, Ulf Norell <span dir="ltr">&lt;<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<br><div class="gmail_quote"><div class="im">On Fri, Sep 7, 2012 at 12:49 PM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">


I would not have expected the following program to type check:<br>
<br>
assert : (A : Set) → A → Bool → Bool<br>
assert _ _ true  = true<br>
assert _ _ false = false<br>
<br>
g : Bool -&gt; Bool -&gt; Bool<br>
g x true  = true<br>
g x false = true<br>
<br>
unsolved : Bool -&gt; Bool<br>
unsolved y =<br>
  let X : Bool<br>
      X = _<br>
  in  assert (g X y ≡ g true y) refl X<br>
<br>
istrue : (unsolved false) ≡ true<br>
istrue = refl<br>
<br>
The meta-variable X is solved to &#39;true&#39; (as witnessed by istrue), even though &#39;false&#39; would also be a solution, semantically, because g actually ignores its first argument.  (It even ignores its second argument, but that does not matter here.)<br>



<br>
The expected behavior would be an unsolved X, since it is not uniquely determined.<br></blockquote><div><br></div></div><div>This is the correct behaviour. Your assertion that &#39;false&#39; would be a solution is incorrect. If you actually try it you get</div>


<div><br></div><div><div>false != true of type Bool</div><div>when checking that the expression refl has type</div><div>g false y ≡ g true y</div></div><div><br></div><div>We&#39;ve had this discussion before. Metavariables are solved with unique solutions that make the intensional equality hold, not the extensional equality. This is why solving true for X is fine in g X y ≡ g true y, even though, for all closed y, g false y ≡ g true y.</div>

</div></blockquote><div><br></div><div>To drive the point home further, if you change the program so that false is actually a solution (by replacing refl by a different proof), X is not solved:</div><div><br></div><div>lem : ∀ {x₁ x₂} y → g x₁ y ≡ g x₂ y</div>

<div>lem true  = refl</div><div>lem false = refl</div><div><br></div><div>unsolved : Bool -&gt; Bool</div><div>unsolved y =</div><div>  let X : Bool</div><div>      X = _</div><div>  in  assert (g X y ≡ g true y) (lem y) X</div>

<div><br></div><div>/ Ulf </div></div><br>