Discrete Mathematics - Ecee.colorado.edu

Discrete MathematicsJeremy SiekSpring 2010Jeremy SiekDiscrete Mathematics1 / 24

Outline of Lecture 31. Proofs and Isabelle2. Proof Strategy, Forward and Backwards Reasoning3. Making MistakesJeremy SiekDiscrete Mathematics2 / 24

Theorems and ProofsIIn the context of propositional logic, a theorem is just a tautology.IIn this course, we’ll be writing theorems and their proofs in theIsabelle/Isar proof language.IHere’s the syntax for a theorem in Isabelle/Isar.theorem "P"proof step 1step 2.Istep nqedEach step applies an inference rule to establish the truth of someproposition.Jeremy SiekDiscrete Mathematics3 / 24

Inference RulesIWhen applying inference rules, use the keyword have to establishintermediate truths and use the keyword show to conclude thesurrounding theorem or sub-proof.IMost inference rules can be categorized as either an introductionor elimination rule.IIntroduction rules are for creating bigger propositions.IElimination rules are for using propositions.We write “Li proves P ” if there is a preceeding step or assumptionin the proof that is labeled Li and whose proposition is P .IJeremy SiekDiscrete Mathematics4 / 24

Introduction RulesAnd If Li proves P and Lj proves Q, then writefrom Li Lj have Lk : "P Q" .Or (1) If Li proves P , then writefrom Li have Lk : "P Q" .Or (2) If Li proves Q, then writefrom Li have Lk : "P Q" .Implieshave Lk : "P Q"proofassume Li : "P".· · · show "Q" · · ·qedJeremy SiekDiscrete Mathematics5 / 24

Introduction Rules, cont’dNot have Lk : " P"proofassume Li : "P".· · · show "False" · · ·qedHint: The Appendix of our text Isabelle/HOL – A Proof Assistant forHigher-Order Logic lists the logical connectives, such as and , andfor each of them gives two ways to input them as ASCI text. If youuse Emacs (or XEmacs) to edit your Isabelle files, then the x-symbolpackage can be used to display the logic connectives in their traditionalform.Jeremy SiekDiscrete Mathematics6 / 24

Using AssumptionsISometimes the thing you need to prove is already an assumption.In this case your job is really easy!IIf Li proves P , writefrom Li have "P" .Jeremy SiekDiscrete Mathematics7 / 24

Example Prooftheorem "p p"proof show "p p"proofassume 1: "p"from 1 show "p" .qedqedInstead of proof -, you can apply the introduction ruleright away.theorem "p p"proofassume 1: "p"from 1 show "p" .qedJeremy SiekDiscrete Mathematics8 / 24

Exercisetheorem "p (p p)"Jeremy SiekDiscrete Mathematics9 / 24

Solutiontheorem "p (p p)"proofassume 1: "p"from 1 1 show "p p" .qedJeremy SiekDiscrete Mathematics10 / 24

Elimination RulesAnd (1) If Li proves P Q, then writefrom Li have Lk : "P" .And (2) If Li proves P Q, then writefrom Li have Lk : "Q" .Or If Li proves P Q, then writenote Limoreover { assume Lj : "P".· · · have "R" · · ·} moreover { assume Lm : "Q".· · · have "R" · · ·} ultimately have Lk : "R" .Jeremy SiekDiscrete Mathematics11 / 24

Elimination Rules, cont’dImplies If Li proves P Q and Lj proves P , then writefrom Li Lj have Lk : "Q" .(This rule is known as modus ponens.)Not If Li proves P and Lj proves P , then writefrom Li Lj have Lk : "Q" .False If Li proves False, then writefrom Li have Lk : "P" .Jeremy SiekDiscrete Mathematics12 / 24

Example Prooftheorem "(p q) (p q)"proofassume 1: "p q"from 1 have 2: "p" .from 2 show "p q" .qedJeremy SiekDiscrete Mathematics13 / 24

