How to apply an axiom to simplify a match in Coq?

user_652528 0
Viewed 115

I have this code

Parameter foo : nat -> option bool.

Definition foo_valid x :=
  match foo x with
      Some _ => True
    | None => False
  end.

Axiom foo_is_valid : forall x, foo x = Some true.

Lemma foo_some_is_true_for_real : forall {x : nat}, foo_valid x.
  cbv.
  intros.

At this point I have this goal


x : nat

========================= (1 / 1)

match foo x with
| Some _ => True
| None => False
end

Is it possible to use foo_is_valid axiom to eliminate the match and finish the proof? How can I do that?

coq
1 Answers

foo_is_valid x is an equality so you can use it to rewrite. The easiest way to do so is using the rewrite tactic.

rewrite foo_is_valid.

should replace foo x by Some true in your goal, and then simpl will make the match compute.

user_12759750
Related