►Logic & Computation
▼Lectures
►Lecture 25:   Forward Reasoning
On this page:
1 Purpose
2 Outline
8.7
    contents  ← prev  up  next → 

Lecture 25: Forward Reasoning

1 Purpose

Learn how to do proofs by forward reasoning

2 Outline

We’ll show how to use have, a tactic you have already seen, to work forward, and also another tactic, suffices that allows you to work forward in a slightly more natural way.

Here are a bunch of examples!

theorem p6_back : ¬ Q -> (R -> Q) -> (R ∨ ¬ S) -> S -> False := 
 by intros nq rq rons s
    cases rons
    case inl r =>
      apply nq
      apply rq
      assumption
    case inr ns =>
      apply ns
      assumption
theorem p6_have : ¬ Q -> (R -> Q) -> (R ∨ ¬ S) -> S -> False := 
 by intros nq rq rons s
    cases rons
    case inl r =>
      have q : Q := by apply rq; assumption
      have f : False := by apply nq; assumption
      assumption
    case inr ns =>
      have f : False := by apply ns; assumption
      assumption
theorem p6_suffices : ¬ Q -> (R -> Q) -> (R ∨ ¬ S) -> S -> False := 
 by intros nq rq rons s
    cases rons
    case inl r =>
      suffices q : Q by apply nq; assumption
      apply rq; assumption
    case inr ns =>
      -- this doesn't do anything, since False was 
      -- already our goal!
      suffices f : False by assumption
      apply ns; assumption
inductive ev : Nat → Prop where
  | O : ev 0
  | SS (n : Nat) (H : ev n) : ev (Nat.succ (Nat.succ n))

theorem ev_plus6 : forall n, ev n → ev (Nat.add n 6) :=
 by intros n H
    apply ev.SS
    apply ev.SS
    apply ev.SS
    assumption

theorem ev_plus6_have : forall n, ev n → ev (Nat.add n 6) :=
 by intros n H
    have ev2 : ev (Nat.add n 2) := by 
      apply ev.SS; assumption
    have ev4 : ev (Nat.add n 4) := by 
      apply ev.SS; assumption
    have ev6 : ev (Nat.add n 6) := by 
      apply ev.SS; assumption
    exact ev6

theorem ev_plus6_suffices : forall n, ev n → ev (Nat.add n 6) :=
 by intros n H
    suffices ev4 : ev (Nat.add n 4) by
      apply ev.SS
      assumption
    suffices ev2 : ev (Nat.add n 2) by
      apply ev.SS
      assumption
    apply ev.SS
    assumption
inductive ev' : Nat → Prop :=
  | O : ev' 0
  | SSO : ev' 2
  | sum n m (Hn : ev' n) (Hm : ev' m) : ev' (Nat.add n m)

example : ev' 8 :=
 by suffices rr : 8 = Nat.add (Nat.add 2 2) (Nat.add 2 2) by
      rw [rr]
      suffices ev4 : ev' (Nat.add 2 2) by 
        constructor <;> assumption
      constructor <;> constructor
    rfl

Tactic Use

Tactic Description

suffices h : H by ...

Creates new hypothesis h : H which you can use to complete the proof. Once you finish the proof, you now have to prove h : H. This can be useful to 'cut' a proof in the middle: first go from the middle to the end, and then go back and prove up to that middle point.

rename_i h

Gives a name h to the most recent anonymous hypothesis (unnamed or given with italicized, gray, crossed names). This can be useful if you manage to override a name, or you don't want to actually switch into a case before using names that it introduces.

    contents  ← prev  up  next →