Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

boolean proof thingy

  • Loading branch information...
commit 1fc5731173a800960990dbb7fc8c11270aa25f6b 1 parent 9e2b5f9
@oconnor0 authored
Showing with 7 additions and 2 deletions.
  1. +7 −2 sf/Basics.v
View
9 sf/Basics.v
@@ -1396,8 +1396,13 @@ Theorem all3_spec : forall b c : bool,
(negb c))
= true.
Proof.
- intros b c.
- (* FILL IN HERE *) Admitted.
+ intros b c. destruct b. destruct c.
+ Case "b = true, c = true".
+ simpl. reflexivity.
+ Case "b = true, c = false".
+ simpl. reflexivity.
+ Case "b = false".
+ simpl. reflexivity. Qed.
(* simplification & rewrites *)
Theorem mult_plus_distr_r : forall n m p : nat,
Please sign in to comment.
Something went wrong with that request. Please try again.