## Stream: new members

### Topic: how to turn goal into a hypothesis automatically

#### Ben Nale (Sep 10 2020 at 03:11):

Hi. I want to turn my goals into hypotheses so that when I prove them I could use them later - im doing induction.
I could do a have with the goal contents but actually I want to write a repeat loop.

#### Johan Commelin (Sep 10 2020 at 03:17):

Hi Ben, welcome! Could you please give some example code (format it with #backticks)?

#### Johan Commelin (Sep 10 2020 at 03:17):

It's not so clear to me what you want exactly. If you use induction n with n IH, as tactic, then it will automatically put an induction hypothesis in your goal state.

#### Ben Nale (Sep 10 2020 at 03:25):

Im typing my code :)

#### Ben Nale (Sep 10 2020 at 03:28):

def com:  ℕ → ℕ
| 0 := 1
| 1:= 3
| (n+2) := com (n+1) + 2*com(n)

lemma com_7 (k: ℕ):com(6*k)%7 =1 ∧ com(6*k+1) %7 =3 ∧ com(6*k+2) %7 =5 ∧ com(6*k+3) %7=4 ∧ com(6*k+4) %7 = 0 ∧ com(6*k+5) %7=1 :=
begin
induction k with d hd,
simp, omega,
rcases hd with ⟨ h1,h2,h3,h4,h5,h6 ⟩,
end


#### Ben Nale (Sep 10 2020 at 03:31):

the proof i am trying to implement is that com mod 7 is basically
1 3 5 4 0 1 and the pattern repeats

#### Ben Nale (Sep 10 2020 at 03:44):

Actually, I've found a way to do it with 2step induction. Thanks for your help :)

Last updated: Dec 20 2023 at 11:08 UTC