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.

Definition not_prop (P : prop) :=
  impl_prop P (bot_prop).


Inductive SC_proves : list prop -> prop -> Prop :=
| SC_init P Γ : In P Γ -> SC_proves Γ P
| SC_bot_elim P Γ : In bot_prop Γ -> SC_proves Γ P
| SC_top_intro Γ : SC_proves Γ top_prop
| SC_and_intro Γ P Q : SC_proves Γ P -> SC_proves Γ Q -> SC_proves Γ (and_prop P Q)
| SC_and_elim Γ P Q R : In (and_prop P Q) Γ -> 
        SC_proves (cons P (cons Q Γ)) R -> SC_proves Γ R
| SC_or_introl Γ P Q : SC_proves Γ P -> SC_proves Γ (or_prop P Q)
| SC_or_intror Γ P Q : SC_proves Γ Q -> SC_proves Γ (or_prop P Q)
| SC_or_elim Γ P Q R : In (or_prop P Q) Γ -> SC_proves (cons P Γ)  R ->
        SC_proves (cons Q Γ) R -> SC_proves Γ R
| SC_impl_intro Γ P Q : SC_proves (cons P Γ) Q -> SC_proves Γ (impl_prop P Q)
| SC_impl_elim Γ P Q R : In (impl_prop P Q) Γ -> SC_proves Γ P ->
        SC_proves (cons Q Γ) R -> SC_proves Γ R.

Theorem PP : forall P, SC_proves nil (impl_prop P P).
Proof.
intros.
apply SC_impl_intro.
apply SC_init.
simpl. apply or_introl. reflexivity. Qed.

Theorem and_comm : forall P Q, SC_proves nil 
    (impl_prop (and_prop P Q) (and_prop 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, SC_proves nil
    (impl_prop (or_prop P Q) (or_prop Q P)).
Proof.
  intros.
  apply SC_impl_intro.
  apply (SC_or_elim (cons (or_prop P Q) nil) P Q (or_prop 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, SC_proves nil 
    (impl_prop P (impl_prop 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, SC_proves
    (cons (impl_prop P Q) (cons (impl_prop Q R) nil)) (impl_prop 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, SC_proves nil 
      (impl_prop (bot_prop) P).
Proof.
  intros.
  apply SC_impl_intro.
  apply SC_bot_elim.
  simpl. apply or_introl. reflexivity.
Qed.