Syllogisms in Coq (using classical logic, and dependent types).

Syllogism_with_dependent_type.v

Module SigmaTry.

  Inductive D : Type :=
  | a
  | b
  | c.

  Definition P (x : D) : Prop :=
    match x with
    | a => True
    | b => True
    | c => True
    end.

  Definition Q (x : D) : Prop :=
    match x with
    | a => True
    | b => True
    | c => True
    end.
  
  Compute {x : D | P x}.
  Compute {x : D | Q x}.

  Search "sig".
  Search "exist".
  Print sig.
  (* So the one constructor [exist] for [sig] takes two arguments:
     - [x : A], some object [x] in [A].
     - [P x], a function [P : A -> Prop] proving that [x] satisfies [P].
     It then returns an instance of [{x : A | P x}]. *)

  Lemma all_Ps_are_Q :
    forall z : {x : D | P x}, Q (proj1_sig z). 
  Proof.
    (* Let z' be a fixed [{x : D | P x}]. *)
    intros z'.

    (* We must show that [Q (proj1_sig z')] holds for [z'].
       Let's do induction over it's constructors. 
       It has one constructor, [exists], which takes two arguments,
       an [x] and a [P], as noted above.

       So, assume that there is an [x'] of type [D], and a function [P]
       such that [P x']. Then if we apply the [exist] constructor to those,
       we will get an instance of [{x : D | P x}]. *)
    induction z' as [x' P'].
    (* In the proof state, we can see the assumed [x'] and [P'], then
       we can see in the goal that we take the [exist] constructor
       (which is a function [fun x : D => P x]), and we apply it to
       [x'] and [P']. So this will yield an instance of [{x : D | P x}],
       under the assumption that [x'] belongs to [D], and [P'] holds. *)

    (* We must show that taking the [proj1_sig] of this [{x : D | P x}]
       satisfies [Q]. We can do that by looking at all cases of [x']. 
       This is trivial, because [Q] is defined to hold on all [D]s. *)
    case x'.
    - unfold Q. trivial.
    - unfold Q. trivial.
    - unfold Q. trivial.
  Qed.

  Definition R (x : D) : Prop :=
    match x with
    | a => True
    | b => True
    | c => False
    end.

  Definition S (x : D) : Prop :=
    match x with
    | a => False
    | b => True
    | c => False
    end.

  Lemma b_is_R : R b.
    Proof. unfold R. trivial. Qed.
  
  Lemma some_Rs_are_S :
    exists z : {x : D | R x}, S (proj1_sig z).
  Proof.
    (* We must construct a witness of [{x : D | R x}].
       To do that, we can use the [exist] constructor.
       It takes a predicate [R], an object in [D], and
       a proof that the object satisfies [R]. *)
    exists (exist R b b_is_R).

    (* Now we must show that if we take the first projection
       of this witness, it satisfies [S]. If we apply [b_is_R],
       that somehow solves the goal. We can also do [reflexivity],
       and that will solve it too. *)
    apply b_is_R.
  Qed.

  Definition T (x : D) : Prop :=
    match x with
    | _ => False
    end.

  Lemma no_Rs_are_T :
    forall z : { x : D | R x}, ~ T (proj1_sig z).
  Proof.
    unfold not.
    intro z'.
    induction z' as [x' R'].

    (* Let's consider all forms that [x'] can take. *)
    induction x'.

    (* In each case, the first projection of [z] does not satisfy [T]. *)
    - trivial.
    - trivial.
    - trivial.
  Qed.

  Lemma c_is_P : P c.
  Proof. unfold P. trivial. Qed.

  Lemma c_is_not_R : ~ R c.
  Proof.
    unfold not.
    unfold R.
    trivial.
  Qed.
  
  Lemma some_Ps_are_not_R :
    exists z : { x : D | P x}, ~ R (proj1_sig z).
  Proof.
    (* Construct a witness. *)
    exists (exist P c c_is_P).
    (* Now show that the first projection fails to satisfy [Q]. *)
    unfold not.
    intro H.
    apply c_is_not_R in H.
    apply H.
  Qed.
    
End SigmaTry.

Syllogism_with_predicate_calculus.v

Module SimpleTry.

(** A domain of objects. *)
Inductive D : Set :=
| a
| b
| c.

(** A predicate over [D]. *)
Definition P (x : D) : Prop :=
  match x with
  | a => True
  | b => True
  | c => False
  end.

(** Another predicate over [D]. *)
Definition Q (x : D) : Prop :=
  match x with
  | _ => False
  end.

(** A predicate that is true of all of [D]. *)
Definition R (x : D) : Prop :=
  match x with
  | _ => True
  end.

(** Another one that's true of all of [D]. *)
Definition S (x : D) : Prop :=
  match x with
  | _ => True
  end.

(** And one more. *)
Definition T (x : D) : Prop :=
  match x with
  | _ => True
  end.

(** Check some evaluations. *)
Compute P a.
Compute P b.
Compute Q a.

(** Some examples. *)
Example test_P_a : P a = True.
Proof.
  unfold P.
  reflexivity.
Qed.

Example test_Q_a : Q a = False.
Proof.
  unfold Q.
  reflexivity.
Qed.

(** The object [a] satisfies [P]. *)
Theorem a_is_P : P a = True.
Proof.
  trivial.
Qed.

(** It's false that the object [c] satisfies [P]. *)
Theorem c_is_not_P : P c = False.
Proof.
  unfold P.
  reflexivity.
Qed.

(* It is not the case that the object [c] satisfies [P]. *)
Theorem c_is_not_P_is_true : not (P c).
Proof.
  unfold not.
  unfold P.
  intros H.
  apply H.
Qed.
  
(** Some objects satisfy [P]. *)
Theorem sigma_P : exists x : D, P x.
Proof.
  exists a.
  unfold P.
  reflexivity.
Qed.

(** An object satisfies [P] and it is [a]. *)
Theorem sigma_P_is_a : exists x : D, P x /\ x = a.
Proof.
  exists a.
  split.
  - unfold P. reflexivity.
  - reflexivity.
Qed.

(** It is not the case that every object satisfies [P]. *)
Theorem not_pi_P : not (forall x : D, P x).
Proof.
  unfold not.
  intros H.
  destruct H with (x := c).
Qed.

(** Some objects are not [P]. *)
Theorem sigma_not_P : exists x : D, not (P x).
Proof.
  unfold not.
  exists c.
  unfold P.
  intros H.
  apply H.
Qed.

(** No objects satisfy [Q]. *)
Theorem pi_D_not_P : forall x : D, not (Q x).
Proof.
  unfold not.  
  intros a.
  unfold Q.
  intros H.
  apply H.
Qed.

(** All [R]s are [S]s. *)
Theorem all_Rs_are_Ss :
  forall x : D, R(x) -> S(x).
Proof.
  intro a.
  intro H.
  unfold R in H.
  unfold S.
  apply H.
Qed.

(** All [S]s are [T]s. *)
Theorem all_Ss_are_Ts:
  forall x : D, S(x) -> T(x).
Proof.
  intro a.
  intro H.
  unfold S in H.
  unfold T.
  apply H.
Qed.

(** All [R]s are [T]s. *)
Theorem all_Rs_are_Ts:
  forall x : D, R(x) -> T(x).
Proof.
  intro a.
  intro H.
  unfold R in H.
  unfold T.
  apply H.
Qed.

(** Baraba. *)
Theorem Barbara:
  forall x : D, ((R(x) -> S(x) /\ S(x) -> T(x)) -> R(x) -> T(x)).
Proof.
  intro a.
  intro H.
  unfold R in H.
  unfold S in H.
  unfold T in H.
  unfold R.
  unfold T.
  split.
Qed.

End SimpleTry.