Wang's algorithm in Coq.

wangsAlgorithm.v

Require Import List.
Require Import Datatypes.
Require Export Coq.Strings.String.
Require Export Coq.Lists.List.
Inductive CL: Type :=
  | var (a: string)
  | CLNot (a: CL)
  | CLAnd (a1 a2: CL)
  | CLOr (a1 a2: CL)
  | CLImp (a1 a2: CL).

Notation "x '" := (var x) (at  level 59).
Notation "~! x" := (CLNot x) (at level 60).
Notation "x &! y" := (CLAnd x y) (at level 62).
Notation "x |! y"  := (CLOr x y) (at level 63).
Notation "x ->! y" := (CLImp x y) (at level 61).

Definition CLSet: Type := list CL.
Definition Sequent: Type := (CLSet * CLSet).

Definition eqclb (a b: CL): bool :=
  match a, b with
  | (var v1), (var v2) => (eqb v1 v2)
  | _, _ => false
  end.

Definition initialSequent (l1 l2: CLSet): bool :=
  (existsb (fun x => (existsb (eqclb x) l2)) l1).

Theorem aboutInitialSequent: forall x y: CLSet, (initialSequent x y) = true <-> exists c: CL, In c x /\ In c y.

Fixpoint wang (Gam Del: CLSet) (d: nat): bool :=
  match Gam, Del, d with
  | _, _, 0 => false
  | G, (~!a)::D, S d' => wang (a::G) D d'
  | (~! a)::G, D, S d' => wang G (a::D) d'
  | G, (a &! b)::D, S d' => (wang G (a::D) d') && (wang G (b::D) d')
  | (a &! b)::G, D, S d' => (wang (a::b::G) D d')
  | G, (a |! b)::D, S d' => (wang G (a::b::D) d')
  | (a |! b)::G, D, S d' => (wang (a::G) D d') && (wang (b::G) D d')
  | G, (a ->! b)::D, S d' => (wang (a::G) (b::D) d')
  | (a ->! b)::G, D, S d' => (wang G (a::D) d') && (wang (b::G) D d')
  | a::G, b::D, S d' => initialSequent (a::G) (b::D) || wang (G ++ (a::nil)) (D ++ (b::nil)) d'
  | G, b::D, S d' => initialSequent G (b::D) || wang G (D ++ (b::nil)) d'
  | a::G, D, S d' => initialSequent (a::G) D || wang (G ++ (a::nil)) D d'
  | _, _, _ => false
  end.

Eval compute in (wang nil (("a"' |! ~! "a"')::nil) 1000).
Eval compute in (wang (("a"' |! "b"')::nil) (("b"' |! "a"')::nil) 1000).