CODEWITHSUNDEEP
coqlogical-foundations
user4035
user4035

Reputation: 23719

How to make coq simplify expressions inside an implication hypothesis

Im trying to prove the following lemma:

Inductive even : nat → Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

Lemma even_Sn_not_even_n : forall n,
    even (S n) <-> not (even n).
Proof.
  intros n. split.
  + intros H. unfold not. intros H1. induction H1 as [|n' E' IHn].
    - inversion H.
    - inversion_clear H. apply IHn in H0. apply H0.
  + unfold not. intros H. induction n as [|n' E' IHn].
    -
Qed.

Here is what I got at the end:

1 subgoal (ID 173)

H : even 0 -> False
============================
even 1

I want coq to evaluate "even 0" to true and "even 1" to false. I tried simpl, apply ev_0 in H. but they give an error. What to do?

Upvotes: 3

Views: 2280

Answers (1)

Bubbler
Bubbler

Reputation: 982

Answer to the title

simpl in H.

Real answer

The above code will not work.

The definition of even from the Logical Foundations book is:

Inductive even : nat → Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

even 0 is a Prop, not a bool. Looks like you're mixing up the types True and False and the booleans true and false. They're totally different things, and not interchangeable under Coq's logic. In short, even 0 does not simplify to true or True or anything. It is just even 0. If you want to show even 0 is logically true, you should construct a value of that type.

I don't remember which tactics are available at that point in LF, but here are some possibilities:

(* Since you know `ev_0` is a value of type `even 0`,
   construct `False` from H and destruct it.
   This is an example of forward proof. *)
set (contra := H ev_0). destruct contra.

(* ... or, in one step: *)
destruct (H ev_0).

(* We all know `even 1` is logically false,
   so change the goal to `False` and work from there.
   This is an example of backward proof. *)
exfalso. apply H. apply ev_0.

Upvotes: 6

Related Questions