(** * Propositional Logic in Coq *)
(** This is just for demonstration purposes and not directly related to the AI lecture *)
(* begin hide *)
Set Implicit Arguments.

Declare Scope pl.
Open Scope pl.
(* end hide *)

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 : forall 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 : forall P Q, and P Q = and Q P.
    intros [] []; trivial.
  Qed.

  Theorem and_assoc : forall P Q R, and P (and Q R) = (and (and P Q) R).
    intros [] [] []; trivial.
  Qed.

  Theorem contra : forall P, and P (negate P) = F.
    intros []; trivial.
  Qed.

  Theorem and_F : forall 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        (** 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.

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.

  (** We can now apply the interpretation function recursively: *)
  Fixpoint I (φ : Assignment) (f : Formula Var) : U :=
    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 :=
    forall (φ : Assignment), I φ A = ⊤.

  Definition satisfiable (A : Formula Var) : Prop :=
    exists (φ : Assignment), I φ A = ⊤.

End Interpretation.

Module Example1.
  Inductive Var : Set := A | B.
  (* begin hide *)
  Definition c (v : Var) : Formula Var :=
    var v.
  Coercion c : Var >-> Formula.
  (* end hide *)
  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.
  
  (* begin hide *)
  Definition c (v : Var) : Formula Var :=
    var v.
  Coercion c : Var >-> Formula.
  (* end hide *)
  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.