Another Prooftheorem "(p q) (p r) (q r) r"proofassume 1: "(p q) (p r) (q r)"from 1 have 2: "p q" .from 1 have 3: "(p r) (q r)" .from 3 have 4: "p r" .from 3 have 5: "q r" .note 2moreover { assume 6: "p"from 4 6 have "r" .} moreover { assume 7: "q"from 5 7 have "r" .} ultimately show "r" .qedJeremy SiekDiscrete Mathematics14 / 24

Exercisetheorem "(p q) (q r) (p r)"Jeremy SiekDiscrete Mathematics15 / 24

Solutiontheorem "(p q) (q r) (p r)"proofassume 1: "(p q) (q r)"from 1 have 2: "p q" .from 1 have 3: "q r" .show "p r"proofassume 4: "p"from 2 4 have 5: "q" .from 3 5 show "r" .qedqedJeremy SiekDiscrete Mathematics16 / 24

Forward and Backwards ReasoningAnd-Intro (forward)If Li proves P and Lj proves Q, then writefrom Li Lj have Lk : "P Q" .And-Intro (backwards)have Lk : "P Q"proof.· · · show "P" · · ·next.· · · show "Q" · · ·qedJeremy SiekDiscrete Mathematics17 / 24

Forward and Backwards Reasoning, cont’dOr-Intro (1) (forwards) If Li proves P , then writefrom Li have Lk : "P Q" .Or-Intro (1) (backwards)have Lk : "P Q"proof (rule disjI1).· · · show "P" · · ·qedJeremy SiekDiscrete Mathematics18 / 24

Forward and Backwards Reasoning, cont’dOr-Intro (2) (forwards) If Li proves Q, then writefrom Li have Lk : "P Q" .Or-Intro (2) (backwards)have Lk : "P Q"proof (rule disjI2).· · · show "Q" · · ·qedJeremy SiekDiscrete Mathematics19 / 24

StrategyILet the proposition you’re trying to prove guide your proof.IFind the top-most logical connective.IApply the introduction rule, backwards, for that connective.IKeep doing that until what you need to prove no longer containsany logical connectives.IThen work forwards from your assumptions (using eliminationrules) until you’ve proved what you ConclusionAssumptionJeremy SiekDiscrete Mathematics20 / 24

Making MistakesITo err is human.IIsabelle will catch your mistakes.IUnfortunately, Isabelle is bad at describing your mistake.IConsider the following attempted prooftheorem "p (p p)"proof show "p (p p)"proofassume 1: "p"from 1 show "p p"IWhen Isabelle gets to from 1 show "p p" (adding . at theend), it gives the following response:Failed to finish proofAt command ".".Jeremy SiekDiscrete Mathematics21 / 24

Making Mistakes, cont’dIIn this case, the mistake was a missing label in the from clause.Conjuction introduction requires two premises, not one. Here’sthe fix:theorem "p (p p)"proof show "p (p p)"proofassume 1: "p"from 1 1 show "p p" .qedqedIWhen Isablle says “no”, double check the inference rule. If thatdoesn’t work, get a classmate to look at it. If that doesn’t work,email the instructor with the minimal Isabelle file that exhibitsyour problem.Jeremy SiekDiscrete Mathematics22 / 24

Making Mistakes, cont’dIHere’s another proof with a typo:theorem "p p"proofassume 1: "p"from 1 show "q" .qedIIsabelle responds with:Local statement will fail to refine any pending goalFailed attempt to solve goal by exported rule :(p) qAt command " show ".IThe problem here is that the proposition in the show "q", doesnot match what we are trying to prove, which is p.Jeremy SiekDiscrete Mathematics23 / 24

Stuff to RememeberIHow to write Isabelle/Isar proofs of tautologies in PropositionalLogic.The introduction and elimination rules.IForwards and backwards reasoning.IJeremy SiekDiscrete Mathematics24 / 24

Discrete Mathematics Jeremy Siek Spring 2010 Jeremy Siek Discrete Mathematics 1/24. Outline of Lecture 3 1. Proofs and Isabelle 2. Proof Strategy, Forward and Backwards Reasoning 3. Making Mistakes Jeremy Siek Discrete Mathematics 2/24. Theorems and Proofs I In the conte