Propositional Logic in Coq
This is just for demonstration purposes and not directly related to the AI lecture
Find the source code here.
Section Universe.
We introduce a universe of booleans
Inductive U : Set := T | F.
And provide some definitions and theorems
Definition negate (t : U) : U :=
match t with
| T ⇒ F
| F ⇒ T
end.
Theorem dneg : ∀ P, negate (negate P) = P.
intros []; trivial.
Qed.
Definition and (a b : U) : U :=
match (a, b) with
| (T, T) ⇒ T
| _ ⇒ F
end.
Theorem and_comm : ∀ P Q, and P Q = and Q P.
intros [] []; trivial.
Qed.
Theorem and_assoc : ∀ P Q R, and P (and Q R) = (and (and P Q) R).
intros [] [] []; trivial.
Qed.
Theorem contra : ∀ P, and P (negate P) = F.
intros []; trivial.
Qed.
Theorem and_F : ∀ P, and P F = F.
intros []; trivial.
Qed.
End Universe.
Notation "⊤" := T : pl.
Notation "⊥" := F : pl.
match t with
| T ⇒ F
| F ⇒ T
end.
Theorem dneg : ∀ P, negate (negate P) = P.
intros []; trivial.
Qed.
Definition and (a b : U) : U :=
match (a, b) with
| (T, T) ⇒ T
| _ ⇒ F
end.
Theorem and_comm : ∀ P Q, and P Q = and Q P.
intros [] []; trivial.
Qed.
Theorem and_assoc : ∀ P Q R, and P (and Q R) = (and (and P Q) R).
intros [] [] []; trivial.
Qed.
Theorem contra : ∀ P, and P (negate P) = F.
intros []; trivial.
Qed.
Theorem and_F : ∀ P, and P F = F.
intros []; trivial.
Qed.
End Universe.
Notation "⊤" := T : pl.
Notation "⊥" := F : pl.
Section Syntax.
We assume a set of variables to exist
Variable Var : Set.
Inductive Formula : Set :=
| var : Var → Formula
Inductive Formula : Set :=
| var : Var → Formula
A variable is a formula
| neg : Formula → Formula
The negation of a formula is a formula
| conj : Formula → Formula → Formula.
The conjunction of two formulae is a formula
Disjunction and implication can be derived now
Definition disj (A B : Formula) : Formula :=
neg (conj (neg A) (neg B)).
Definition imp (A B : Formula) : Formula :=
(disj (neg A) B).
End Syntax.
Notation "¬ A" := (neg A) (at level 75) : pl.
Notation "A ∧ B" := (conj A B) (at level 80, right associativity) : pl.
Notation "A ∨ B" := (disj A B) (at level 85, right associativity) : pl.
Notation "A ⇒ B" := (imp A B) (at level 90, right associativity) : pl.
neg (conj (neg A) (neg B)).
Definition imp (A B : Formula) : Formula :=
(disj (neg A) B).
End Syntax.
Notation "¬ A" := (neg A) (at level 75) : pl.
Notation "A ∧ B" := (conj A B) (at level 80, right associativity) : pl.
Notation "A ∨ B" := (disj A B) (at level 85, right associativity) : pl.
Notation "A ⇒ B" := (imp A B) (at level 90, right associativity) : pl.
Section Interpretation.
Again, we assume a set of variables to exist
Variable Var : Set.
An assignment is now just a function from variables to universe elements.
Note that this means that we assume all assignments to be total.
Definition Assignment : Type :=
Var → U.
Var → U.
We can now apply the interpretation function recursively:
Fixpoint I (φ : Assignment) (f : Formula Var) : U :=
match f with
| var P ⇒ φ P
match f with
| var P ⇒ φ P
A variable is interpreted as its assigned value
| neg A ⇒ negate (I φ A)
The negation of A is the boolean negation of the interpretation of A
| conj A B ⇒ and (I φ A) (I φ B)
The conjunction of A and B is the boolean conjunction...
end.
We can now state validity and satisfiability
Definition valid (A : Formula Var) : Prop :=
∀ (φ : Assignment), I φ A = ⊤.
Definition satisfiable (A : Formula Var) : Prop :=
∃ (φ : Assignment), I φ A = ⊤.
End Interpretation.
Module Example1.
Inductive Var : Set := A | B.
Definition F1 : Formula Var :=
A ⇒ (B ⇒ A).
Lemma F1_valid : valid F1.
Proof.
unfold valid.
intros.
unfold F1.
unfold imp.
simpl.
repeat rewrite dneg.
rewrite and_assoc.
rewrite (and_comm (φ A) (φ B)).
rewrite <- and_assoc.
rewrite contra.
rewrite and_F.
trivial.
Qed.
End Example1.
Module Example2.
Inductive Var : Set := A | B | C.
Definition φ_counter (v : Var) : U :=
match v with
| A ⇒ ⊤
| B ⇒ ⊤
| C ⇒ ⊥
end.
Definition F2 : Formula Var :=
A ∧ B ⇒ A ∧ C.
Lemma F2_not_valid : ¬ valid F2.
Proof.
unfold valid.
intro H.
specialize (H φ_counter).
simpl in H.
discriminate.
Qed.
End Example2.
∀ (φ : Assignment), I φ A = ⊤.
Definition satisfiable (A : Formula Var) : Prop :=
∃ (φ : Assignment), I φ A = ⊤.
End Interpretation.
Module Example1.
Inductive Var : Set := A | B.
Definition F1 : Formula Var :=
A ⇒ (B ⇒ A).
Lemma F1_valid : valid F1.
Proof.
unfold valid.
intros.
unfold F1.
unfold imp.
simpl.
repeat rewrite dneg.
rewrite and_assoc.
rewrite (and_comm (φ A) (φ B)).
rewrite <- and_assoc.
rewrite contra.
rewrite and_F.
trivial.
Qed.
End Example1.
Module Example2.
Inductive Var : Set := A | B | C.
Definition φ_counter (v : Var) : U :=
match v with
| A ⇒ ⊤
| B ⇒ ⊤
| C ⇒ ⊥
end.
Definition F2 : Formula Var :=
A ∧ B ⇒ A ∧ C.
Lemma F2_not_valid : ¬ valid F2.
Proof.
unfold valid.
intro H.
specialize (H φ_counter).
simpl in H.
discriminate.
Qed.
End Example2.
This page has been generated by coqdoc