61 lines
1.6 KiB
Coq
61 lines
1.6 KiB
Coq
(* Boolean formula *)
|
||
Inductive boolf: Type :=
|
||
| Atom: bool -> boolf
|
||
| Neg: boolf -> boolf
|
||
| And: boolf -> boolf -> boolf
|
||
| Or: boolf -> boolf -> boolf
|
||
| Impl: boolf -> boolf -> boolf.
|
||
Notation "⊤" := (Atom true) (at level 10).
|
||
Notation "⊥" := (Atom false) (at level 10).
|
||
Notation "'¬' b" := (Neg b) (at level 10).
|
||
Infix "∧" := And (at level 15).
|
||
Infix "∨" := Or (at level 20).
|
||
Infix "→" := Impl (at level 25).
|
||
|
||
Example f1 := ((⊤ ∨ ⊥) ∧ ⊥) → (¬ ⊥).
|
||
|
||
Inductive kont {V:Type}: Type :=
|
||
| Letk: kont -> kont -> kont.
|
||
Arguments kont: clear implicits.
|
||
|
||
Inductive kont {V:Type}: Type :=
|
||
| KAtom: bool -> kont
|
||
| KNeg: kont -> kont
|
||
| KAnd: (V -> kont) -> (V -> kont) -> kont
|
||
| KOr: (V -> kont) -> (V -> kont) -> kont
|
||
| KImpl: (V -> kont) -> (V -> kont) -> kont.
|
||
Arguments kont: clear implicits.
|
||
|
||
Fixpoint compile {V:Type} (f:boolf): kont V :=
|
||
match f with
|
||
| Atom b => KAtom b
|
||
| Neg f => KNeg (compile f)
|
||
| And f1 f2 => KAnd (fun k => compile f1) (fun k => compile f2)
|
||
| Or f1 f2 => KOr (fun k => compile f1) (fun k => compile f2)
|
||
| Impl f1 f2 => KImpl (fun k => compile f1) (fun k => compile f2)
|
||
end.
|
||
|
||
Check compile (V:=unit) f1.
|
||
Compute compile (V:=unit) f1.
|
||
(* https://en.wikipedia.org/wiki/Tseytin_transformation *)
|
||
|
||
Inductive cnf: Type :=
|
||
| CTru | CFls: cnf
|
||
| CNeg: cnf -> cnf
|
||
| CCons: cnf -> cnf -> cnf.
|
||
|
||
Fixpoint cnfy (f:boolf): cnf :=
|
||
match f with
|
||
| Tru => CTru
|
||
| Fls => CFls
|
||
| Neg b => CNeg (cnfy b)
|
||
| And Fls _ => CFls
|
||
| And _ Fls => CFls
|
||
| And Tru f2 => cnfy f2
|
||
| And f1 Tru => cnfy f1
|
||
| And f1 f2 =>
|
||
| Or f1 f2 =>
|
||
| Impl f1 f2 => CCons (CNeg (cnfy f1)) (cnfy f2)
|
||
end.
|
||
|