Anne Baanen Alexander Bentkamp Jasmin Blanchette Johannes Hölzl Jannis Limperg

Anne Baanen Alexander Bentkamp Jasmin Blanchette Johannes Hölzl Jannis Limperg The Hitchhiker’s Guide to Logical Verification 2020 Standard Edition (October 12, 2020) lean-forward.github.io/ logical-verification/2020 ii Contents Contents iii Preface vii I Basics 1 1 Definitions and Statements 3 1.1 Types and Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Type Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.3 Function Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.4 Lemma Statements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 1.5 Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . . 18 2 Backward Proofs 19 2.1 Tactic Mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.2 Basic Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.3 Reasoning about Connectives and Quantifiers . . . . . . . . . . . . . . 23 2.4 Reasoning about Equality . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.5 Rewriting Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.6 Proofs by Mathematical Induction . . . . . . . . . . . . . . . . . . . . . 29 2.7 Induction Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.8 Cleanup Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2.9 Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . . 31 3 Forward Proofs 33 3.1 Structured Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.2 Structured Constructs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.3 Forward Reasoning about Connectives and Quantifiers . . . . . . . . 37 3.4 Calculational Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.5 Forward Reasoning with Tactics . . . . . . . . . . . . . . . . . . . . . . 40 3.6 Dependent Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.7 The Curry–Howard Correspondence . . . . . . . . . . . . . . . . . . . . 43 3.8 Induction by Pattern Matching . . . . . . . . . . . . . . . . . . . . . . . 45 3.9 Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . . 47 iii II Functional–Logic Programming 49 4 Functional Programming 51 4.1 Inductive Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.2 Structural Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 4.3 Structural Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 4.4 Pattern Matching Expressions . . . . . . . . . . . . . . . . . . . . . . . 55 4.5 Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 4.6 Type Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 4.7 Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 4.8 Binary Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.9 Case Distinction and Induction Tactics . . . . . . . . . . . . . . . . . . 69 4.10 Dependent Inductive Types . . . . . . . . . . . . . . . . . . . . . . . . . 69 4.11 Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . . 72 5 Inductive Predicates 73 5.1 Introductory Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 5.2 Logical Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 5.3 Rule Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 5.4 Linear Arithmetic Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 5.5 Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 5.6 Further Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 5.7 Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . . 89 6 Monads 91 6.1 Introductory Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 6.2 Two Operations and Three Laws . . . . . . . . . . . . . . . . . . . . . . 93 6.3 A Type Class . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 6.4 No Efects . . . . . . . . . . . . uploads/Ingenierie_Lourd/ hitchhikers-guide.pdf

Tags
Ingénierie lemma proof tactic apply inductive
Documents similaires
  • 24
  • 0
  • 0
Afficher les détails des licences
Licence et utilisation
Gratuit pour un usage personnel Attribution requise
Partager