[Agda] [new-reflection] unsolved metas in induction

[Ulf Norell]

Simplified, you have the following situation:

thm : ∀ n → T n
thm = induction   -- works

thm' : ∀ n → T n
thm' n = induction n  -- fails

The induction tactic looks at the current goal type, so to understand why
the first case works but the second one fails we have to figure out what
the goal types are for the two induction calls. In the first case the goal
is
clearly ∀ n → T n, which induction can handle no problem. In the other
case however the goal is not so obvious. At the very least it needs to be a
function type, so

  induction : ∀ x → _1 n x

for a fresh meta _1. Note that the meta has access to both the fresh x and
the n. Now we need

  induction n : T n

for the right-hand side to type correct, so

  _1 n n == T n

Here we can see the problem. There are two solutions to this equation:

  _1 := λ x y → T x
  _1 := λ x y → T y

so the meta will not be solved.

So, why is this not a problem in the by-hand case? Because in the by-hand
case
you provide the solution to the meta explicitly. If you instead try

  by-hand : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
  by-hand n = nat-induction _ auto (λ n eq → by eq) n

you'll get the same unsolved metas.

/ Ulf

On Fri, Jan 22, 2016 at 9:57 PM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> I'm a newbie to reflection in Agda and am excited to learn the
> new-reflection machinery. I'm starting by working through the example of
> induction in Tactic.Nat.
>
>   induction-example : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
>   induction-example = induction
>
> I tried to figure out what the induction macro is doing and came up with
> this:
>
>   by-hand : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
>   by-hand = nat-induction (λ n → sum (downFrom n) * 2 ≡ n * (n + 1)) auto
> (λ n eq → by eq)
>
> So far, great. I also tried:
>
>   unsolved-metas : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
>   unsolved-metas n = induction n
>
> but that produces 3 yellow-highlighted errors. However, there are no such
> problems in the "by-hand" version:
>
>   by-hand-2 : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
>   by-hand-2 n = nat-induction (λ n → sum (downFrom n) * 2 ≡ n * (n + 1))
> auto (λ n eq → by eq) n
>
> I'm confused. TIA for help in understanding this.
> --
> Martin Stone Davis
>
> Postal/Residential:
> 1223 Ferry St
> Apt 5
> Eugene, OR 97401
> Talk / Text / Voicemail: (310) 699-3578 <3106993578>
> Electronic Mail: martin.stone.davis at gmail.com
> Website: martinstonedavis.com
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160123/ed35f287/attachment-0001.html