Module OtherExamples.

Parameter Term : Type.

Record Quantity : Type :=
  universal : Quantity
| particular : Quantity.

Record Quality : Type :=
  affirmative : Quality
| negative : Quality.

Record CategoricalProposition : Type := 
cp {  
  quantity : Quantity;
  quality : Quality;
  subject : Term; 
  object : Term
}.

Notation "'All' subject 'are' object " := 
   (cp universal affirmative subject object) (at level 50).

Notation "'No' subject 'are' object " := 
   (cp universal negative subject object) (at level 50).

Notation "'Some' subject 'are' object " := 
   (cp particular affirmative subject object) (at level 50).

Notation "'Some' subject 'are' 'not' object " := 
   (cp particular negative subject object) (at level 50).

Parameter holds : CategoricalProposition -> Prop.

Parameter non: Term -> Term.

Axiom NonNon: forall t, non (non t) = t.

Definition convert: CategoricalProposition -> CategoricalProposition := 
  fun x : CategoricalProposition => match x with
    | cp quantity quality subject object => 
      cp quantity quality object subject
  end.

Axiom ConvE1:
   forall subject object,
   holds (convert (Some subject are object))
   ->
   holds (Some subject are object).

Axiom ConvE2:
   forall subject object,
   holds (convert (No subject are object))
   ->
   holds (No subject are object).

Ltac eliminateConversion1 :=
  match goal with 
   | [ |- holds (cp ?quantity ?quality ?subject ?object)] 
     => 
     assert (holds (convert (cp quantity quality subject object))
             -> 
             holds (cp quantity quality subject
             object))
        as ConvertPremise;
     try solve [eapply ConvE1;
                eauto];
     apply ConvertPremise;
     clear ConvertPremise; 
     unfold convert
  end.

Ltac eliminateConversion2 :=
  match goal with 
   | [ |- holds (cp ?quantity ?quality ?subject ?object)] 
     => 
     assert (holds (convert (cp quantity quality subject object))
             -> 
             holds (cp quantity quality subject
             object))
        as ConvertPremise;
     try solve [eapply ConvE2;
                eauto];
     apply ConvertPremise;
     clear ConvertPremise; 
     unfold convert
  end.

Definition contrapose: CategoricalProposition -> 
                       CategoricalProposition := 
  fun x : CategoricalProposition => match x with
    | cp quantity quality subject object => 
      cp quantity quality (non object) (non subject)
  end.

Axiom ContrE1:
   forall subject object,
   holds (contrapose (All subject are object))
   ->
   holds (All subject are object).

Axiom ContrE2:
   forall subject object,
   holds (contrapose (Some subject are not object))
   ->
   holds (Some subject are not object).

Ltac eliminateContraposition1 :=
  match goal with 
   | [ |- holds (cp ?quantity ?quality ?subject ?object)] 
     => 
        assert (holds (contrapose (cp quantity quality subject object))
                -> holds (cp quantity quality subject object)) as ContraposePremise;
        try solve [eapply ContrE1;
                   eauto];
        apply ContraposePremise;
        clear ContraposePremise;
        unfold contrapose
  end.

Ltac eliminateContraposition2 :=
  match goal with 
   | [ |- holds (cp ?quantity ?quality ?subject ?object)] 
     => 
        assert (holds (contrapose (cp quantity quality subject object))
                -> holds (cp quantity quality subject object)) as ContraposePremise;
        try solve [eapply ContrE2;
                   eauto];
        apply ContraposePremise;
        clear ContraposePremise;
        unfold contrapose
  end.

Definition complement: Quality -> Quality :=
  fun x : Quality => match x with
    | affirmative => negative
    | negative => affirmative
  end.

Definition obvert: CategoricalProposition -> CategoricalProposition := 
  fun x : CategoricalProposition => match x with
    | cp quantity quality subject object 
      => cp quantity (complement quality) subject (non object)  
  end.

Axiom ObvE : 
   forall catprop, holds (obvert catprop) -> holds catprop.

Ltac eliminateObversion :=
  match goal with 
   | [ |- holds (cp ?quantity ?quality ?subject ?object)] 
     => 
       assert (holds (obvert (cp quantity quality subject object))
               -> holds (cp quantity quality subject object)) as ObvertPremise;
       try solve [eapply ObvE; eauto];
       apply ObvertPremise;  
       clear ObvertPremise;
       unfold obvert;
       unfold complement
  end.

