gdritter repos software-foundations / master
Flattened some proofs Getty Ritter 7 years ago
1 changed file(s) with 14 addition(s) and 20 deletion(s). Collapse all Expand all
102102 Theorem andb_true_elim2 : forall b c : bool,
103103 andb b c = true -> c = true.
104104 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.
113110 Qed.
114111
115112 (* exercise zero_nbeq_plus_1 *)
184181 (andb b c = orb b c) ->
185182 b = c.
186183 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.
199193 Qed.
200194
201195 (* exercise binary *)