(* Time-stamp: *) (****************************************************************************) (* propositional.v *) (* *) (* Pierre Lescanne *) (* *) (* LIP (ENS-Lyon, CNRS, INRIA) *) (* *) (* *) (* Developed in V7.4 January 2001 --- March 2004 *) (****************************************************************************) Section Propositional_logic. Require Export false. (* ======== Syntax ======== *) Notation "|- p" := (theorem p) (at level 7). Infix RIGHTA 5 "=>" Imp. Infix 4 "&" AND. Infix 4 "V" OR. Notation "¬ p" := (Not p) (at level 3). (* ==================== OR Lemmas ======================= *) (* This lemma shows the connection between \/ (meta or) and V (object or) *) Lemma rule_OR :(p,q:proposition) |- p \/ |- q -> |- p V q. Proof. Intros. Elim H. Intros. Apply MP with p. Apply OR1. Assumption. Intros. Apply MP with q. Apply OR2. Assumption. Qed. Lemma rule_OR0:(p,q,r: proposition) |- p => r -> |- q => r -> |- (p V q) =>r. Proof. Intros. Apply MP with q => r. Apply MP with p => r. Apply OR0. Assumption. Assumption. Qed. Lemma Imp_OR1: (p,q,r:proposition) |- p => q -> |- p => q V r. Proof. Intros. Apply Cut_rule with q; Auto. Apply OR1. Qed. Lemma Imp_OR2: (p,q,r:proposition) |- p => r -> |- p => q V r. Proof. Intros. Apply Cut_rule with r; Auto. Apply OR2. Qed. Lemma OR_comm: (p,q: proposition) |- (p V q) => (q V p). Proof. Intros. Apply rule_OR0. Apply OR2. Apply OR1. Qed. Lemma rule_OR_comm: (p,q: proposition) |- (p V q) -> |- (q V p). Proof. Intros. Apply MP with p V q. Apply OR_comm. Assumption. Qed. Lemma OR_ass1: (p,q,r: proposition) |- (p V (q V r)) => ((p V q) V r). Proof. Intros. Apply rule_OR0. Apply Cut_rule with p V q. Apply OR1. Apply OR1. Apply rule_OR0. Apply Cut_rule with p V q. Apply OR2. Apply OR1. Apply OR2. Qed. Lemma OR_ass2: (p,q,r: proposition) |- ((p V q) V r) => (p V (q V r)). Proof. Intros. Apply rule_OR0. Apply rule_OR0. Apply OR1. Apply Cut_rule with q V r. Apply OR1. Apply OR2. Apply Cut_rule with q V r. Apply OR2. Apply OR2. Qed. Lemma OR_idempotence: (p: proposition) |- (p V p) => p. Intro. Apply rule_OR0. Apply I. Apply I. Qed. Lemma OR_left_regular: (p,q,r: proposition) |- (p => q) => (r V p) => (r V q). Proof. Intros. Apply rule_C. Apply rule_OR0. Apply Cut_rule with r V q. Apply OR1. Apply Hilbert_K. Apply rule_C. Apply MP with q => (r V q). Apply B. Apply OR2. Qed. Lemma rule_OR_left_regular: (p,q,r: proposition) |- p => q -> |- (r V p) => (r V q). Proof. Intros. Apply MP with p => q. Apply OR_left_regular. Assumption. Qed. Lemma OR_right_regular: (p,q,r: proposition) |- (p => q) => (p V r) => (q V r). Proof. Intros. Apply rule_C. Apply rule_OR0. Apply rule_C. Apply MP with q => (q V r). Apply B. Apply OR1. Apply Cut_rule with q V r. Apply OR2. Apply Hilbert_K. Qed. Lemma rule_OR_right_regular:(p,q,r: proposition) |- p => q -> |- (p V r) => (q V r). Proof. Intros. Apply MP with p => q. Apply OR_right_regular. Trivial. Qed. Lemma rule_glueOR: (p1,p2,q1,q2: proposition) |- p1 => q1 -> |- p2 => q2 -> |- (p1 V p2) => (q1 V q2). Proof. Intros. Apply rule_OR0. Apply Cut_rule with q1. Assumption. Apply OR1. Apply Cut_rule with q2. Assumption. Apply OR2. Qed. (* ==================== AND Lemmas ======================= *) Lemma rule_split_AND: (p1,p2: proposition) |- p1 -> |- p2 -> |- p1 & p2. Proof. Intros. Apply MP with p2. Apply MP with p1. Apply AND0. Assumption. Assumption. Qed. (* These lemmas shows the connection between /\ (meta and) and & (object and) *) Lemma rule_AND: (p1,p2: proposition) (|- p1) /\ (|- p2) -> |- p1 & p2. Proof. Intros. Elim H. Intros. Apply MP with p2. Apply MP with p1. Apply AND0. Assumption. Assumption. Qed. Lemma rule_AND_alt: (p1,p2:proposition) |- p1 & p2 -> (|- p1) /\ |- p2. Proof. Intros. Apply conj. Apply MP with p1&p2. Apply AND1. Assumption. Apply MP with p1&p2. Apply AND2. Assumption. Qed. Lemma Imp_AND:(p,q,r: proposition) |- (p => q => r) => (p & q) => r. Proof. Intros. Apply rule_C. Apply rule_CSI. Apply rule_C2. Apply Cut_rule with p. Apply AND1. Apply rule_C. Apply MP with (q => r) => (p&q) =>r. Apply B. Apply MP with (p&q) => q. Apply CB. Apply AND2. Qed. Lemma rule_Imp_AND:(p,q,r: proposition) |- p => q => r -> |- (p & q) => r. Proof. Intros. Apply MP with p=> q => r. Apply Imp_AND. Assumption. Qed. Lemma rule_Imp_AND_left:(p,q,r: proposition) |- p => r -> |- (p & q) => r. Proof. Intros. Apply rule_Imp_AND. Apply rule_Drop. Assumption. Qed. Lemma rule_Imp_AND_right:(p,q,r: proposition) |- q => r -> |- (p & q) => r. Proof. Intros. Apply rule_Imp_AND. Apply rule_C. Apply rule_Drop. Assumption. Qed. Lemma rule_AND_Imp: (p,q,r: proposition) |- (p => q) -> |- (p => r) -> |- (p => (q & r)). Proof. Intros. Apply rule_CSI. Apply MP with (p => r). Apply MP with r => p => (q & r). Apply B. Apply rule_C. Apply Cut_rule with q. Assumption. Apply AND0. Assumption. Qed. Lemma rule_rev_AND_Imp: (p,q,r: proposition) |- (p & q) => r -> |- p => q => r. Proof. Intros. Apply Cut_rule2 with (p & q). Assumption. Apply AND0. Qed. Lemma rule_glueAND: (p1,p2,q1,q2: proposition) |- p1 => q1 -> |- (p2 => q2) -> |- (p1 & p2) => (q1 & q2). Proof. Intros. Apply rule_CSI. Apply Cut_rule with q1. Apply Cut_rule with p1. Apply AND1. Assumption. Apply rule_C. Apply Cut_rule with p2. Apply AND2. Apply Cut_rule with q2. Assumption. Apply rule_C. Apply AND0. Qed. Lemma rule_glueAND2: (p1,p2,q1,q2,r1,r2: proposition) |- p1 => q1 => r1 -> |- p2 => q2 => r2 -> |- (p1 & p2) => (q1 & q2)=> (r1 & r2). Proof. Intros. Apply rule_rev_AND_Imp. Apply rule_AND_Imp. Apply rule_Imp_AND. Apply Cut_rule with p1. Apply AND1. Apply rule_C. Apply Cut_rule with q1. Apply AND1. Apply rule_C. Assumption. Apply rule_Imp_AND. Apply Cut_rule with p2. Apply AND2. Apply rule_C. Apply Cut_rule with q2. Apply AND2. Apply rule_C. Assumption. Qed. Lemma AND_drop1: (p1,p2: proposition) |- p1 & p2 -> |- p1. Proof. Intros. Apply MP with p1 & p2. Apply AND1. Assumption. Qed. Lemma AND_drop2: (p1,p2: proposition) |- p1 & p2 -> |- p2. Proof. Intros. Apply MP with p1 & p2. Apply AND2. Assumption. Qed. Lemma AND_comm: (p,q: proposition) |- (p & q) => (q & p). Proof. Intros. Apply rule_CSI. Apply Cut_rule with p. Apply AND1. Apply rule_C. Apply Cut_rule with q. Apply AND2. Apply AND0. Qed. Lemma rule_AND_comm: (p,q: proposition) |- p & q -> |- q & p. Proof. Intros. Apply MP with (p & q). Apply AND_comm. Assumption. Qed. Lemma AND_ass: (p,q,r: proposition) |- p & q & r => p & (q & r). Proof. Intros. Apply Cut_rule with (q & r) & p. Apply rule_CSI. Apply Cut_rule with p. Apply Cut_rule with (p & q). Apply AND1. Apply AND1. Apply rule_C. Apply rule_CSI. Apply Cut_rule with r. Apply AND2. Apply rule_C. Apply Cut_rule with q. Apply Cut_rule with (p & q). Apply AND1. Apply AND2. Apply MP with q => r => (q & r). Apply MP with (q & r) => (p => ((q & r) & p)). Apply rule_C. Apply Cut2. Apply AND0. Apply AND0. Apply AND_comm. Qed. Lemma AND_ass1: (p,q,r: proposition) |- p & (q & r)=> (p & q)& r. Proof. Intros. Apply Cut_rule with (r & (p & q)). Apply Cut_rule with (r & p) & q. Apply Cut_rule with q & (r & p). Apply Cut_rule with (q & r) & p. Apply AND_comm. Apply AND_ass. Apply AND_comm. Apply AND_ass. Apply AND_comm. Qed. Lemma rule_AND_ass: (p,q,r: proposition) |- (p & q) & r -> |- p & (q & r). Proof. Intros. Apply MP with (p & q) & r. Apply AND_ass. Assumption. Qed. Lemma rule_AND_ass1: (p,q,r: proposition) |- p & (q & r) -> |- (p & q) & r. Proof. Intros. Apply MP with (p & (q & r)). Apply AND_ass1. Assumption. Qed. Lemma AND_right_regular: (p,q,r: proposition) |- (p => q) => (p & r) => (q & r). Proof. Intros. Apply rule_C. Apply rule_CSI. Apply Cut_rule with r. Apply AND2. Apply rule_C. Apply MP with (p & r) => (p => q) => r => (q & r). Apply MP with ((p => q) => r => (q & r)) => r => (p => q) => (q & r). Apply rule_C. Apply CB. Apply Hilbert_C. Apply Cut_rule with p. Apply AND1. Apply rule_C. Apply MP with q => r => (q & r). Apply rule_C. Apply CB. Apply AND0. Qed. Lemma rule_AND_right_regular: (p,q,r: proposition) |- p => q -> |- p & r => q & r. Proof. Intros. Apply MP with p => q. Apply AND_right_regular. Assumption. Qed. Lemma AND_left_regular: (p,q,r: proposition) |- (p => q) => (r & p) => (r & q). Proof. Intros. Apply rule_C. Apply Cut_rule with p & r. Apply AND_comm. Apply Cut_rule2 with q & r. Apply AND_comm. Apply rule_C. Apply AND_right_regular. Qed. Lemma rule_AND_left_regular: (p,q,r: proposition) |- (p => q) -> |- r & p => r & q. Proof. Intros. Apply MP with p => q. Apply AND_left_regular. Assumption. Qed. Lemma AND_idempotence: (p: proposition) |- p => (p & p). Proof. Intros. Apply rule_CSI. Apply AND0. Qed. Lemma ANDAND: (p,q: proposition) |- (p & p) => q -> |- (p => q). Proof. Intros. Apply Cut_rule with (p & p). Apply AND_idempotence. Assumption. Qed. Lemma AND_perm: (p,q,r: proposition) |- p & (q & r) => r & (p & q). Proof. Intros. Apply Cut_rule with (p & q) & r. Apply AND_ass1. Apply AND_comm. Qed. Lemma rule_AND_perm: (p,q,r: proposition) |- p & (q & r) -> |- r & (p & q). Proof. Intros. Apply rule_AND_comm. Apply rule_AND_ass1. Assumption. Qed. Lemma AND_swap: (p,q,r: proposition) |- p & (q & r) => q & (p & r). Proof. Intros. Apply Cut_rule with (AND (p & q) r). Apply AND_ass1. Apply Cut_rule with (AND (q & p) r). Apply rule_AND_right_regular. Apply AND_comm. Apply AND_ass. Qed. (* ==================== Distributivity Lemmas ======================= *) Lemma undist_AND: (p,q,r: proposition) |- (p & q) V (p & r) => p & (q V r). Proof. Intros. Apply rule_OR0. Apply rule_AND_left_regular. Apply OR1. Apply rule_AND_left_regular. Apply OR2. Qed. Lemma undist_AND2: (p,q,r: proposition) |- (p & r) V (q & r) => (p V q) & r. Proof. Intros. Apply Cut_rule with r & (p V q). Apply Cut_rule with (r & p) V (r & q). Apply rule_glueOR; Apply AND_comm. Apply undist_AND. Apply AND_comm. Qed. Lemma dist_AND: (p,q,r: proposition) |- p & (q V r) => (p & q) V (p & r). Proof. Intros. Apply rule_Imp_AND. Apply rule_C. Apply rule_OR0. Apply rule_C. Apply Cut_rule2 with (p & q). Apply OR1. Apply AND0. Apply rule_C. Apply Cut_rule2 with (p & r). Apply OR2. Apply AND0. Qed. Lemma dist_AND2: (p,q,r: proposition) |- (p V q) & r => (p & r) V (q & r). Proof. Intros. Apply Cut_rule with r & (p V q). Apply AND_comm. Apply Cut_rule with (r & p) V (r & q). Apply dist_AND. Apply rule_glueOR; Apply AND_comm. Qed. Lemma undist_OR: (p,q,r: proposition) |- (p V q) & (p V r) => p V (q & r). Proof. Intros. Apply rule_Imp_AND. Apply rule_OR0. Apply rule_C. Apply MP with p => (p V (q & r)). Apply Hilbert_K. Apply OR1. Apply rule_C. Apply rule_OR0. Apply rule_C. Apply MP with p => (p V (q & r)). Apply Hilbert_K. Apply OR1. Apply Cut_rule2 with q & r. Apply OR2. Apply rule_C. Apply AND0. Qed. Lemma undist_OR2: (p,q,r: proposition) |- (q V p) & (r V p) => (q & r) V p. Proof. Intros. Apply Cut_rule with p V (q & r). Apply Cut_rule with (p V q) & (p V r). Apply rule_glueAND; Apply OR_comm. Apply undist_OR. Apply OR_comm. Qed. Lemma dist_OR: (p,q,r: proposition) |- p V (q & r) => (p V q) & (p V r). Proof. Intros. Apply rule_OR0. Apply rule_CSI. Apply Cut_rule with p V q. Apply OR1. Apply rule_C. Apply Cut_rule with p V r. Apply OR1. Apply rule_C. Apply AND0. Apply rule_Imp_AND. Apply Cut_rule with p V q. Apply OR2. Apply rule_C. Apply Cut_rule with p V r. Apply OR2. Apply rule_C. Apply AND0. Qed. Lemma p_or_r_and_q_or_r: (p,q,r:proposition) |- (p V r) & (q V r) => (p & q) V r. Proof. Intros. Apply Cut_rule with (p & (q V r)) V (r & (q V r)). Apply dist_AND2. Apply Cut_rule with (p & (q V r)) V r. Apply rule_OR_left_regular. Apply AND1. Apply Cut_rule with (p & q) V ((p & r) V r). Apply Cut_rule with (p & q) V (p & r) V r. Apply rule_OR_right_regular. Apply dist_AND. Apply OR_ass2. Apply rule_OR_left_regular. Apply rule_OR0. Apply AND2. Apply I. Qed. (* ==================== Lemmas about Not ======================= *) Lemma AND_Not: (p,q:proposition) |- ¬(p V q) => ¬p & ¬q. Proof. Intros. Unfold Not. Apply rule_AND_Imp. Apply MP with p => (p V q). Apply Contraposition with q:=(p V q) p:=p. Apply OR1. Apply MP with q => (p V q). Apply Contraposition with q:=(p V q) p:=q. Apply OR2. Qed. Lemma AND_Not_rule: (p,q:proposition) |- ¬(p V q) -> |- ¬p & ¬q. Proof. Intros. Apply MP with ¬(p V q). Apply AND_Not. Assumption. Qed. Lemma Not_OR: (p,q:proposition) |- ¬p & ¬q => ¬(p V q). Proof. Intros. Unfold Not. Apply rule_Imp_AND. Apply OR0. Qed. Lemma rule_Not_OR: (p,q:proposition) |- ¬p & ¬q -> |- ¬(p V q). Proof. Intros. Apply MP with ¬p & ¬q. Apply Not_OR. Assumption. Qed. Lemma Not_AND: (p,q:proposition) |- ¬p V ¬q => ¬(p & q). Proof. Unfold Not. Intros. Apply rule_OR0. Apply rule_C. Apply Cut_rule with p. Apply AND1. Apply rule_C. Apply I. Apply rule_C. Apply Cut_rule with q. Apply AND2. Apply rule_C. Apply I. Qed. Lemma rule_Not_AND: (p,q:proposition) |- ¬p V ¬q -> |- ¬(p & q). Proof. Intros. Apply MP with ¬p V ¬q. Apply Not_AND. Assumption. Qed. Lemma Not_p_AND_p: (p:proposition) |- ¬p & p => FALSE. Proof. Intros. Unfold Not. Apply rule_Imp_AND. Apply I. Qed. Lemma OR_FALSE: (p:proposition) |- p V FALSE => p. Proof. Intros. Apply rule_OR0. Apply I. Apply False_Imp_everything. Qed. Lemma AND_FALSE: (p:proposition) |- p & FALSE => FALSE. Proof. Intros. Apply rule_Imp_AND. Apply KI. Qed. Lemma AND_TRUE: (p:proposition) |- p => p & TRUE. Proof. Intros. Apply rule_AND_Imp. Apply I. Apply Everything_Imp_True. Qed. (* ==================== Xor ======================= *) Definition Xor := [p,q:proposition] (p V q) & ¬(p & q). Infix RIGHTA 4 "|" Xor. Lemma Xor_Imp: (p,q:proposition) |- (p | q) => ¬p => q. Proof. Intros. Unfold Xor. Apply rule_Imp_AND. Apply rule_Drop. Apply rule_OR0. Unfold Not. Apply rule_C. Apply MP with FALSE => q. Apply B. Apply False_Imp_everything. Apply Hilbert_K. Qed. Lemma Xor_comm: (p,q:proposition) |- p | q => q | p. Intros p q. Unfold Xor. Apply rule_glueAND. Apply OR_comm. Apply rule_Contrapos1. Apply AND_comm. Qed. End Propositional_logic.