1

There is a point in proving 

Theorem negb_is_not : (forall a, Is_true (negb a) <-> (~(Is_true a))).

from this tutorial in Coq where I am stuck. This is the case when False is left to prove as "False cannot be proven". How do I cope with that?

Theorem negb_is_not : (forall a, Is_true (negb a) <-> (~(Is_true a))).
Proof.
  intros A.
  unfold iff.
  refine (conj _ _).
  case A.
  simpl.
  intros H.
  destruct H. 
  intros H.
  simpl in H.
  simpl.
  unfold not.
  intros.
  exact H0.
  unfold not.
  intros H.
  case A.
  simpl.
  destruct H.
  case A.
  simpl.
  exact I.
  simpl.
  Focus 2.
  simpl.
  exact I.

I think I just missed some little important thing in the tutorial.

Improve this question

1 Answer 1

Reset to default
1

OK, after some rewrites, I was able to write this proof:

Theorem negb_is_not : (forall a, Is_true (negb a) <-> (~(Is_true a))).
Proof.
  intros A.
  unfold iff.
  refine (conj _ _).
    case A.
      simpl.
      intros H.
      case H.

      simpl.
      intros.
      unfold not.
      intros.
      exact H0.

    case A.
      simpl.
      unfold not.
      intros.
      refine (H _).
      exact I.

      simpl.
      unfold not.
      intros.
      exact I.
Qed.
Improve this answer
1
  • 3
    A few remarks: case seems to operate only on the conclusion, you can use destruct instead which operates on the conclusion and the hypotheses; instead of unfold iff. refine (conj _ _)., you can use the more natural split.
    – eponier
    Commented Mar 28, 2018 at 9:20

Not the answer you're looking for? Browse other questions tagged or ask your own question.