Commit f3503901b158b3a9a5cc5dd3dbe0d9b77b14fe33 - software-foundations

Flattened some proofs Getty Ritter 7 years ago

1 changed file(s) with 14 addition(s) and 20 deletion(s). Collapse all Expand all

+14

-20

01-basics.v less more

102	102	Theorem andb_true_elim2 : forall b c : bool,
103	103	andb b c = true -> c = true.
104	104	Proof.
105		intros b c.
106		destruct b.
107		- destruct c.
108		+ reflexivity.
109		+ simpl. intros H. rewrite -> H. reflexivity.
110		- destruct c.
111		+ reflexivity.
112		+ simpl. intros H. rewrite -> H. reflexivity.
	105	intros [] [].
	106	- reflexivity.
	107	- simpl. intros H. rewrite -> H. reflexivity.
	108	- reflexivity.
	109	- simpl. intros H. rewrite -> H. reflexivity.
113	110	Qed.
114	111
115	112	(* exercise zero_nbeq_plus_1 *)

184	181	(andb b c = orb b c) ->
185	182	b = c.
186	183	Proof.
187		intros b c.
188		destruct b.
189		- destruct c.
190		+ reflexivity.
191		+ rewrite -> andb_comm. rewrite -> andb_l_false.
192		rewrite -> orb_l_true.
193		intros H. rewrite -> H. reflexivity.
194		- destruct c.
195		+ rewrite -> andb_l_false.
196		rewrite -> orb_comm. rewrite -> orb_l_true.
197		intros H. rewrite -> H. reflexivity.
198		+ reflexivity.
	184	intros [] [].
	185	- reflexivity.
	186	- rewrite -> andb_comm. rewrite -> andb_l_false.
	187	rewrite -> orb_l_true.
	188	intros H. rewrite -> H. reflexivity.
	189	- rewrite -> andb_l_false.
	190	rewrite -> orb_comm. rewrite -> orb_l_true.
	191	intros H. rewrite -> H. reflexivity.
	192	- reflexivity.
199	193	Qed.
200	194
201	195	(* exercise binary *)