prop.v

Print list.

Fixpoint In {A} (a:A) (l:list A) : Prop :=
  match l with
    | nil => False
    | cons b m => b = a \/ In a m
  end.

Print nil.

Print or.
Print eq.

Context {atom : Type}.

Inductive prop1 : Type :=
  | atom_prop1 : atom -> prop1.

Print prop1.
Check atom.
Print atom.

Inductive SC_proves1 : list prop1 -> prop1 -> Prop :=
  | SC_init1  Γ P : In P Γ -> SC_proves1 Γ P.

Print False.

Inductive prop : Type :=
| atom_prop : atom -> prop
| bot_prop : prop
| top_prop : prop
| and_prop : prop -> prop  -> prop
| or_prop : prop  -> prop  -> prop
| impl_prop : prop  -> prop  -> prop.

Notation "⊥" := bot_prop.
Notation "⊤" := top_prop.
Infix "∧" := and_prop (left associativity, at level 52).
Infix "∨" := or_prop (left associativity, at level 53).
Infix "⊃" := impl_prop (right associativity, at level 54).

Definition not_prop (P : prop) := P ⊃ ⊥.

Notation "¬ P" := (not_prop P) (at level 51).

Infix "∈" := In (right associativity, at level 55).
Notation "x → y" := (x -> y) (at level 99, y at level 200, right associativity).

Open Scope list_scope.

Reserved Notation "Γ ⇒ P" (no associativity, at level 61).

Inductive SC_proves : list prop -> prop -> Prop :=
| SC_init P Γ : P ∈ Γ → Γ  ⇒ P
| SC_bot_elim P Γ : ⊥ ∈ Γ → Γ ⇒ P
| SC_top_intro Γ : Γ ⇒ ⊤
| SC_and_intro Γ P Q : Γ ⇒ P → Γ ⇒ Q → Γ ⇒ P ∧ Q
| SC_and_elim Γ P Q R : P ∧ Q ∈ Γ → P :: Q :: Γ ⇒ R → Γ ⇒ R
| SC_or_introl Γ P Q :  Γ ⇒ P → Γ ⇒ P ∨ Q
| SC_or_intror Γ P Q : Γ ⇒ Q → Γ ⇒ P ∨ Q
| SC_or_elim Γ P Q R : P ∨ Q ∈ Γ → P :: Γ ⇒ R → Q :: Γ ⇒ R → Γ ⇒ R
| SC_impl_intro Γ P Q : P :: Γ ⇒ Q → Γ ⇒ P ⊃ Q
| SC_impl_elim Γ P Q R : P ⊃ Q ∈ Γ → Γ ⇒ P → Q :: Γ ⇒ R → Γ ⇒ R
  where "Γ ⇒ P" := (SC_proves Γ P).

Notation "⇒ P" := (nil ⇒ P) (no associativity, at level 61).

Theorem PP : forall P, ⇒ P⊃P.
Proof.
intros.
apply SC_impl_intro.
apply SC_init.
simpl. apply or_introl. reflexivity. Qed.

Theorem and_comm : forall P Q, ⇒ P∧Q ⊃ Q∧P.
Proof.
 intros.
 apply SC_impl_intro.
 apply SC_and_intro.
 + apply (SC_and_elim _ P Q _).
    - simpl. apply or_introl. reflexivity.
    - apply SC_init. simpl. apply or_intror. apply or_introl. reflexivity.
 + apply (SC_and_elim _ P Q _).
    - simpl. apply or_introl. reflexivity.
    - apply SC_init. simpl. apply or_introl. reflexivity.
Qed.

Theorem or_comm : forall P Q, ⇒ P∨Q ⊃ Q∨P.
Proof.
  intros.
  apply SC_impl_intro.
  apply (SC_or_elim (P ∨ Q :: nil) P Q (Q ∨ P)).
  + simpl. apply or_introl. reflexivity.
  + apply SC_or_intror. apply SC_init. simpl. apply or_introl. reflexivity.
  + apply SC_or_introl. apply SC_init. simpl. apply or_introl. reflexivity.
Qed.

Theorem PQP : forall P Q, ⇒ P ⊃ Q⊃P.
Proof.
  intros.
  apply SC_impl_intro.
  apply SC_impl_intro.
  apply SC_init.
  simpl. apply or_intror. apply or_introl. reflexivity.
Qed.

Theorem syllogism : forall P Q R, P⊃Q :: Q⊃R :: nil ⇒ P⊃R.
Proof.
  intros.
  apply SC_impl_intro.
  apply (SC_impl_elim _ P Q R).
  +  simpl. apply or_intror. apply or_introl. reflexivity.
  +  apply SC_init. simpl. apply or_introl. reflexivity.
  +  apply (SC_impl_elim _ Q R R).
      -  simpl. apply or_intror. apply or_intror. apply or_intror. apply or_introl. reflexivity.
      -  apply SC_init. simpl. apply or_introl. reflexivity.
      -  apply SC_init. simpl. apply or_introl. reflexivity.
Qed.

Theorem exp : forall P, ⇒ ⊥⊃P.
Proof.
  intros.
  apply SC_impl_intro.
  apply SC_bot_elim.
  simpl. apply or_introl. reflexivity.
Qed.