Skip to content

Instantly share code, notes, and snippets.

@myazakky

myazakky/wangsAlgorithm.v

Created January 29, 2022 22:41
Show Gist options
  • Save myazakky/3672680fe53e7ca80355bf913d6a9dd0 to your computer and use it in GitHub Desktop.
Save myazakky/3672680fe53e7ca80355bf913d6a9dd0 to your computer and use it in GitHub Desktop.
Download ZIP
Wang's algorithm in Coq.
Raw
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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment