Induction.ConjunctiveFalseness
(*
CoMoEx - Example of inductive proofs: Conjunctive Falseness
Copyright (C) 2024 Max Ole Elliger
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
From Induction Require Export Intro.
CoMoEx - Example of inductive proofs: Conjunctive Falseness
Copyright (C) 2024 Max Ole Elliger
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
From Induction Require Export Intro.
Die folgende Zeile einfach durch eine passende Definition ersetzen!
In den nachfolgenden Beispielen einfach Admitted durch Qed ersetzen!
Local Example sanity_check_top :
only_top_bottom_atom_conjunction top.
Proof.
firstorder.
Admitted.
Local Example sanity_check_bottom :
only_top_bottom_atom_conjunction bottom.
Proof.
firstorder.
Admitted.
Local Example sanity_check_atom :
forall a,
only_top_bottom_atom_conjunction (atom a).
Proof.
firstorder.
Admitted.
Local Example sanity_check_negation :
forall f,
~ only_top_bottom_atom_conjunction (negation f).
Proof.
firstorder.
Admitted.
Local Example sanity_check_conjunction :
forall f1 f2,
only_top_bottom_atom_conjunction f1 ->
only_top_bottom_atom_conjunction f2 ->
only_top_bottom_atom_conjunction (conjunction f1 f2).
Proof.
firstorder.
Admitted.
Local Example sanity_check_disjunction :
forall f1 f2,
~ only_top_bottom_atom_conjunction (disjunction f1 f2).
Proof.
firstorder.
Admitted.
Local Example sanity_check_implication :
forall f1 f2,
~ only_top_bottom_atom_conjunction (implication f1 f2).
Proof.
firstorder.
Admitted.
Local Example sanity_check_biimplication :
forall f1 f2,
~ only_top_bottom_atom_conjunction (biimplication f1 f2).
Proof.
firstorder.
Admitted.