Stream: Coq users

Topic: Propositional logic lemma

view this post on Zulip alexm98 (Jun 17 2020 at 09:01):

Variables A B C P1 P2: Prop.

Lemma lem1: (A /\ B) \/ (~A /\ B) \/ (A /\~B) \/ (~A /\~B).

I have to demonstrate the upside mentioned predicate logic lemma and don't know how to start with intros. Can anyone give me some advice for this?

view this post on Zulip Karl Palmskog (Jun 17 2020 at 09:09):

there is no point in using intros when you've already declared all variables. You probably want to declare the variables and declare the proof inside a section, e.g., Section PredicateLogic. (* code *) End PredicateLogic.

view this post on Zulip Karl Palmskog (Jun 17 2020 at 09:12):

as for how to get started, this lemma can't be proven without adding axioms from classical logic (From Coq Require Import Classical.), and conjuring the premises A \/ ~A and B \/ ~B, e.g., via the axiom classic.

Last updated: Oct 13 2024 at 01:02 UTC