expanding proofs

Stream: general

[Eric Rodriguez]

I was given this example code, which I don't fully understand:

import data.nat.prime

example (n : ℕ) : ℕ :=
match n.min_fac, rfl : ∀ x, n.min_fac = x → ℕ with
  | 0, h := absurd h n.min_fac_pos.ne'
  | (n+1), h := n
  end

the point of this is that we want to be able to get what the value "originally" was in the match. But to me, in the RHS, there are 3 terms (the nat x, the proof of equality, and the arbitrary output natural number) whilst on the left hand side wwe only provide it min_fac and rfl. What is this synrax doing, then?

[Yaël Dillies]

The trailing ℕ is not an input, right? It's the return type of your match.

[Eric Rodriguez]

but that's not how match usually works, no?

[Yaël Dillies]

If you don't specify the type of a match, then its type will be your goal, fi that's what you mean.

[Kyle Miller]

I haven't tested it here, but you should be able to write

example (n : ℕ) : ℕ :=
match n.min_fac, rfl : ∀ x, n.min_fac = x → _ with
  | 0, h := absurd h n.min_fac_pos.ne'
  | (n+1), h := n
  end

if you want to avoid writing the expected type of the match expression.

[Eric Rodriguez]

this does work, I specified all the types to try understand what was going on

[Eric Rodriguez]

so I guess this match creates this dependent function \forall x, n.min_fac = x -> nat and then the left hand side "provides values to it"?

[Kyle Miller]

Yeah, and this is something you can verify:

def foo (n : ℕ) : ℕ :=
match n.min_fac, rfl : ∀ x, n.min_fac = x → _ with
  | 0, h := absurd h n.min_fac_pos.ne'
  | (n+1), h := n
  end

#print foo
/-
def foo : ℕ → ℕ :=
λ (n : ℕ), foo._match_1 n n.min_fac _
-/
#print foo._match_1
/-
def foo._match_1 : Π (n x : ℕ), n.min_fac = x → ℕ :=
...
-/

[Eric Wieser]

I wrote about this syntax a little here

[Kyle Miller]

There's a small implementation detail that this match function has some extra arguments corresponding to values it depends on (n in this case)

[Sebastian Ullrich]

This is called the convoy pattern in http://adam.chlipala.net/cpdt/html/MoreDep.html

we can extend the match to return functions over the free variables whose types we want to refine