From a55a98b4268805ece49deb171af9ae1785b931a2 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 28 Feb 2021 17:19:06 -0500 Subject: [PATCH] RuleInduction: some propositional logic, with slightly naughty use of excluded middle --- RuleInduction.v | 663 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 663 insertions(+) diff --git a/RuleInduction.v b/RuleInduction.v index c04ae98..547f8b7 100644 --- a/RuleInduction.v +++ b/RuleInduction.v @@ -220,3 +220,666 @@ Proof. apply Permutation_app2. assumption. Qed. + + +(** * Simple propositional logic *) + +Module SimplePropositional. + Inductive prop := + | Truth + | Falsehood + | Var (x : var) + | And (p1 p2 : prop) + | Or (p1 p2 : prop). + + Inductive valid (vars : var -> Prop) : prop -> Prop := + | ValidTruth : + valid vars Truth + | ValidVar : forall x, + vars x + -> valid vars (Var x) + | ValidAnd : forall p1 p2, + valid vars p1 + -> valid vars p2 + -> valid vars (And p1 p2) + | ValidOr1 : forall p1 p2, + valid vars p1 + -> valid vars (Or p1 p2) + | ValidOr2 : forall p1 p2, + valid vars p2 + -> valid vars (Or p1 p2). + + Fixpoint interp (vars : var -> Prop) (p : prop) : Prop := + match p with + | Truth => True + | Falsehood => False + | Var x => vars x + | And p1 p2 => interp vars p1 /\ interp vars p2 + | Or p1 p2 => interp vars p1 \/ interp vars p2 + end. + + Theorem interp_valid : forall vars p, interp vars p -> valid vars p. + Proof. + induct p; simplify. + + apply ValidTruth. + + propositional. + + apply ValidVar. + assumption. + + propositional. + apply ValidAnd. + assumption. + assumption. + + propositional. + apply ValidOr1. + assumption. + apply ValidOr2. + assumption. + Qed. + + Theorem valid_interp : forall vars p, valid vars p -> interp vars p. + Proof. + induct 1; simplify. + + propositional. + + assumption. + + propositional. + + propositional. + + propositional. + Qed. + + Fixpoint commuter (p : prop) : prop := + match p with + | Truth => Truth + | Falsehood => Falsehood + | Var x => Var x + | And p1 p2 => And (commuter p2) (commuter p1) + | Or p1 p2 => Or (commuter p2) (commuter p1) + end. + + Theorem valid_commuter_fwd : forall vars p, valid vars p -> valid vars (commuter p). + Proof. + induct 1; simplify. + + apply ValidTruth. + + apply ValidVar. + assumption. + + apply ValidAnd. + assumption. + assumption. + + apply ValidOr2. + assumption. + + apply ValidOr1. + assumption. + Qed. + + Theorem valid_commuter_bwd : forall vars p, valid vars (commuter p) -> valid vars p. + Proof. + induct p; invert 1; simplify. + + apply ValidTruth. + + apply ValidVar. + assumption. + + apply ValidAnd. + apply IHp1. + assumption. + apply IHp2. + assumption. + + apply ValidOr2. + apply IHp2. + assumption. + + apply ValidOr1. + apply IHp1. + assumption. + Qed. +End SimplePropositional. + + +(** * Propositional logic with implication *) + +Module PropositionalWithImplication. + Inductive prop := + | Truth + | Falsehood + | Var (x : var) + | And (p1 p2 : prop) + | Or (p1 p2 : prop) + | Imply (p1 p2 : prop). + + Definition Not (p : prop) := Imply p Falsehood. + + Inductive valid (hyps : prop -> Prop) : prop -> Prop := + | ValidHyp : forall h, + hyps h + -> valid hyps h + | ValidTruthIntro : + valid hyps Truth + | ValidFalsehoodElim : forall p, + valid hyps Falsehood + -> valid hyps p + | ValidAndIntro : forall p1 p2, + valid hyps p1 + -> valid hyps p2 + -> valid hyps (And p1 p2) + | ValidAndElim1 : forall p1 p2, + valid hyps (And p1 p2) + -> valid hyps p1 + | ValidAndElim2 : forall p1 p2, + valid hyps (And p1 p2) + -> valid hyps p2 + | ValidOrIntro1 : forall p1 p2, + valid hyps p1 + -> valid hyps (Or p1 p2) + | ValidOrIntro2 : forall p1 p2, + valid hyps p2 + -> valid hyps (Or p1 p2) + | ValidOrElim : forall p1 p2 p, + valid hyps (Or p1 p2) + -> valid (fun h => h = p1 \/ hyps h) p + -> valid (fun h => h = p2 \/ hyps h) p + -> valid hyps p + | ValidImplyIntro : forall p1 p2, + valid (fun h => h = p1 \/ hyps h) p2 + -> valid hyps (Imply p1 p2) + | ValidImplyElim : forall p1 p2, + valid hyps (Imply p1 p2) + -> valid hyps p1 + -> valid hyps p2 + | ValidExcludedMiddle : forall p, + valid hyps (Or p (Not p)). + + Fixpoint interp (vars : var -> Prop) (p : prop) : Prop := + match p with + | Truth => True + | Falsehood => False + | Var x => vars x + | And p1 p2 => interp vars p1 /\ interp vars p2 + | Or p1 p2 => interp vars p1 \/ interp vars p2 + | Imply p1 p2 => interp vars p1 -> interp vars p2 + end. + + Theorem valid_interp : forall vars hyps p, + valid hyps p + -> (forall h, hyps h -> interp vars h) + -> interp vars p. + Proof. + induct 1; simplify. + + apply H0. + assumption. + + propositional. + + propositional. + + propositional. + + propositional. + + propositional. + + propositional. + + propositional. + + propositional. + apply IHvalid2. + propositional. + equality. + apply H2. + assumption. + apply IHvalid3. + propositional. + equality. + apply H2. + assumption. + + apply IHvalid. + propositional. + equality. + apply H0. + assumption. + + propositional. + + excluded_middle (interp vars p); propositional. + (* Note that use of excluded middle is a bit controversial in Coq, + * and we'll generally be trying to avoid it, + * but it helps enough with this example that we don't sweat the details. *) + Qed. + + Lemma valid_weaken : forall hyps1 p, + valid hyps1 p + -> forall hyps2 : prop -> Prop, + (forall h, hyps1 h -> hyps2 h) + -> valid hyps2 p. + Proof. + induct 1; simplify. + + apply ValidHyp. + apply H0. + assumption. + + apply ValidTruthIntro. + + apply ValidFalsehoodElim. + apply IHvalid. + assumption. + + apply ValidAndIntro. + apply IHvalid1. + assumption. + apply IHvalid2. + assumption. + + apply ValidAndElim1 with p2. + apply IHvalid. + assumption. + + apply ValidAndElim2 with p1. + apply IHvalid. + assumption. + + apply ValidOrIntro1. + apply IHvalid. + assumption. + + apply ValidOrIntro2. + apply IHvalid. + assumption. + + apply ValidOrElim with p1 p2. + apply IHvalid1. + assumption. + apply IHvalid2. + first_order. + apply IHvalid3. + first_order. + + apply ValidImplyIntro. + apply IHvalid. + propositional. + right. + apply H0. + assumption. + + apply ValidImplyElim with p1. + apply IHvalid1. + assumption. + apply IHvalid2. + assumption. + + apply ValidExcludedMiddle. + Qed. + + Lemma valid_cut : forall hyps1 p p', + valid hyps1 p + -> forall hyps2, valid hyps2 p' + -> (forall h, hyps1 h -> hyps2 h \/ h = p') + -> valid hyps2 p. + Proof. + induct 1; simplify. + + apply H1 in H. + propositional. + apply ValidHyp. + assumption. + equality. + + apply ValidTruthIntro. + + apply ValidFalsehoodElim. + apply IHvalid; assumption. + + apply ValidAndIntro. + apply IHvalid1; assumption. + apply IHvalid2; assumption. + + apply ValidAndElim1 with p2. + apply IHvalid; assumption. + + apply ValidAndElim2 with p1. + apply IHvalid; assumption. + + apply ValidOrIntro1. + apply IHvalid; assumption. + + apply ValidOrIntro2. + apply IHvalid; assumption. + + apply ValidOrElim with p1 p2. + apply IHvalid1; assumption. + apply IHvalid2. + apply valid_weaken with hyps2. + assumption. + propositional. + first_order. + apply IHvalid3. + apply valid_weaken with hyps2. + assumption. + propositional. + first_order. + + apply ValidImplyIntro. + apply IHvalid. + apply valid_weaken with hyps2. + assumption. + propositional. + first_order. + + apply ValidImplyElim with p1. + apply IHvalid1; assumption. + apply IHvalid2; assumption. + + apply ValidExcludedMiddle. + Qed. + + Fixpoint varsOf (p : prop) : list var := + match p with + | Truth + | Falsehood => [] + | Var x => [x] + | And p1 p2 + | Or p1 p2 + | Imply p1 p2 => varsOf p1 ++ varsOf p2 + end. + + Lemma interp_valid'' : forall p hyps, + (forall x, In x (varsOf p) -> hyps (Var x) \/ hyps (Not (Var x))) + -> (forall x, hyps (Var x) -> ~hyps (Not (Var x))) + -> IF interp (fun x => hyps (Var x)) p + then valid hyps p + else valid hyps (Not p). + Proof. + induct p; unfold IF_then_else; simplify. + + left; propositional. + apply ValidTruthIntro. + + right; propositional. + apply ValidImplyIntro. + apply ValidHyp. + propositional. + + specialize (H x); propositional. + left; propositional. + apply ValidHyp. + assumption. + right; first_order. + apply ValidHyp. + assumption. + + excluded_middle (interp (fun x => hyps (Var x)) p1). + excluded_middle (interp (fun x => hyps (Var x)) p2). + left; propositional. + apply ValidAndIntro. + assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + apply IHp1; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + apply IHp2; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + right; propositional. + assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + apply IHp2; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + apply ValidImplyIntro. + apply ValidImplyElim with p2. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidAndElim2 with p1. + apply ValidHyp. + propositional. + right; propositional. + assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + apply IHp1; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H2; propositional. + apply ValidImplyIntro. + apply ValidImplyElim with p1. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidAndElim1 with p2. + apply ValidHyp. + propositional. + + excluded_middle (interp (fun x => hyps (Var x)) p1). + left; propositional. + apply ValidOrIntro1. + assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + apply IHp1; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H2; propositional. + excluded_middle (interp (fun x => hyps (Var x)) p2). + left; propositional. + apply ValidOrIntro2. + assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + apply IHp2; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + right; propositional. + apply ValidImplyIntro. + apply ValidOrElim with p1 p2. + apply ValidHyp. + propositional. + assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + apply IHp1; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + apply ValidImplyElim with p1. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidHyp. + propositional. + assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + apply IHp2; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + apply ValidImplyElim with p2. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidHyp. + propositional. + + excluded_middle (interp (fun x => hyps (Var x)) p1). + excluded_middle (interp (fun x => hyps (Var x)) p2). + left; propositional. + apply ValidImplyIntro. + assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + apply IHp2; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + apply valid_weaken with hyps. + assumption. + propositional. + right; propositional. + apply ValidImplyIntro. + assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + apply IHp1; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H3; propositional. + assert (IF interp (fun x : var => hyps (Var x)) p2 then valid hyps p2 else valid hyps (Not p2)). + apply IHp2; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H4; propositional. + apply ValidImplyElim with p2. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidImplyElim with p1. + apply ValidHyp. + propositional. + apply valid_weaken with hyps. + assumption. + propositional. + left; propositional. + apply ValidImplyIntro. + assert (IF interp (fun x : var => hyps (Var x)) p1 then valid hyps p1 else valid hyps (Not p1)). + apply IHp1; propositional. + apply H. + apply in_or_app; propositional. + unfold IF_then_else in H2; propositional. + apply ValidFalsehoodElim. + apply ValidImplyElim with p1. + apply valid_weaken with hyps. + assumption. + propositional. + apply ValidHyp. + propositional. + Qed. + + Lemma interp_valid' : forall p leftToDo alreadySplit, + (forall x, In x (varsOf p) -> In x (alreadySplit ++ leftToDo)) + -> forall hyps, (forall x, In x alreadySplit -> hyps (Var x) \/ hyps (Not (Var x))) + -> (forall x, hyps (Var x) \/ hyps (Not (Var x)) -> In x alreadySplit) + -> (forall x, hyps (Var x) -> ~hyps (Not (Var x))) + -> (forall vars : var -> Prop, + (forall x, hyps (Var x) -> vars x) + -> (forall x, hyps (Not (Var x)) -> ~vars x) + -> interp vars p) + -> valid hyps p. + Proof. + induct leftToDo; simplify. + + rewrite app_nil_r in H. + assert (IF interp (fun x : var => hyps (Var x)) p then valid hyps p else valid hyps (Not p)). + apply interp_valid''; first_order. + unfold IF_then_else in H4; propositional. + exfalso. + apply H4. + apply H3. + propositional. + first_order. + + excluded_middle (In a alreadySplit). + + apply IHleftToDo with alreadySplit; simplify. + apply H in H5. + apply in_app_or in H5. + simplify. + apply in_or_app. + propositional; subst. + propositional. + first_order. + first_order. + first_order. + first_order. + + apply ValidOrElim with (Var a) (Not (Var a)). + apply ValidExcludedMiddle. + + apply IHleftToDo with (alreadySplit ++ [a]); simplify. + apply H in H5. + apply in_app_or in H5. + simplify. + apply in_or_app. + propositional; subst. + left; apply in_or_app; propositional. + left; apply in_or_app; simplify; propositional. + apply in_app_or in H5. + simplify. + propositional; subst. + apply H0 in H6. + propositional. + propositional. + propositional. + invert H5. + apply in_or_app. + simplify. + propositional. + apply in_or_app. + simplify. + first_order. + invert H5. + apply in_or_app. + simplify. + first_order. + propositional. + invert H5. + invert H7. + first_order. + invert H5. + first_order. + apply H3. + first_order. + first_order. + + apply IHleftToDo with (alreadySplit ++ [a]); simplify. + apply H in H5. + apply in_app_or in H5. + simplify. + apply in_or_app. + propositional; subst. + left; apply in_or_app; propositional. + left; apply in_or_app; simplify; propositional. + apply in_app_or in H5. + simplify. + propositional; subst. + apply H0 in H6. + propositional. + propositional. + propositional. + invert H5. + apply in_or_app. + simplify. + first_order. + invert H5. + apply in_or_app. + simplify. + propositional. + apply in_or_app. + simplify. + first_order. + propositional. + invert H7. + invert H7. + invert H5. + first_order. + first_order. + apply H3. + first_order. + first_order. + Qed. + + Theorem interp_valid : forall p, + (forall vars, interp vars p) + -> valid (fun _ => False) p. + Proof. + simplify. + apply interp_valid' with (varsOf p) []; simplify; first_order. + Qed. +End PropositionalWithImplication.