index.md (3600B)
1 +++ 2 title = 'Backward proofs' 3 +++ 4 # Backward proofs 5 6 This is like going up the proof tree. 7 8 Tactical propositions look like this: 9 10 ```lean 11 lemma lemma_name : 12 statement := 13 begin 14 proof 15 end 16 ``` 17 18 It can also be a one-line proof, with `by`: 19 20 ```lean 21 lemma lemma_name : 22 statement := 23 by tactic 24 ``` 25 26 Tactics: 27 28 - `intro h` creates assumption `h` from left-hand of implication or quantifiers (`intros` for multiple at once) 29 - `apply h` matches goal's conclusion with conclusion of `h` and adds `h`'s hypotheses as new goals 30 - `exact h` matches goal's conclusion with conclusion of `h`, closing the goal (could also use `apply`) 31 - `assumption` finds a hypothesis from the context that matches the goal's conclusion and applies it 32 - `refl` proves reflexivity (`l = r`) including unfolding definitions, β reduction, and more 33 - `and.intro`, `and.elim_right`, `and.elim_left`, `or.intro_right`, `or.intro_left`, `or.elim` are for logical connectives (∧, ∨) 34 - `eq.refl` for reflexivity, `eq.subst h` to substitute h into equality 35 - `rw h` applies `h` once as left-to-right rewrite rule. can apply right-to-left by writing `←h`. 36 - `not_def`: ¬a ↔ a → false 37 - `simp [h1, h2...]` applies rewrite rules and hypothesis set 38 - `cc` applies congruence closure 39 - `em` applies Law of Excluded Middle (p ∨ ¬p) 40 - `induction'` performs proof by induction, yields one subgoal per constructor 41 - `rename h1 h2` renames `h1` to `h2` 42 - `clear h1` removes `h1` 43 44 ## Rewrite rules 45 46 This wasn't covered in the lecture, but it's useful so I'll add them here. 47 48 <table> 49 <tr> 50 <th>Implication</th> 51 <th>Conjunction</th> 52 <th>Negation</th> 53 <th>Disjunction</th> 54 <th>Bi-implication ("if and only if")</th> 55 <th>True & False</th> 56 </tr> 57 <tr> 58 <td> 59 <img src="68c840d11fe44ef29cb662c5b8ca1641.png" alt="implication-elimination.png"> 60 </td> 61 <td> 62 <img src="d6ea36c804da4da3a1ba5be0b92d3234.png" alt="and-elimination.png"> 63 </td> 64 <td> 65 <img src="6a8c517e54014b91bc71be3cb288d803.png" alt="negation-elimination.png"> 66 </td> 67 <td> 68 <img src="6463b42ec717467c82a85101441f06c8.png" alt="disjunction-elimination.png"> 69 </td> 70 <td> 71 <img src="2be50f863ace4c788b9dbe612c835bcb.png" alt="bi-implication-elimination.png"> 72 </td> 73 <td> 74 <img src="e4ca711cb4bf4095806d8d7478b38b66.png" alt="falsum-elimination.png"> 75 </td> 76 </tr> 77 <tr> 78 <td> 79 <img src="042e1ee9cd194f558fe79fd0f59857d4.png" alt="Implication introduction"> 80 </td> 81 <td> 82 <img src="3fe765a8a14e4b8db6de84bcf5d6c97a.png" alt="conjunction-introduction.png"> 83 </td> 84 <td> 85 <img src="5615644a2e664300a6d97325777bde3c.png" alt="Negation introduction"> 86 </td> 87 <td> 88 <img src="a3129857d2114c8cae495ca1917c27c5.png" alt="disjunction-introduction.png"> 89 </td> 90 <td> 91 <img src="50a65a98d80b4e5babf78c571487649e.png" alt="bi-implication-introduction.png"> 92 </td> 93 <td> 94 <img src="d60db12d0f7941f3baf1b81243ea2aca.png" alt="truth-introduction.png"> 95 </td> 96 </tr> 97 </table> 98 99 Quantifiers 100 101 <table> 102 <tr> 103 <th>Universal</th> 104 <th>Existential</th> 105 </tr> 106 <tr> 107 <td> 108 <img src="1cf1941c0bd24761a12d32d17945432f.png" alt="universal-elimination.png"> 109 </td> 110 <td> 111 <img src="25529c12211e4d65986715e83210a531.png" alt="existential-elimination.png"> 112 </td> 113 </tr> 114 <tr> 115 <td> 116 <img src="fb5ddc0670d14b739136cdcc6450584f.png" alt="universal-introduction.png"> 117 </td> 118 <td> 119 <img src="3a95c65fe13f4c41a39a5fe143fa3919.png" alt="existential-introduction.png"> 120 </td> 121 </tr> 122 123 Conjunction-negation: 124 125  126 127 Proof by contradiction: 128 129  130 131 Induction: 132 133 