(* Icharate Light: Pierre Castéran, Houda Anoun *) Inductive Atom : Set := _n | _np | _s | _wh | _pp. Check _n. (* all constructors are distinct *) Lemma n_np : _n <> _np. Proof. discriminate. Qed. (* every atomic type is one of the constructors *) Lemma atom_enum : forall a:Atom, a = _s \/ a = _np \/ a = _n \/ a = _pp \/ a = _wh. Proof. intro. (* let a be of type Atom *) case a; auto. Qed. (* definition by pattern matching *) Definition is_axiom (a:Atom) : Prop := match a with | _s => True | _ => False end. Goal ~(is_axiom _np). simpl. auto. Save np_not_ax. Definition atom_eq_dec : forall a a':Atom, {a=a'}+{a<>a'}. intro a; case a; intro a';case a'; try (right;discriminate); try (left;trivial). Defined. Inductive Form : Set := | At : Atom -> Form | Slash : Form -> Form -> Form | Backslash : Form -> Form -> Form | Dot : Form -> Form -> Form. Notation "A // B" := (Slash A B) (at level 41, right associativity) : lbk_scope. Notation " A \\ B" := (Backslash A B) (at level 41, right associativity) : lbk_scope. Notation " A 'o' B" := (Dot A B) (at level 42, left associativity) : lbk_scope. Notation "! a" := (At a) (at level 40): lbk_scope. Definition Suc := S. Definition np := (At _np). Definition n := (At _n). Definition pp := (At _pp). Definition wh := (At _wh). Definition s := (At _s). Delimit Scope lbk_scope with lbk. Check (Dot (At _np) (Backslash (At _np) (Slash (At _s) (At _np)))). Open Scope lbk_scope. Check (Dot np (Backslash np (Slash s np))). Definition atomic (f : Form) := match f with At _ => True | _ => False end. Fixpoint size (f:Form): nat := match f with !a => 1 | g // h => size g + size h | g \\ h => size g + size h | g o h => size g + size h end. Eval compute in size (np o np \\ s // np). Lemma size_pos : forall f, size f > 0. Require Import Arith. induction f;simpl;auto with arith. Qed. Lemma size_pos_with_details : forall f, size f > 0. induction f. simpl. auto with arith. simpl. auto with arith. simpl. auto with arith. simpl. auto with arith. Qed. Lemma size_slash_gt1 : forall f g, size (f // g) > size f. intros f g. simpl. generalize (size_pos g). auto with arith. Require Import Omega. omega. Qed. Hint Resolve size_slash_gt1 :ctl. Goal forall A B, (A // B) <> A. Proof. induction A; intro B; case B; intros; try discriminate; intro H; injection H; intros; intuition eauto. Save L0. Goal forall A B, (A // B) <> A. Proof. intros A B H. absurd (size (A//B) > size A). rewrite H;auto with arith. auto with ctl. Save L'0. Require Import ZArith. Open Scope Z_scope. Fixpoint polarform (p:Atom)(F : Form){struct F}:Z := match F with (At a) => (if atom_eq_dec p a then 1 else 0) | A // B => polarform p A - polarform p B | B \\ A => polarform p A - polarform p B | A o B => polarform p A + polarform p B end.