## Stream: general

### Topic: expanding proofs

#### Eric Rodriguez (Jan 16 2023 at 11:02):

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 (Jan 16 2023 at 11:04):

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

#### Eric Rodriguez (Jan 16 2023 at 11:08):

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

#### Yaël Dillies (Jan 16 2023 at 11:10):

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 (Jan 16 2023 at 11:13):

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 (Jan 16 2023 at 11:15):

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

#### Eric Rodriguez (Jan 16 2023 at 11:16):

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 (Jan 16 2023 at 11:17):

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 (Jan 16 2023 at 11:22):

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