Unfolding definitions with match

Stream: new members

[Ken Roe]

I'm trying to prove the following:

def evv (x :ℕ → ℕ) (y: ℕ):=
    match x y with
    | 0 := tt
    | 1 := ff
    | _ := tt
    end

theorem test: ∀ x (f: ℕ → ℕ), f x=1 → evv f x :=
begin
    intros, unfold evv, ...
end

At the point of the "...", I have the following state:

x : ℕ,
f : ℕ → ℕ,
a : f x = 1
⊢ ↥(evv._match_1 (f x))

How do I complete the theorem?

[Ken Roe]

I was using quotation, however, I would like to find a way to construct the expression without the quotation.

[Kevin Buzzard]

Your theorem is false so it's hard to complete.

[Kevin Buzzard]

theorem test: ∀ x (f: ℕ → ℕ), f x=1 → evv f x :=
begin
    intros,
    unfold evv,
    rw a,
    simp only [evv._match_1],
    -- suffices to prove ff
    sorry
end

[Kevin Buzzard]

The arrow business is because you are talking about booleans as if they're propositions, so a coercion is happening.

[Chris Hughes]

It wasn't true so I changed it.

theorem test: ∀ x (f: ℕ → ℕ), f x=0 → evv f x :=
begin
  intros,
  unfold evv,
  rw a,
  exact rfl,
end