LogicExamples.v

Module ClassicLogic.
  Definition LEM := forall A : Prop, A \/ ~A.
  Definition CONTRA := forall A B : Prop, (~A -> ~B) -> (B -> A).

  Axiom lem : LEM.
  Axiom contra : CONTRA.

  Notation "( x , y , .. , z )" := (conj .. (conj x y) .. z) (at level 0).
End ClassicLogic.

Set Firstorder Depth 200.

Module Q1.
  (*1. Каждая тряка шмакает такую тряку, которая себя не шмакает.
    2. Каждая грылая тряка себя шмакает, а любую негрылую не шмакает.
    
    Вопрос 1. Существуют ли грылые тряки?
    Вопрос 2. Обязательно ли каждая негрылая тряка себя не шмакает?*)


  Variable X : Type.
  Variable P : X -> X -> Prop.
  Variable Q : X -> Prop.
  Definition A1 := forall x : X, exists y, ~(P y y) /\ (P x y).
  Definition A2 := forall x : X, (Q x -> P x x) /\ (forall y : X, ~(Q y) -> ~(P x y)).
  
  Import ClassicLogic.
  
  Axiom a1 : A1.
  Axiom a2 : A2.
  Axiom X0 : X.
  
  Theorem exX : exists x : X, True.
  Proof.
    exists X0. auto.
  Qed.
  
  Definition axioms := (a1, a2, lem, contra, exX).
  
  (*manual proof*)
  Theorem t1 : exists x : X, Q x. (*question 1 statement*)
  Proof.
    destruct (a1 X0). (*apply a1*)
    destruct H. (*conjunction elimination*)
    assert (aux : forall x y, (P x y) -> (Q y)).
    {
      intros x0 y0 HH.
      apply (contra (Q y0) (P x0 y0)).
      - destruct (a2 x0).
        apply H2.
      - assumption.
    }
    exists x.
    apply (aux X0).
    assumption.
  Qed.
  
  (*auto proof*)
  Theorem t1' : exists x : X, Q x.
  Proof.
    firstorder using axioms.
  Qed.
  
  (*manual proof for question 2*)
  Theorem t2 : forall x : X, ~(Q x) -> ~(P x x). (*question 2 statement*) 
  Proof.
    intros. destruct (a2 x).
    apply H1. assumption.
  Qed.

  (*auto proof*)
  Theorem t2' : forall x : X, ~(Q x) -> ~(P x x).
  Proof.
    firstorder using axioms.
  Qed.
  
End Q1.