(* ESSLLI 2004 : Coq for natural language *) (* Using a previously compiled module (NL.vo) *) Require Import NL. Check _np. Check np. Check s. Check true. Check O. Check -34. Check 2=3. (* declarations *) Parameter Word : Set. Parameters mary likes pierre : Word. Check mary. Search Word. Search Atom. (* functions: application and abstraction *) Check Zplus. Check (Zplus 5 (-2)). Check (Zplus (-5)). Check At. Check Slash. Check Dot. Search Form. Check np \\ s. Check np o np \\ s. Check (Backslash np (Slash s np)). Check fun z:Z => 2*z. Definition double z := 2*z. Definition lift A B := B // (A \\ B). Print lift. Eval compute in lift s np. Definition dist2 z z' := let d := z - z' in d*d. Check (dist2 4 (-6)). Eval compute in (dist2 4 (-6)). Check polarform. Check (polarform _np (lift s np)). Eval compute in polarform _np (lift s np). (* propositions and proofs *) Check is_axiom. Check 2=3. Check 1+1=2. Check (is_axiom _np). Check atomic. Check (atomic (lift s np)). Check polarform _np (lift s np) = 0. Check NL_complete. Check NL_sound. Search NL_complete. Check NL_completeness_thm. Print NL_completeness_thm. Section Minimal_Propositional_Logic. Variables P Q R S : Prop. Check P->Q. Check P->Q->R. Check fun p:P => p. Check fun (p:P)(q:Q) => p. Theorem KPQ : P -> Q -> P. Proof fun p q => p. (* exo *) Check fun (H:P->P->Q)(p:P) => H p p. Theorem imp_trans : (P->Q)->(Q->R)->P->R. Proof fun (H:P->Q)(H':Q->R)(p:P)=> (H' (H p)). Theorem imp_trans' : (P->Q)->(Q->R)->P->R. Proof. intro H. intros H' p. apply H'. apply H. assumption. Qed. Theorem imp_trans_2 : (P->Q)->(Q->R)->P->R. Proof. intros H H' p. apply H'; apply H. assumption. Qed. Theorem imp_trans_3 : (P->Q)->(Q->R)->P->R. Proof. auto. Qed. Print imp_trans_3. End Minimal_Propositional_Logic. Section Propositional_Logic. Variables P Q R S: Prop. Check and. Check or. Check not. Check False. Theorem and_comm : P/\Q -> Q/\P. Proof. intro H;elim H;split;trivial. Qed. Theorem or_comm : P\/Q -> Q\/P. Proof. intro H;elim H. intro;right;assumption. intro;left;assumption. Qed. Theorem contrap : (P->Q)->~Q -> ~P. Proof. intros H H0. red; intro p. elim H0;auto. Qed. End Propositional_Logic. (* dependent products *) Check (forall z:Z, z < z+1). Theorem all_perm : forall (A:Set)(P:A->A->Prop), (forall x y, P x y)-> forall x y, P y x. auto. Qed. Lemma toy : (forall x y:Z, x < y) -> forall x y:Z, y < x. intros; apply all_perm. assumption. Qed. Theorem le_double : forall z, 0 <= z -> z <= 2 * z. auto with zarith. Qed. Check (le_double 5). Goal forall z, z * z <= 2 * (z * z). intro z; apply le_double. auto with zarith. case z; simpl ; auto with zarith. Save double_square. Section Predicate_logic. Lemma eqn : exists z:Z, z+z = z*z. Proof. exists 2. simpl; trivial. Qed. Section A_fixed. Variable A:Set. Variables P Q S: A->Prop. Variable R : A->A->Prop. Lemma all_not_ex_not : (forall a, P a)->~(exists a, ~(P a)). Proof. red; intros H H0. elim H0; intros b Hb. elim Hb;apply H. Qed. End A_fixed. Lemma no_diff : forall A:Set, A -> ~(forall x y: A, x<>y). Proof. intros A a H. elim (H a a). trivial. Qed. Lemma L: (exists n:Z, forall p:Z, n<>p ) -> 2=3. intro H; elim H. intros x Hx. elim (Hx x). reflexivity. Qed. End Predicate_logic. Section proof_by_induction. Open Scope nat_scope. Theorem plus_assoc: forall n p q, (n+p)+q = n+(p+q). Proof. intro n; elim n; simpl; auto. Qed. Close Scope nat_scope. End proof_by_induction. SearchPattern (NL_arrow ?X1 ?X1). Print NL_arrow. Check one. Check (one (np\\s)). Definition deriv0 : np \\ s -NL-> np \\ s := one (np\\s). Definition deriv0' : np \\ s -NL-> np \\ s. apply one. Defined. Definition deriv0'' : np \\ s -NL-> np \\ s. auto with ctl. Defined. (* building/applying new derived rules *) Lemma scheme1 : forall A B, A -NL-> (A o B) //B. auto with ctl. Defined. Lemma ex2 : (np\\s)//np -NL-> ((np\\s)//np o np)//np. apply scheme1. Defined. (* induction *) Check list_ind. Print length. Set Implicit Arguments. Fixpoint length (A:Set)(l:list A){struct l} : nat := match l with nil => O | (x::l')=> S (length l') end. Fixpoint app (A:Set)(l l': list A) {struct l}: list A := match l with nil => l' | a::l1 => a::(app l1 l') end. Theorem app_assoc : forall (A:Set) (l1 l2 l3: list A), app l1 (app l2 l3) = app (app l1 l2) l3. induction l1; simpl;auto. intros; rewrite IHl1; auto. Qed. Lemma ex5 : (np o (np // (s // np)) o np) -NL-> s -> False. intro H; elim H. Abort. Theorem Hilbert_polar : forall A B a, A -NL-> B -> polarform a A = polarform a B. intros A B a H; elim H; simpl; auto with zarith. Qed. Lemma ex5 : (np o (np // (s // np)) o np) -NL-> s -> False. intro H; elim H. Restart. intro H; generalize (Hilbert_polar _np H). simpl. auto with zarith. Qed. Ltac noderiv H atom := match goal with H : NL_arrow ?A ?B |- False => generalize(Hilbert_polar atom H); simpl ; auto with zarith end. Lemma ex5' : np o np//s//np o np -NL-> s -> False. intro H. noderiv H _s. Defined. Lemma ex5'' : ^np oo ^(np // (s // np)) oo ^np ==> s -> False. intro H. apply ex5'. generalize (seqToNL_arrow H). simpl; auto. Qed. Ltac noderiv_plus H atom := match goal with H : NL_arrow ?A ?B |- False => generalize(Hilbert_polar atom H); simpl ; auto with zarith |H : ?Gamma ==> ?A |- False => generalize (seqToNL_arrow H); let fr := fresh in (intro fr ; generalize (Hilbert_polar atom fr); simpl ; auto with zarith) end. Ltac noderiv_elim H atom := cut False ; [destruct 1 | noderiv_plus H atom]. Lemma ex5''' : ^np oo ^(np // (s // np)) oo ^np ==> s -> 2=3. intro H. noderiv_elim H _np. Qed.