how to turn goal into a hypothesis automatically

Stream: new members

[Ben Nale]

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]

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

[Johan Commelin]

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]

Im typing my code :)

[Ben Nale]

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]

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]

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