Axiom Barbara : forall major minor middle, 
    holds (All middle are major)
 /\ holds (All minor are middle)
 -> holds (All minor are major).

Axiom Celarent : forall major minor middle, 
    holds (No middle are major)
 /\ holds (All minor are middle)
 -> holds (No minor are major).

Axiom Darii : forall major minor middle, 
    holds (All middle are major)
 /\ holds (Some minor are middle)
 -> holds (Some minor are major).

Axiom Ferio : forall major minor middle, 
    holds (No middle are major)
 /\ holds (Some minor are middle)
 -> holds (Some minor are not major).

 (*
    All unripe fruit is unwholesome.
    All these apples are wholesome.
    No fruit, grown in the shade, is ripe.
    --------------------------------------
    These apples are not grown in the shade.
 *)

Parameter ripe_fruit : Term.
Parameter wholesome_fruit : Term.
Parameter these_apples : Term.
Parameter fruit_grown_in_the_shade : Term.

Lemma These_apples_are_non_fruit_grown_in_the_shade :
   holds (All non ripe_fruit are non wholesome_fruit) /\
   holds (All these_apples are wholesome_fruit) /\
   holds (No fruit_grown_in_the_shade are ripe_fruit) 
   ->
   holds (All these_apples are non fruit_grown_in_the_shade).

Proof.
admit.
Qed.

(*
All writers, who understand human nature, are clever;
No one is a true poet unless he can stir the hearts of men;
Shakespeare wrote "Hamlet";
No writer, who does not understand human nature, can stir the hearts of men;
None but a true poet could have written "Hamlet".
-------------------------------------------------
Shakespeare was clever.
 *)

Parameter writers_who_understand_human_nature : Term.
Parameter clever_people : Term.
Parameter true_poets: Term.
Parameter writers_who_can_stir_the_hearts_of_men : Term.
Parameter people_who_are_Shakespeare : Term.
Parameter people_who_wrote_Hamlet : Term.

Lemma Clever_Shakespeare :
   holds (All writers_who_understand_human_nature are clever_people) /\
   holds (No non writers_who_can_stir_the_hearts_of_men are true_poets) /\
   holds (All people_who_are_Shakespeare are people_who_wrote_Hamlet) /\
   holds (No non writers_who_understand_human_nature are writers_who_can_stir_the_hearts_of_men) /\
   holds (No non true_poets are people_who_wrote_Hamlet)
   ->
   holds (All people_who_are_Shakespeare are clever_people).

Proof.
admit.
Qed.

  
(*
All the dated letters in this room are written on blue paper;
None of them are in black ink, except those that are written in the third person;
I have not filed any of them that I can read;
None of them, that are written on one sheet, are undated;
All of them, that are not crossed, are in black ink;
All of them, written by Brown, begin with "Dear Sir";
All of them, written on blue paper, are filed;
None of them, written on more than one sheet, are crossed;
None of them, that begin with "Dear Sir", are written in the third person. 
----------------------------------------
I cannot read any of Brown's letters.
*)


Parameter dated_letters : Term.
Parameter letters_written_on_blue_paper : Term.
Parameter letters_written_in_black_ink : Term.
Parameter letters_written_in_the_third_person : Term.
Parameter filed_letters : Term.
Parameter letters_that_I_can_read : Term.
Parameter letters_written_on_one_sheet : Term.
Parameter crossed_letters : Term.
Parameter letters_written_by_Brown : Term.
Parameter letters_that_begin_with_'Dear_Sir' : Term.

Lemma I_cannot_read_any_of_Brown's_letters :
   holds (All dated_letters are letters_written_on_blue_paper) /\
   holds (No letters_written_in_black_ink are non letters_written_in_the_third_person) /\
   holds (No filed_letters are letters_that_I_can_read) /\
   holds (No letters_written_on_one_sheet are non dated_letters) /\
   holds (All non crossed_letters are letters_written_in_black_ink) /\
   holds (All letters_written_by_Brown are letters_that_begin_with_'Dear_Sir') /\
   holds (All letters_written_on_blue_paper are filed_letters) /\
   holds (No non letters_written_on_one_sheet are crossed_letters) /\
   holds (No letters_that_begin_with_'Dear_Sir' are letters_written_in_the_third_person)
   ->
   holds (No letters_written_by_Brown are letters_that_I_can_read).

Proof.
admit.
Qed.

End OtherExamples.