Skip to content

Instantly share code, notes, and snippets.

@SPY

SPY/andb_eq_orb.v

Last active January 1, 2016 22:38
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save SPY/8210862 to your computer and use it in GitHub Desktop.
Save SPY/8210862 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
andb_eq_orb.v
(** **** Exercise: 2 stars (andb_eq_orb) *)
(** Prove the following theorem. (You may want to first prove a
subsidiary lemma or two.) *)
Lemma orb_always_true :
forall b,
orb true b = true.
Proof. reflexivity. Qed.
Lemma andb_always_false :
forall b,
andb false b = false.
Proof. reflexivity. Qed.
Theorem andb_eq_orb :
forall (b c : bool),
(andb b c = orb b c) ->
b = c.
Proof.
destruct b.
intros c.
intros H.
rewrite <- orb_always_true with c.
rewrite <- H.
destruct c.
reflexivity.
reflexivity.
intros c.
intros H.
rewrite <- andb_always_false with c.
rewrite -> H.
destruct c.
reflexivity.
reflexivity.
Qed.
@fabriceleal
Copy link

If you're interested in a shorter solution, I found this one https://github.com/etosch/software_foundations/blob/master/lesson1_Basics.v#L194

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment