sequent_cal.v

Require Import List.
Import ListNotations.

Variable var : Type.
Variable tru fls : var.

Inductive prop :=
  | Var : var -> prop
  | Not : prop -> prop
  | And : prop -> prop -> prop
  | Or : prop -> prop -> prop
  | Imp : prop -> prop -> prop.

Definition Bot := Var tru.
Definition Top := Not Bot.

Notation "# p" := (Var p) (at level 1).
Notation "A ∨ B" := (Or A B) (at level 15, right associativity).
Notation "A ∧ B" := (And A B) (at level 15, right associativity).
Notation "A ⊃ B" := (Imp A B) (at level 16, right associativity).
Notation "⊥" := Bot (at level 0).
Notation "¬ A" := (Not A) (at level 5).
Notation "⊤" := Top (at level 0).

Definition assign := var -> bool.

Fixpoint valuation (v : assign) (A : prop) :=
  match A with
  | # p => v p
  | ¬ A => negb (valuation v A)
  | A ∧ B => andb (valuation v A) (valuation v B)
  | A ∨ B => orb (valuation v A) (valuation v B)
  | A ⊃ B => implb (valuation v A) (valuation v B)
  end.

Definition tautology A :=
  forall v, valuation v A = true.

Definition equiv A B :=
  (A ⊃ B) ∧ (B ⊃ A).

Definition eqtot A B :=
  tautology (equiv A B).

Reserved Notation "Γ → Δ" (at level 80).
Inductive prv : list prop -> list prop -> Prop :=
  | init A : [A] → [A]

  | weakL A Γ Δ : 
    Γ → Δ -> (A :: Γ) → Δ
  | weakR A Γ Δ : Γ → Δ -> Γ → (Δ ++ [A])

  | contraL A Γ Δ : (A :: A :: Γ) → Δ -> (A :: Γ) → Δ
  | contraR A Γ Δ : Γ → (Δ ++ [A ; A]) -> Γ → (Δ ++ [A])

  | changeL A B Γ Π Δ : (Γ ++ A :: B :: Π) → Δ -> (Γ ++ B :: A :: Π) → Δ
  | changeR A B Γ Δ Σ : Γ → (Δ ++ A :: B :: Σ) -> Γ → (Δ ++ B :: A :: Σ)

  | cut A Γ Π Δ Σ : Γ → (Δ ++ [A]) -> A :: Π → Σ -> Γ ++ Π → Δ ++ Σ

  | andL1 A B Γ Δ : A :: Γ → Δ ->  A ∧ B :: Γ → Δ
  | andL2 A B Γ Δ : B :: Γ → Δ ->  A ∧ B :: Γ → Δ
  | andR A B Γ Δ : Γ → Δ ++ [A] -> Γ → Δ ++ [B] ->  Γ → Δ ++ [A ∧ B]

  | orL A B Γ Δ : A :: Γ → Δ -> B :: Γ → Δ -> A ∨ B :: Γ → Δ
  | orR1 A B Γ Δ : Γ → Δ ++ [A] -> Γ → Δ ++ [A ∨ B]
  | orR2 A B Γ Δ : Γ → Δ ++ [B] -> Γ → Δ ++ [A ∨ B]

  | impL A B Γ Π Δ Σ : Γ → Δ ++ [A] -> B :: Π → Σ -> A ⊃ B :: Γ ++ Π → Δ ++ Σ
  | impR A B Γ Δ : A :: Γ → Δ ++ [B] -> Γ → Δ ++ [A ⊃ B]

  | notL A Γ Δ : Γ → Δ ++ [A] -> ¬ A :: Γ → Δ
  | notR A Γ Δ : A :: Γ → Δ -> Γ → Δ ++ [¬ A]

  where "Γ → Δ" := (prv Γ Δ).

Goal forall A, [] → [A ∨ ¬ A].
Proof.
  intro A.
  assert ([A ∨ ¬ A] = [] ++ [A ∨ ¬ A]) by  auto.
  rewrite H; clear H.
  apply contraR.

  assert ([] ++ [A ∨ ¬ A; A ∨ ¬ A] = [A ∨ ¬ A] ++ [A ∨ ¬ A]) by auto.
  rewrite H; clear H; apply orR1.

  assert ([A ∨ ¬ A] ++ [A] = [] ++ A ∨ ¬ A :: A :: []) by auto.
  rewrite H; clear H. apply changeR.

  assert ([] ++ [A; A ∨ ¬ A] = [A] ++ [A ∨ ¬ A]) by auto.
  rewrite H; clear H ; apply orR2.

  apply notR.
  apply init.
Qed.